[isabelle-dev] OCaml 4.06.0 drops nums.cma

[Lars Hupel]

I've been trying to figure out why some recent updates broke code
checking (both in the distribution and the AFP) for OCaml. It turns out
that the "nums.cma" module that we rely on for big integer arithmetic
got removed from the standard library.

This problem will affect anyone on rolling releases (e.g.
homebrew on macOS). Recent Ubuntu (18.04) does not appear to be affected.

The old module lives here now: <https://github.com/ocaml/num>

To quote the README:

> This is a legacy library. It used to be part of the core OCaml
> distribution (in otherlibs/num) but is now distributed separately.
> New applications that need arbitrary-precision arithmetic should use
> the Zarith library (https://github.com/ocaml/Zarith) instead of the
> Num library, and older applications that already use Num are
> encouraged to switch to Zarith. Zarith delivers much better
> performance than Num and has a nicer API.

No matter whether we decide to stick with Num or migrate to Zarith, the
code generator needs to be updated to not link against "nums.cma" directly:

  val compile_cmd =
    "\"$ISABELLE_OCAMLC\" -w pu -o " ^ File.bash_path compiled_path ^
    " -I " ^ File.bash_path path ^
    " nums.cma " ^ File.bash_path code_path ^ " " ^ File.bash_path
driver_path
    File.bash_path code_path ^ " " ^ File.bash_path driver_path

This is wrong, because it's not guaranteed where "nums.cma" is. The
recommendation is to use "ocamlfind" instead. "ocamlfind" would be an
extra dependency people would have to install, but a cursory search
reveals that there are system packages for all major Linux
distributions, macOS, and Cygwin.

Any thoughts on how to deal with this?