Support for OCaml 4.14 & Camlp5 8.00 #74
Conversation
|
This is potentially very nice to have, thanks! Are you installing an ocaml 4.14.0 + camlp5 8.00 combination via opam? My opam installation (also on an ARM-based Mac) doesn't seem happy with that combination. |
|
Hi, I was interested in trying your patch, but after running it on my Ubuntu machine I met this mystic error message: Do you have any idea what this error means? |
| else if test ${CAMLP5_VERSION} = "6.06" -o ${CAMLP5_VERSION} = "6.07" -o ${CAMLP5_VERSION} = "6.08" -o ${CAMLP5_VERSION} = "6.09" -o ${CAMLP5_VERSION} = "6.10" -o ${CAMLP5_VERSION} = "6.11" -o ${CAMLP5_VERSION} = "6.12" -o ${CAMLP5_VERSION} = "6.13" -o ${CAMLP5_VERSION} = "6.14" -o ${CAMLP5_VERSION} = "6.15" -o ${CAMLP5_VERSION} = "6.16" -o ${CAMLP5_VERSION} = "6.17" ; \ | ||
| then cp pa_j_3.1x_6.11.ml pa_j.ml; \ | ||
| else cp pa_j_3.1x_${CAMLP5_BINARY_VERSION}.xx.ml pa_j.ml; \ | ||
| else if test ${CAMLP5_BINARY_VERSION} = "8" ; \ |
There was a problem hiding this comment.
Nitpicking: can we use the elif instead of else if? It will eliminate a few fis below as well as linearly increasing indentation. :)
@jrh13 Yes, I used opam.
@aqjune To run it, I use the following ocamlinit (be sure to install ocamlfind): |
|
It worked, thanks! |
|
Thank you! This is a really useful contribution and I've merged it. |
This fixes a crash in loading update_database.ml after jrh13#74. The newly written `update_database.ml` is largely based on @chetmurthy's work: https://github.com/chetmurthy/hol-light/blob/99d017c087ee938929d9d40a5fe75022bbee0257/update_database_6.ml ... with the following modifications to address updates in OCaml's Types module as well as crashes when deprecated stdlib modules are to be loaded: ``` diff --git a/update_database_4.14.ml b/update_database_4.14.ml index 79bc6fc..c2b69d4 100755 --- a/update_database_4.14.ml +++ b/update_database_4.14.ml @@ -17,9 +17,11 @@ open Types (* If the given type is simple return its name, otherwise None. *) let rec get_simple_type = function - | Tlink { desc = Tconstr (Pident p,[],_) } -> Some (Ident.name p) + | Tlink texpr -> + (match get_desc texpr with + | Tconstr (Pident p,[],_) -> Some (Ident.name p) + | d -> get_simple_type d) | Tconstr (Path.Pident p, [], _) -> Some (Ident.name p) - | Tlink { desc = d } -> get_simple_type d | _ -> None;; (* Execute any OCaml expression given as a string. *) @@ -45,15 +47,22 @@ let lid_cons lidopt id = | Some li -> Longident.Ldot(li, id) let it_val_1 lidopt s p vd acc = - if (Some "thm") = Ocaml_typing.get_simple_type vd.Types.val_type.desc then + if (Some "thm") = Ocaml_typing.get_simple_type (get_desc vd.Types.val_type) then (lid_cons lidopt s)::acc else acc let it_mod_1 lidopt s p md acc = (lid_cons lidopt s)::acc let enum0 lidopt = - let vl = Env.fold_values (it_val_1 lidopt) lidopt !Toploop.toplevel_env [] in - let ml = Env.fold_modules (it_mod_1 lidopt) lidopt !Toploop.toplevel_env [] in - (vl, ml) + try + let vl = Env.fold_values (it_val_1 lidopt) lidopt !Toploop.toplevel_env [] in + let ml = Env.fold_modules (it_mod_1 lidopt) lidopt !Toploop.toplevel_env [] in + (vl, ml) + with Not_found -> + (* Looking for (Longident.Lident "Stream") raises Not_found. + Stream is a deprecated alias module of "Stdlib.Stream", and the camlp-streams + package that is used by pa_hol_syntax redefines Stream, which seems to + confuse Env.fold_values and Env.fold_modules. *) + ([], []) let rec enum1 lidopt acc = match enum0 lidopt with ``` I checked that the updated `update_database.ml` works well by testing with the `search` commands that are exhibited at the manual from `help "search"`.
The oldest version of OCaml available on Mac OS with M1 hardware is 4.10.2. This version does not offer a Camlp5 compatible with HOL-Light.
This patch updates
pa_j.mlto support OCaml 4.14 & Camlp5 8.00.I have only tested that
#load "hol.ml";;works; in particular, I have not tested if library code and the other developments shipped with HOL-Light still work.