[isabelle-dev] OCaml 4.06.0 drops nums.cma

[Lars Hupel]

> 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.

That sounds reasonable. What is the reason for placing "opam" under
"$ISABELLE_HOME_USER" (by default), though? I don't see a reason why
this couldn't be shared with an existing installation.

Would it be possible to specify the concrete compiler as a system
option? The big benefit there is that it would decrease maintenance
burden: session authors could select their "ocamlc" version in "options
[...]". It means people who have custom OCaml code printing (like Simon)
don't have to care about a hard-coded "4.05.0" somewhere; they'll get a
consistent setup regardless.