Email Gateway (Aug 22 2022 at 19:58): Email Gateway (Aug 22 2022 at 19:58):From: Traytel Dmitriy <traytel@inf.ethz.ch>
Hi all,
the above invocation of export_code that tries to compile the generated OCaml code fails (complaining that ISABELLE_OCAMLEXEC is undefined) with a fresh Isabelle2019 installation (after "isabelle ocaml_setup").
This is probably due to the fact that everything now uses the ISABELLE_OCAMLFIND variable, except for src/Tools/Code/code_ml.ML (line 888). (This is not on purpose, right?)
For Isabelle2019 is is enough to define ISABELLE_OCAMLEXEC in ISABELLE_HOME_USER/etc/settings.
Dmitriy
Email Gateway (Aug 22 2022 at 19:59):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Dimitriy,
This is probably due to the fact that everything now uses the
ISABELLE_OCAMLFIND variable, except for src/Tools/Code/code_ml.ML (line
888). (This is not on purpose, right?)
thanks for reporting this. The issue will disappear in the next
Isabelle release.
Cheers,
Florian
signature.asc
Last updated: Apr 27 2024 at 04:17 UTC