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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev