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



Have you used 64bit poly? What happens on 32bit poly?


-------- Originalnachricht --------
Betreff: Re: [isabelle] Isabelle2016-RC3 -- jEdit build fails when session loaded from different directory
Von: "C. Diekmann"
An: Peter Lammich
Cc: isabelle-users ,Makarius Wenzel


2016-02-02 18:45 GMT+01:00 Peter Lammich :
> This error is strange, and we should be careful not to rule out building
> big sessions without really big machines.

I agree. My office laptop has 8GB of RAM. It would be really hard if
this is not enough for Isabelle. Students often have laptops with less
RAM.

This thread should be called: Isabelle2016 uses too much RAM.

For the way I (personally) use Isabelle, this would be release-critical.


I started buying big machines after I got familiar with Isabelle. I
was a happy intel atom 1GM RAM user before that. But Isabelle was
working okay in 2012 on that device. I understand that these times are
long gone. But requiring more that a common, up-to-date, medium-class,
off-the-shelf laptop to run Isabelle will make it really hard to get
new users or to use Isabelle in a lecture.


> Btw Collections is of moderate
> size, compared to, eg, JinjaThreads.


If Collections is medium-sized, does this mean this theory can
determine the minimum amount of RAM necessary to do something useful
with Isabelle? Should this information be on the website?


> 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%.

I booted my machine with only 6BG of ram (kernel option) and now the
build also fails at the same position with RC2.

Isabelle 2015 (with my 2015 snapshot of the afp, which makes the whole
measurement not comparable) can build Collection on 6GB RAM. But there
was a moment where it "felt like" I almost ran out of RAM.

Cornelius


> 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 :
>> > 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.