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



This error is strange, and we should be careful not to rule out building
big sessions without really big machines. Btw Collections is of moderate
size, compared to, eg, JinjaThreads. 

Is there any way to measure how "close" a build comes to an
out-of-memory error, to figure out whether something serious happened
between RC2 and RC3, or whether on RC2 the build ran at 99% of available
memory, on on RC3 it happens to be 101%.

--
  Peter

On Di, 2016-02-02 at 18:26 +0100, C. Diekmann wrote:
> Thanks.
> 
> If I build it with "isabelle build -d . -b Collections", I also get
> the "Insufficient memory" error.
> 
> With RC2, the same works fine. I can run the following without any problems:
>   $ISABELLE build -d $AFP -v -b Collections
>   $ISABELLE jedit -d $AFP -l Collections
> 
> It should be possible to build Collections with only 8GB of RAM,
> right? I know that a student used this entry in 2015 with a 4GB RAM
> laptop. Something seems to eat up the RAM in RC3 when finalizing* the
> session image.
> 
> *) I'm just guessing that it happens at finalizing because the
> out-of-memory occurs at the last theory and does not occur if I omit
> the "-b" option.
> 
> Best Regards,
>   Cornelius
> 
> 2016-02-02 17:04 GMT+01:00 Makarius <makarius at sketis.net>:
> > On Tue, 2 Feb 2016, C. Diekmann wrote:
> >
> >> Now I also get the error when I build from the current directory.
> >> ~/Downloads/Isabelle2016-RC3/bin/isabelle jedit -d . -l Collections
> >>
> >> If I build Collections first on the command line
> >>  ~/Downloads/Isabelle2016-RC3/bin/isabelle build -d . -v Collections
> >> the build works.
> >> If I try to load it in jEdit (previous command), it is building
> >> Collections again, but not its dependencies. Shouldn't it load
> >> Collections now without building? The jEdit build fails with the
> >> previously mentioned error.
> >
> >
> > You need to build a session image using "isabelle build -b".
> >
> > That also makes a difference in resource requirements.
> >
> >
> >         Makarius
> >






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