[isabelle-dev] Purpose of additional HOL images

Makarius makarius at sketis.net
Mon Jan 7 13:06:49 CET 2013


This is a left-over from the isabelle build reform from last summer: Do 
the additional HOL images still have a purpose?  Notably:

   HOL-Base
   HOL-Plain
   HOL-Main

If it is just for experimentation, these session can be easily provided by 
1 line each in $ISABELLE_HOME_USER/ROOT


Here is the timing I get for "isabelle build -j4 -a" on 8 cores (approx. 
Isabelle/c96bb430ddb0):

0:16:11 elapsed time, 3:09:42 cpu time, factor 11.72 -- with
0:15:53 elapsed time, 3:03:34 cpu time, factor 11.55 -- without

That is clearly noticeable.  Having more images in parallel to main HOL 
and HOL-Proofs also sucks up CPU cycles that are needed for the initial 
start.  The main HOL image alone requires << 2min.


 	Makarius


More information about the isabelle-dev mailing list