[isabelle-dev] OCaml 4.06.0 drops nums.cma

[Lars Hupel]

> 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