[isabelle-dev] NEWS

[Makarius]

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