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