> The best way maybe is to introduce a dedicated isabelle tool »ocamlc« > which uses an environment parameter ISABELLE_OCAML as path prefix to > ocamlc / ocamlfind; this would be more pleasant than any kind of ad-hoc > montage in ML.
Yes, but we would still need to figure out how to "peg" a particular OCaml version. As far as I understand there is now way to make this change that will work for both 4.06+ and before. Maybe we could bundle OPAM, which is a tool that is able to download and install a particular OCaml version on all the platforms that Isabelle also supports. I'm mentioning this because I'm going to have to do a similar thing anyway (eventually!) in order to ensure a consistent installed version of OCaml on all the various testing machines. The reason I found this out was that Homebrew gave me an upgrade to 4.06 which broke it, but Ubuntu 18.04 LTS is still on 4.05. > Btw. Zarith is available at least since Ubuntu 16.04. as package > libzarith-ocaml. It is anyway still unsatisfactory that such a > fundamental concept as proper integers does not work out-of-the-box It might be worth looking at HOL Light to see how they do it. Cheers Lars _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
