[isabelle-dev] Library/List_Prefix

[Christian Sternagel]

Well, it almost worked now ;).

even without -b all my memory was wasted and just as swapping started in 
earnest I got an error message, i.e., I have to adapt JinjaThreads to 
some previous changes.

Still, I am nowhere close to the 3-4 GB RAM usage that seem to be 
possible. Maybe the reason is that I'm on x86_64?

My settings are:

   ISABELLE_BUILD_OPTIONS="threads=4 parallel_proofs=2"

   ML_PLATFORM="x86_64-linux"
   ML_HOME="/home/griff/Repos/polyml/"
   ML_SYSTEM="polyml-5.5.0"
   ML_OPTIONS="--minheap 1000"

Side remark: since I now have to adapt at least TypeComp in JinjaThreads 
I started that theory up in jEdit and noticed that the ProverSession 
panel does not adapt to huge inputs (i.e., no scroll-bars are added. And 
for TypeComp the list of dependencies is already quite long ;)

cheers

chris


On 08/30/2012 11:12 PM, Makarius wrote:
> On Thu, 30 Aug 2012, Christian Sternagel wrote:
>
>> I could however not test JinjaThreads, since even with poly 5.5.0, 4
>> cores and 8GB RAM my computer flat-lined a few minutes after 'isabelle
>> build -d . -b JinjaThreads' with ISABELLE_BUILD_OPTIONS="threads=4
>> parallel_proofs=2". It would be much appreciated if somebody with
>> access to a more powerful computer could adapt JinjaThreads.
>
> It should work comfortably like this:
>
>     ISABELLE_BUILD_OPTIONS="threads=4 parallel_proofs=2"
>
>     ML_PLATFORM="x86-linux"
>     ML_HOME="/home/polyml/polyml-svn/x86-linux"
>     ML_SYSTEM="polyml-5.5.0"
>     ML_OPTIONS="-H 1000"
>
> Resulting in a runtime of JinjaThreads in the range of 20..40min.  You
> don't need to build an image for it (-b).
>
>
>      Makarius