[isabelle-dev] OCaml 4.06.0 drops nums.cma

Makarius makarius at sketis.net
Fri Mar 22 23:19:48 CET 2019

On 21/03/2019 15:22, Makarius wrote:
> 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.

After all I managed on Windows, see now the "</dev/null" in:

changeset:   69947:dbc2426a600d
user:        wenzelm
date:        Fri Mar 22 18:04:52 2019 +0100
files:       src/HOL/Library/code_test.ML src/Tools/Code/code_ml.ML
workaround for the sake of Windows;

This requires the opam Cygwin package: it will pull in tons of other
things, including another copy of ocaml.

Due to some further rearrangements, we now have a chance to see various
multi-platform tests work again:

Note that I am using "isabelle ocaml_setup" only about 50% of the time:
it is often more convenient to use regular ocamlfind with
libzarith-ocaml (on Ubuntu).


More information about the isabelle-dev mailing list