Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle (benchmark)
On 13/03/2019 21:06, Lars Hupel wrote: >> "Unable to increase stack" is one of the various messages that tells >> you that PolyML has run out of resources. It doesn't really tell you >> what the problem is though. It might be an actual problem or a >> temporary problem caused by a machine being overloaded. > > This is likely connected to the recent change of platform. I will > investigate this; maybe bumping the memory limit will resolve it. BTW, with Poly/ML 5.8 being official, you can avoid full x86_64 for most applications and always use the default x86_64_32. This saves a lot of resources: I usually have ML_OPTIONS="--minheap 1500" with an open upper end -- the implicit limit is approx. 16G. Even some entries of the slow/large groups of AFP work well with x86_64_32, but I usually throw them into on big x86_64 pot as a special case. Another remaining application of full x86_64 is the huge PIDE session forked by "isabelle dump" and related tools: it can require 64GB (excluding slow), and I have not explored the upper end yet. Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS
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
Re: [isabelle-dev] NEWS
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
Re: [isabelle-dev] Fwd: [Isabelle-ci] Build failure in Isabelle (benchmark)
"Unable to increase stack" is one of the various messages that tells you that PolyML has run out of resources. It doesn't really tell you what the problem is though. It might be an actual problem or a temporary problem caused by a machine being overloaded. This is likely connected to the recent change of platform. I will investigate this; maybe bumping the memory limit will resolve it. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS
Or maybe as implicit part of isabelle ocaml_setup Sure, that could also work. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS
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 ? Florian signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] NEWS
isabelle ocaml_opam install zarith This should ideally happen on-the-fly from within Isabelle/ML. Cheers Lars ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] OCaml 4.06.0 drops nums.cma
Are there any issues remaining on this thread after http://isabelle.in.tum.de/repos/isabelle/rev/55534affe445 ? Cheers, Florian Am 24.06.18 um 22:29 schrieb Makarius: > On 07/06/18 15:22, Lars Hupel wrote: >>> Does this minimal approach make any sense, and solve the imminent >>> administrative problems? In particular without a decision yet about >>> ISABELLE_OCAML_VERSION vs. ISABELLE_OCAML / ISABELLE_OCAMLC? >> >> I tend to agree. Let's fix OCaml to 4.05.0 and we can figure out a good >> way to upgrade after the release. > > (This thread is still open.) > > I presently tend to postpone the question if/how to support OCaml after > the Isabelle2018. > > > Makarius > > ___ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev > signature.asc Description: OpenPGP digital signature ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
