this repo has no description
Merge pull request #26744 from aqjune/opam-publish-hol_light_module.1.0
Package hol_light_module.1.0
authored by
Shon Feder
and committed by
GitHub
aaa3197f
b7d4c114
+29
+29
packages/hol_light_module/hol_light_module.1.0/opam
+29
packages/hol_light_module/hol_light_module.1.0/opam
···
1
+
opam-version: "2.0"
2
+
authors: "HOL Light"
3
+
homepage: "https://hol-light.github.io"
4
+
bug-reports: "https://github.com/jrh13/hol-light/issues"
5
+
maintainer: ["John Harrison <jrh013@gmail.com>" "Juneyoung Lee <aqjune@gmail.com>"]
6
+
depends: [
7
+
"ocaml" {>= "4.14.0"}
8
+
]
9
+
synopsis: "A flag for compiling HOL Light core to a bytecode and native module"
10
+
license: "https://github.com/jrh13/hol-light/blob/master/LICENSE"
11
+
dev-repo: "git+https://github.com/jrh13/hol-light.git"
12
+
description: """
13
+
Installing this package makes the hol-light package to build the
14
+
bytecode and native module of HOL Light core as well.
15
+
16
+
NOTE: This extends the trusted base of HOL Light to include its inliner script,
17
+
inline_loads.ml. inline_loads.ml is an OCaml program in HOL Light that receives
18
+
an HOL Light proof and replaces the loads/loadt/needs function invocations with
19
+
their actual contents. Please install this package only if having this
20
+
additional trusted base is considered okay.
21
+
"""
22
+
url {
23
+
src:
24
+
"https://github.com/aqjune/hol-light-module/archive/refs/tags/1.0.tar.gz"
25
+
checksum: [
26
+
"md5=232eeb03c8fa6f4f7d076943ad652582"
27
+
"sha512=ec0ae802a6977366b26e0438670579cf3a3d329d3600ae5e2493a01867259d74bc3a09d7f27efd31ef96b6385fdce089aa06fb04611db2077f37aa9d66ce0cfe"
28
+
]
29
+
}