[isabelle-dev] NEWS

[Makarius]

On 13/03/2019 21:12, Makarius wrote:
> 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.

This requirement of statelessness also applies to the etc/settings shell
scripts in the Isabelle components hierarchy. We have recently had
tendencies to postulate automated build or download features here, but
this is not going to work. There can be many simultaneous invocations of
these scripts, and we cannot afford races, long-running operations, or
spurious failures.


Here is an example where I have amended such a mistake of mine,
concerning Haskell stack:
http://isabelle.in.tum.de/repos/isabelle/rev/c911716d29bb -- before
there were spurious "stack" operations to access its stackage repository
in uncontrolled ways.

I've forgotten to apply the analogous change to the Isabelle/Naproche
project (to be found on Github): it has already caused a lot of problems
just with 2 developers and 3 users trying it out at Uni Bonn.

I will have to revise "isabelle ghc_setup" further, to leave more
accurate information in its installation directory (about
platform-specific paths to ghc). Thus etc/settings can refer to that
robustly and portably (note that even just different Linux installations
may lead to different ghc installation names; of course it also needs to
work with Windows and macOS on the same shared stack installation).


Compared to that, "isabelle opam" is still lagging behing in various
respects. I have myself no experience with the underlying opam tool, and
it is also the old version 1.2.2 (which was imposed by Cygwin some
months ago).


	Makarius