[isabelle-dev] OCaml 4.06.0 drops nums.cma

[Makarius]

On 30/05/18 11:15, Lars Hupel wrote:
>> 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 have now experimented a bit with opam-1.2.2 on Linux, Mac OS X,
Windows/Cygwin64. It appears to work quite well, e.g. like this:

  ./opam-1.2.2-x86_64-Darwin init --root ~/.isabelle/opam --comp 4.05.0

The opam executables only require a few MB. The result in
~/.isabelle/opam above is 340 MB, for ocaml and ocamlc. This is a fair
investment to evade the "dynamic version hell", and normal Isabelle
users won't have to see it.

So we could provide "isabelle opam" as wrapper for something like "opam
--root $ISABELLE_OPAM_HOME/$ISABELLE_PLATFORM64" as well as "isabelle
opam_init" for the specific compiler version setup. Our component wiring
would also provide ISABELLE_OCAML and ISABELLE_OCAMLC settings for the
result.


There might be further consequences of such a move: the opam universe
provides packages for alt-ergo, coq, why3, which are potentially useful
tools to be integrated with Isabelle eventually.


	Makarius