[isabelle-dev] isabelle build

[Makarius]

Just as a teaser, this is what can be done with recent Isabelle + Poly/ML:

   Isabelle/90e5093c3e1c
   AFP/c7ea6a0ad609
   Poly/ML SVN 1569

$ isabelle build -j4 -d '$AFP' -a -v
Started at Mon Aug  6 13:52:46 CEST 2012 (polyml-5.5.0_x86_64-darwin on lri29-163.lri.fr)

ISABELLE_BUILD_OPTIONS="threads=4 parallel_proofs=2 parallel_proofs_threshold=1000"

ML_PLATFORM="x86_64-darwin"
ML_HOME="/Volumes/Macintosh_HD/Users/makarius/lib/polyml/polyml-svn/x86_64-darwin"
ML_SYSTEM="polyml-5.5.0"
ML_OPTIONS="--minheap 1000 --maxheap 16000 --gcthreads 4"

...
Building HOL ...
Building ZF ...
Building HOL-Proofs ...
Building CCL ...
...
Finished Main (0:00:03 elapsed time, 0:00:02 cpu time)
Timing ProgProve (4 threads, 2.409s elapsed time, 7.835s cpu time, 0.355s GC time, factor 3.25)
Document sources at /Volumes/Macintosh_HD/Users/makarius/isabelle/repos/doc-src/ProgProve/Thys/document
Finished ProgProve (0:00:04 elapsed time, 0:00:09 cpu time)
Timing JinjaThreads (4 threads, 2611.483s elapsed time, 9315.763s cpu time, 2312.681s GC time, factor 3.57)
Finished JinjaThreads (0:43:36 elapsed time, 2:35:19 cpu time, factor 3.56)
Finished at Mon Aug  6 14:46:12 CEST 2012
0:53:26 elapsed time, 10:22:00 cpu time, factor 11.64

This means all of Isabelle (including doc-src) + AFP + AFP_big sessions in 
53min elapsed time, on a machine with "only" 8 cores and 32 GB.


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


Special wizardry was performed by David Matthews in the Poly/ML runtime 
system in the past 12 months.


 	Makarius