On 14/03/2019 15:30, Manuel Eberl wrote:
> I don't understand what is going on here. I thought I had to set
> ISABELLE_OCAML manually for this kind of code export to even do
> something.
>From the perspective Isabelle/ML, only the presence of settings like
ISABELLE_OCAML or ISABELLE_GHC is decisive.
In the past these had to be provided manually. After Isabelle2018 (and
for the Isabelle2019 release) there will be an (optional) automated way
to get just the right versions of OCaml and GHC, via the admin tools
"isabelle ocaml_setup" and "isabelle ghc_setup".
Here "admin" means: run outside of Isabelle in sequential mode.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
