[isabelle-dev] OCaml 4.06.0 drops nums.cma

[Florian Haftmann]

> 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?

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:
https://caml.inria.fr/pub/docs/manual-ocaml/libref/String.html

Maybe all these issues at a glance justify to modernized OCaml code
generation.

Cheers,
	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20180530/82599197/attachment.sig>