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