On 13/03/2019 21:00, Florian Haftmann wrote:
> Am 13.03.19 um 20:57 schrieb Lars Hupel:
>>> isabelle ocaml_opam install zarith
>>
>> This should ideally happen on-the-fly from within Isabelle/ML.
>
> Or maybe as implicit part of
>
> isabelle ocaml_setup
Note that any change of the physical environment needs to happen in
administrative tools like "isabelle ocaml_setup": there is an implicit
assumption that there is only one administrator doing one thing at a
time. (E.g. in "isabelle build" and its physical update of heap and db
files.)
In contrast, the parallel Isabelle/ML world cannot write to the global
file-system, without causing big problems. We have pending issues with
AFP entries that violate this principle: maybe we manage to put it all
into shape for the Isabelle2019 release, using stateless operations from
Export/Generated_Files in ML for the 'codegen' command in particular.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
