[isabelle-dev] OCaml 4.06.0 drops nums.cma

[Makarius]

On 06/06/18 11:39, Lars Hupel wrote:
>> 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.

I've misunderstood the "opam init --comp" procedure, with its tendency
towards a single version. With "opam switch install" it is possible to
install arbitrary (disjoint) versions, so indeed we can reuse the
central ~/.opam root (with the minor disadvantage that it appears to
assume just one OS platform, i.e. the HOME cannot be shared among
platforms).


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

In practice "their" version means a version in distant past that was the
current one when the author was working on the session.

I was more thinking of one standard OCaml version for a particular
Isabelle version, which could be just ISABELLE_OCAML_VERSION in
etc/settings. Multiple Isabelle versions can take this from a central
~/.opam store to produce ISABELLE_OCAML and ISABELLE_OCAMLC, but within
each Isabelle version it should be a constant, not a variable.

This conforms with the idea of Isabelle components: we include one fixed
version for each tool, such that everything fits nicely together.


	Makarius