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