[isabelle] Isabelle2016-RC3 -- jEdit build fails when session loaded from different directory
I'm trying to start RC3 jEdit with Collections pre-loaded. I'm using
afp-devel 138306721319. I also tried it with a less recent version
which worked on RC2.
For a fresh start, I deleted my .isabelle/Isabelle-2016-RC3 directory.
I started Isabelle from the afp-devel toplevel with
~/Downloads/Isabelle2016-RC3/bin/isabelle jedit -d thys/ -l Collections
It starts building everything, starting from session HOL in the jEdit window.
At some point (Collections), the build just fails. These are the last
parts of the output:
Collections: theory Refine_Monadic_Userguide
(see also /home/diekmann/.isabelle/Isabelle2016-RC3/heaps/polyml-5.6_x86-linux/log/Collections)
Int_of_integer 3072, (),
(B, Branch (..., ...), Int_of_integer 3584, ...))),
Int_of_integer 4096, (),
(B, Branch (..., ...), Int_of_integer 4608, ...),
Int_of_integer 5120, (),
Branch (B, Branch (..., ...), Int_of_integer 5632, ...)),
Int_of_integer 6144, (),
(B, Branch (B, Branch (..., ...), Int_of_integer 6656, ...),
Int_of_integer 7168, (),
Branch (B, Branch (..., ...), Int_of_integer 7680, ...))))
val it = (): unit
ML> Exception- Fail "Insufficient memory" raised
Unfinished session(s): Collections
Return code: 1
Session build failed -- prover process remains inactive!
When the build is at "Collections: theory Refine_Monadic_Userguide",
at most 5.8GB RAM of 7.8GB RAM are used on my system (tested three
However, when I cd to thys and start isabelle with
~/Downloads/Isabelle2016-RC3/bin/isabelle jedit -d . -l Collections
it works fine.
I could reproduce this several times (3 tests each, always the same
behavior). It does not look like a _random_ memory shortage to me. The
whole thing worked fine with the previous RCs.
This behavior does not occur with the command line build. I.e.
~/Downloads/Isabelle2016-RC3/bin/isabelle build -d thys -v Collections
My system has 8GB of RAM, 2 physical cores + hyperthreading, Linux
ubuntu 14.04, unity.
This archive was generated by a fusion of
Pipermail (Mailman edition) and