[isabelle-dev] Grouping ISABELLE_FULL_TEST?
Lars Hupel
hupel at in.tum.de
Sun Jan 31 14:05:50 CET 2016
As of 527488dc8b90, there are five sessions which contain theories that
are only processed under ISABELLE_FULL_TEST=true:
HOL-ex
Sudoku
HOL-Datatype_Examples
Brackin
IsaFoR
Misc_N2M
HOL-Word-SMT_Examples
SMT_Tests
HOL-Quickcheck_Benchmark
Find_Unused_Assms_Examples
Needham_Schroeder_No_Attacker_Example
Needham_Schroeder_Guided_Attacker_Example
Needham_Schroeder_Unguided_Attacker_Example
HOL-Record_Benchmark
Record_Benchmark
Most of these appear to be benchmarks of some sort. Currently, the new
CI setup doesn't set the ISABELLE_FULL_TEST flag. I think it would be
useful to run those, but I'd like to split them up into a separate run
so that they can be executed in parallel to the regular makeall. To that
end, I would suggest grouping these sessions in 'full'. I could then run
export ISABELLE_FULL_TEST=true
isabelle build -v -g full
(In a similar fashion, I run 'slow' sessions separately from the others.)
If nobody complains, I'll add the group.
Cheers
Lars
More information about the isabelle-dev
mailing list