[isabelle-dev] OCaml 4.06.0 drops nums.cma
hupel at in.tum.de
Wed May 30 11:15:09 CEST 2018
> 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
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.
More information about the isabelle-dev