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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
