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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
