[isabelle-dev] Build NEWS
Makarius
makarius at sketis.net
Sun Apr 17 15:55:09 CEST 2016
On Sat, 16 Apr 2016, Lars Hupel wrote:
> * I have eliminated the last occurrence of ISABELLE_FULL_TEST in the
> known Isabelle universe. Flyspeck_Tame used it to determine whether
> full computations should be carried out. It does that now by default,
> which takes about 7 hours (!) on a regular machine. I have also tagged
> this session with "slow" (like the other huge sessions). If you want
> to test the AFP locally without provoking the heat death of your
> machine, I recommend building with "-X slow".
Maybe this can be simplified further. The "slow" group in the main
Isabelle repository is now rather pointless, even counterproductive.
HOL-Proofs and its subsessions has become relatively fast compared to
other bulky sessions.
E.g. Isabelle/65f279853449 on 12 cores with 6 threads per ML process:
build -j4 -a
0:27:21 elapsed time, 7:13:18 cpu time, factor 15.84
build -j4 -a -X slow
0:23:53 elapsed time, 6:02:21 cpu time, factor 15.17
build -j4 -g slow
0:12:23 elapsed time, 0:57:07 cpu time, factor 4.61
Makarius
More information about the isabelle-dev
mailing list