[isabelle-dev] OCaml 4.06.0 drops nums.cma

Makarius makarius at sketis.net
Thu Mar 21 15:22:42 CET 2019

On 14/03/2019 19:11, Florian Haftmann wrote:
> Here the current matter of affairs:
> * 0c0f7b4a72bf introduces a dedicated setting for regarding ocamlexec,
> hence there should be no invocations of it if no opam setup is present.
> * 036037573080 takes up the idea that zarith is already part of the
> initial opam bootstrap.

I have refined that further as follows (presently Isabelle/564985d6867e):

  * ISABELLE_OCAMLFIND is the main "user-interface": it is provided
either by opam or by regular "ocamlfind" installed on the system (e.g.
Ubuntu 18.04); the latter then also requires the deb package

  * Update to OPAM 2.0.3: this is the latest version, and the one that
the current Cygwin 3.0.4 provides.

The OPAM update required a few more changes of settings: somehow it
seems that the OPAM guys want to make it hard to use OCaml in such a
generic OS-packageless environment.

Note that there are many implicit dependencies of OPAM, notably
libgmp-dev for zarith. Thus it can be difficult to use "isabelle
ocaml_setup" on macOS. And I did not fully succeed on Windows/Cygwin yet.

My conclusion so far: OPAM may help in our internal administration, but
average users will have difficulties using it themselves. This is in
contrast to Haskell stack: that usually works out-of-the-box, although
that box can be rather big (5-25 GB).


More information about the isabelle-dev mailing list