this repo has no description
anil.recoil.org
1opam-version: "2.0"
2synopsis: "The HOL-Light interactive theorem prover"
3description: """
4HOL Light is a computer program written by John Harrison to help users prove
5interesting mathematical theorems completely formally in higher order logic.
6It sets a very exacting standard of correctness, but provides a number of
7automated tools and pre-proved mathematical theorems (e.g. about arithmetic,
8basic set theory and real analysis) to save the user work. It is also fully
9programmable, so users can extend it with new theorems and inference rules
10without compromising its soundness. There are a number of versions of HOL,
11going back to Mike Gordon’s work in the early 80s. Compared with other HOL
12systems, HOL Light uses a much simpler logical core and has little legacy code,
13giving the system a simple and uncluttered feel. Despite its simplicity, it
14offers theorem proving power comparable to, and in some areas greater than,
15other versions of HOL, and has been used for some significant
16industrial-scale verification applications.
17
18This package will install `hol.sh` which will run OCaml REPL with HOL Light
19loaded.
20To use a compiled module of HOL Light, please install with the
21hol_light_module OPAM package.
22"""
23authors: "HOL Light"
24license: "https://github.com/jrh13/hol-light/blob/master/LICENSE"
25homepage: "https://hol-light.github.io/"
26bug-reports: "https://github.com/jrh13/hol-light/issues"
27dev-repo: "git+https://github.com/jrh13/hol-light.git"
28maintainer: ["John Harrison <jrh013@gmail.com>" "Juneyoung Lee <aqjune@gmail.com>"]
29depopts: [ "hol_light_module" ]
30depends: [
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]
57available: os = "linux" | os = "macos" | os = "cygwin"
58build: [
59 [make] {!hol_light_module:installed}
60 [make "HOLLIGHT_USE_MODULE=1"] {hol_light_module:installed}
61 ["sh" "-c" "sed \"s^%{hol_light:build}%^%{hol_light:lib}%^g\" hol.sh >hol_new.sh"]
62 ["mv" "hol_new.sh" "hol.sh"]
63 ["chmod" "+x" "hol.sh"]
64]
65install: [
66 ["mkdir" "-p" "%{hol_light:lib}%"]
67 ["cp" "-r" "." "%{hol_light:lib}%"]
68 ["cp" "hol.sh" "%{bin}%/hol.sh"]
69]
70remove: [
71 ["rm" "%{bin}%/hol.sh"]
72 ["rm" "-rf" "%{hol_light:lib}%"]
73]
74extra-source "META" {
75 src: "https://gist.githubusercontent.com/aqjune/4b77edcc29faeebf15fcd4949f27d7ae/raw/3ff64fa63304e1944e4fc6fef8c7a7a5a2009bc2/META"
76 checksum: [
77 "sha256=60ba1ecd6c1b4c7ef96a1547111279cd7c27abefd2a09ae18e3bf0a8fa82698c"
78 "md5=0766bfdee09f7a31b4a36f3038b83fa0"
79 ]
80}
81url {
82 src:
83 "https://github.com/jrh13/hol-light/archive/refs/tags/Release-3.0.0.tar.gz"
84 checksum: [
85 "md5=6b7ece405efe5d891f547042d102f9ee"
86 "sha512=ffedba9a96cd0058a1ec74825c25b22f5b29117c2e7378715c5f8efc576e6008576b0649395e8f5fab8575f7f81f8816fb19a57c81413bc0d9e7d0c49b8a4c99"
87 ]
88}