[isabelle-dev] Library/List_Prefix

Christian Sternagel c-sterna at jaist.ac.jp
Fri Aug 31 05:25:32 CEST 2012

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_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 ;)



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

More information about the isabelle-dev mailing list