[isabelle-dev] isabelle build

[Makarius]

On Tue, 7 Aug 2012, David Matthews wrote:

> On 06/08/2012 14:01, Makarius wrote:
>> Just as a teaser, this is what can be done with recent Isabelle + Poly/ML:
>>
>>    Isabelle/90e5093c3e1c
>>    AFP/c7ea6a0ad609
>>    Poly/ML SVN 1569
>> The best runs of JinjaThreads in isolation are:
>> 
>> Finished JinjaThreads (0:20:31 elapsed time, 2:00:34 cpu time, factor
>> 5.87) # 8/8 threads, 16 GB
>> Finished JinjaThreads (0:18:57 elapsed time, 1:58:27 cpu time, factor
>> 6.25) # 8/8 threads, 24 GB
>
> Just to add that JinjaThreads runs quite happily in a relatively small 
> amount of memory with the latest SVN version of Poly/ML.  6-8 Gbytes are 
> fine.  Even in 32-bit mode it takes around 33 minutes.

Indeed, here is another even faster run in 32bit mode:


$ isabelle build -j4 -a -d '$AFP' -v

Started at Tue Aug  7 19:53:48 CEST 2012 (polyml-5.5.0_x86-darwin on lri29-163.lri.fr)
ISABELLE_BUILD_OPTIONS="threads=4 parallel_proofs=2 parallel_proofs_threshold=1000"

ML_PLATFORM="x86-darwin"
ML_HOME="/Volumes/Macintosh_HD/Users/makarius/lib/polyml/polyml-svn/x86-darwin"
ML_SYSTEM="polyml-5.5.0"
ML_OPTIONS="--minheap 500 --gcthreads 4"

Building Pure ...
Running RAW ...
Finished RAW (0:00:00 elapsed time, 0:00:00 cpu time)
Finished Pure (0:00:08 elapsed time, 0:00:08 cpu time, factor 1.00)
Building HOL ...
...
Finished ProgProve (0:00:04 elapsed time, 0:00:06 cpu time)
Timing JinjaThreads (4 threads, 2321.212s elapsed time, 7836.332s cpu time, 2934.999s GC time, factor 0.00)
Finished JinjaThreads (0:38:45 elapsed time, 2:10:38 cpu time, factor 3.37)
Finished at Tue Aug  7 20:39:33 CEST 2012
0:45:45 elapsed time, 8:44:02 cpu time, factor 11.45


Most processes stay in the 1GB range, the formerly bulky JinjaThreads 
stabilizes at comformtable 2.5-3.5 GB.

We have to find new ways to waste memory :-)


 	Makarius