[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