[isabelle] Isabelle2016-RC3 -- jEdit build fails when session loaded from different directory



Hi,

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

Collections FAILED
(see also /home/diekmann/.isabelle/Isabelle2016-RC3/heaps/polyml-5.6_x86-linux/log/Collections)

                   Int_of_integer 3072, (),
                   Branch
                    (B, Branch (..., ...), Int_of_integer 3584, ...))),
            Int_of_integer 4096, (),
            Branch
             (B, Branch
                  (B, Branch
                       (B, Branch (..., ...), Int_of_integer 4608, ...),
                   Int_of_integer 5120, (),
                   Branch (B, Branch (..., ...), Int_of_integer 5632, ...)),
              Int_of_integer 6144, (),
              Branch
               (B, Branch (B, Branch (..., ...), Int_of_integer 6656, ...),
                Int_of_integer 7168, (),
                Branch (B, Branch (..., ...), Int_of_integer 7680, ...))))
          ):
   (Isabelle1955749.Generated_Code.inta, unit)
   Isabelle1955749.Generated_Code.rbt
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
times).

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
works fine.

My system has 8GB of RAM, 2 physical cores + hyperthreading, Linux
ubuntu 14.04, unity.

Best Regards,
  Cornelius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.