HOL-Light with recent versions of ocaml & camlp5 ?

[fblanqui]

Hi. Is there any plan to have hol-light working with recent versions of ocaml and camlp5? See #71.

[mpu]

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

[rbjones]

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.

[aqjune]

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.

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.

[mpu]

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.

[aqjune]

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

[jrh13]

I'm assuming all is now good since HOL Light now works well with even the latest OCaml 5.4