this repo has no description
Merge pull request #26745 from aqjune/opam-publish-hol_light.3.0.0
Package hol_light.3.0.0
authored by
Shon Feder
and committed by
GitHub
9be670dc
4bbd530b
+89
+89
packages/hol_light/hol_light.3.0.0/opam
+89
packages/hol_light/hol_light.3.0.0/opam
···
1
+
opam-version: "2.0"
2
+
synopsis: "The HOL-Light interactive theorem prover"
3
+
description: """
4
+
HOL Light is a computer program written by John Harrison to help users prove
5
+
interesting mathematical theorems completely formally in higher order logic.
6
+
It sets a very exacting standard of correctness, but provides a number of
7
+
automated tools and pre-proved mathematical theorems (e.g. about arithmetic,
8
+
basic set theory and real analysis) to save the user work. It is also fully
9
+
programmable, so users can extend it with new theorems and inference rules
10
+
without compromising its soundness. There are a number of versions of HOL,
11
+
going back to Mike Gordon’s work in the early 80s. Compared with other HOL
12
+
systems, HOL Light uses a much simpler logical core and has little legacy code,
13
+
giving the system a simple and uncluttered feel. Despite its simplicity, it
14
+
offers theorem proving power comparable to, and in some areas greater than,
15
+
other versions of HOL, and has been used for some significant
16
+
industrial-scale verification applications.
17
+
18
+
This package will install `hol.sh` which will run OCaml REPL with HOL Light
19
+
loaded.
20
+
To use a compiled module of HOL Light, please install with the
21
+
hol_light_module OPAM package.
22
+
"""
23
+
authors: "HOL Light"
24
+
license: "https://github.com/jrh13/hol-light/blob/master/LICENSE"
25
+
homepage: "https://hol-light.github.io/"
26
+
bug-reports: "https://github.com/jrh13/hol-light/issues"
27
+
dev-repo: "git+https://github.com/jrh13/hol-light.git"
28
+
maintainer: ["John Harrison <jrh013@gmail.com>" "Juneyoung Lee <aqjune@gmail.com>"]
29
+
depopts: [ "hol_light_module" ]
30
+
depends: [
31
+
("ocaml" {> "4.02.0" & < "4.04.0"} &
32
+
"camlp5" {>= "6.15" & <= "7.1"})
33
+
|
34
+
("ocaml" {>= "4.04.0" & < "4.06.0"} &
35
+
"camlp5" {>= "7.01" & <= "7.1"})
36
+
|
37
+
("ocaml" {>= "4.06.1" & < "4.08.0"} &
38
+
"num" &
39
+
"camlp5" {>= "7.06" & < "7.15"} &
40
+
"ledit")
41
+
|
42
+
("ocaml" {>= "4.08.0" & < "4.10.0"} &
43
+
"num" &
44
+
"camlp5" {>= "7.11" & < "8.01"} &
45
+
"ledit")
46
+
|
47
+
("ocaml" {>= "4.10.0" & < "4.14.0"} &
48
+
"num" &
49
+
"camlp5" {>= "7.14"} &
50
+
"ledit")
51
+
|
52
+
("ocaml" {>= "4.14.0"} &
53
+
"camlp5" {>= "8.0"} &
54
+
"zarith" {>= "1.5"} &
55
+
"ledit")
56
+
]
57
+
available: os = "linux" | os = "macos" | os = "cygwin"
58
+
build: [
59
+
[make] {!hol_light_module:installed}
60
+
[make "HOLLIGHT_USE_MODULE=1"] {hol_light_module:installed}
61
+
]
62
+
install: [
63
+
["cp" "hol.sh" "%{bin}%/hol.sh"]
64
+
65
+
["mkdir" "-p" "%{hol_light:lib}%"] {hol_light_module:installed}
66
+
["cp" "hol_lib.cma" "hol_lib.cmi" "hol_lib.cmo" "hol_lib.cmx" "hol_lib.cmxa" "hol_lib.o" "hol_lib.a"
67
+
"bignum.cmi" "bignum.cmo" "bignum.cmx" "bignum.o"
68
+
"hol_loader.cmi" "hol_loader.cmo" "hol_loader.cmx" "hol_loader.o" "META"
69
+
"%{hol_light:lib}%"] {hol_light_module:installed}
70
+
]
71
+
remove: [
72
+
["rm" "%{bin}%/hol.sh"]
73
+
["rm" "-rf" "%{hol_light:lib}%"] {hol_light_module:installed}
74
+
]
75
+
extra-source "META" {
76
+
src: "https://gist.githubusercontent.com/aqjune/4b77edcc29faeebf15fcd4949f27d7ae/raw/3ff64fa63304e1944e4fc6fef8c7a7a5a2009bc2/META"
77
+
checksum: [
78
+
"sha256=60ba1ecd6c1b4c7ef96a1547111279cd7c27abefd2a09ae18e3bf0a8fa82698c"
79
+
"md5=0766bfdee09f7a31b4a36f3038b83fa0"
80
+
]
81
+
}
82
+
url {
83
+
src:
84
+
"https://github.com/jrh13/hol-light/archive/refs/tags/Release-3.0.0.tar.gz"
85
+
checksum: [
86
+
"md5=6b7ece405efe5d891f547042d102f9ee"
87
+
"sha512=ffedba9a96cd0058a1ec74825c25b22f5b29117c2e7378715c5f8efc576e6008576b0649395e8f5fab8575f7f81f8816fb19a57c81413bc0d9e7d0c49b8a4c99"
88
+
]
89
+
}