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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
