[isabelle-dev] NEWS: support for OCaml / OPAM

Makarius makarius at sketis.net
Mon Oct 8 16:37:06 CEST 2018

*** System ***

* Support for OCaml via command-line tools "isabelle ocaml_setup",
"isabelle ocaml", "isabelle ocamlc", "isabelle ocaml_opam". Existing
settings variables ISABELLE_OCAML and ISABELLE_OCAMLC are maintained
dynamically according the state of ISABELLE_OPAM_ROOT concerning

This refers to Isabelle/be20f5f6feb9. It is the result of 2 rounds of
refinements over https://github.com/larsrh/isabelle-opam

Note that I've used the old opam-1.2.2 for the sake of Cygwin: it
presently provides that version only, no 2.0 yet.

Bundling the Cygwin opam package with Isabelle did not work out: it
requires tons of other things, including Python, Mercurial, even OCaml
itself. For the moment, users of "isabelle ocaml_setup" need to install
Cygwin opam with the Cygwin setup tool manually.

In any case, an explicit "isabelle ocaml_setup" is required: the user
needs to decide to venture on this enterprise -- opam uses non-standard
things like "make" and may fail in odd ways. When the setup has
succeeded, ISABELLE_OCAML and ISABELLE_OCAMLC are magically provided and
meant to be stable.

At the moment we have ISABELLE_OCAML_VERSION="4.05.0" and
"$ISABELLE_OCAML" nums.cma works outright as before.

There are still some open questions:

  * How to re-init the opam installation, e.g. after changing
    (Presently I have just removed purged ISABELLE_OPAM_ROOT.)

  * Is the update of ~/.ocamlinit that is proposed by opam init required?

  * How to work with add-on OCaml libraries?

  * Update of Cygwin (or native Windows) version to opam 2.0 when/if
that becomes available.


More information about the isabelle-dev mailing list