[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