[isabelle-dev] OCaml 4.06.0 drops nums.cma
florian.haftmann at informatik.tu-muenchen.de
Wed May 30 10:15:35 CEST 2018
> 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
> 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?
The best way maybe is to introduce a dedicated isabelle tool »ocamlc«
which uses an environment parameter ISABELLE_OCAML as path prefix to
ocamlc / ocamlfind; this would be more pleasant than any kind of ad-hoc
montage in ML.
Btw. Zarith is available at least since Ubuntu 16.04. as package
libzarith-ocaml. It is anyway still unsatisfactory that such a
fundamental concept as proper integers does not work out-of-the-box
But there is now a possibility to have proper strings:
Maybe all these issues at a glance justify to modernized OCaml code
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 819 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev