search

jrh13 / hol-light

The HOL Light theorem prover
Other
435 stars 78 forks source link

opam installation #67

Open ncihnegn opened 2 years ago

ncihnegn commented 2 years ago

Probably a naive question: can hol-light be installed as an opam pacakge? If not, why?

PetrosPapapa commented 2 years ago

No because it runs on the OCaml toplevel REPL and is not compiled.

fblanqui commented 1 year ago

To know which pairs ocaml-camlp5 work, see https://github.com/jrh13/hol-light/pull/71.

aqjune commented 1 month ago

hol light is now available on opam. It will create hol.sh that will launch an OCaml REPL with proper flags according to the OCaml version.

opam install hol_light
# To compile the core module of HOL Light and use, add hol_light_module
opam install hol_light hol_light_module