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