hol-light icon indicating copy to clipboard operation
hol-light copied to clipboard
verified publisher icon jrh13

HOL-Light with recent versions of ocaml & camlp5 ?

Open fblanqui opened this issue 3 years ago • 5 comments

Hi. Is there any plan to have hol-light working with recent versions of ocaml and camlp5? See https://github.com/jrh13/hol-light/pull/71.

fblanqui avatar Jan 16 '23 12:01 fblanqui

I just opened PR #74 that might be of interest.

mpu avatar Jan 16 '23 17:01 mpu

The latest version of ocaml now seems to be 5, but there are no combinations in #71 with ocaml 5. The link in the README file to Ckpt no longer works and the Cryopid repository doesn't seem to have any downloads available. As well as adding package num (as instructed in README file) it's necessary to download camp-streams. But then I'm stuck with incompatible preprocessor, and I don't seem to be able to revert to an earlier version of ocaml.

rbjones avatar Mar 08 '23 19:03 rbjones

The latest version of ocaml now seems to be 5, but there are no combinations in https://github.com/jrh13/hol-light/pull/71 with ocaml 5. The link in the README file to Ckpt no longer works and the Cryopid repository doesn't seem to have any downloads available. As well as adding package num (as instructed in README file) it's necessary to download camp-streams. But then I'm stuck with incompatible preprocessor, and I don't seem to be able to revert to an earlier version of ocaml.

README is recently updated to introduce three checkpointing tools that work. :) HOL Light will use Zarith instead of num if OCaml 4.14 is used. Zarith officially succeeds Num and can be installed using opam.

make will create hol.sh which will contain a proper command line invoking the OCaml REPL according to its version.

aqjune avatar Apr 04 '24 16:04 aqjune

I can confirm that it works. I recently setup an opam switch from scratch for ocaml 4.14.1, then run make and got a working hol.sh. Good job @aqjune, HOL-Light is now a fair bit less finicky to setup!

One thing that tripped me initially is that I had installed the num and camlp5 packages with opam on the default switch (the one using the system compiler). This does not work well as the libraries are not placed in the stdlib directory. The working procedure involved creating a new switch with opam switch create hol ocaml-base-compiler=4.14.1 then installing num and camlp5 in this switch.

mpu avatar Apr 05 '24 11:04 mpu

@mpu Oops, I just read your message. Do you want to open an issue with the error message please?

aqjune avatar Apr 16 '24 17:04 aqjune