jrh13 / hol-light

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

Add camlp5 8.03 support, update make switch to use it #102

Closed aqjune closed 4 months ago

aqjune commented 5 months ago

This patch adds camlp5 8.03 support and does the following updates:

Using camlp5 8.03 is necessary to enable using native OCaml REPL in the future.

aqjune commented 4 months ago

I checked that s2n bignum proofs checked successfully with this patch.

jrh13 commented 4 months ago

Thank you, this is a very worthwhile reorganization and improvement.

I've checked that the new "make switch" combination works on several platforms, and that direct build still works equally well the the "native" OCaml and camlp5 versions on those platforms (ranging from OCaml 4.05 to 5.1).

aqjune commented 4 months ago

Thanks. :)