[isabelle-dev] Grouping ISABELLE_FULL_TEST?

[Makarius]

On Sun, 31 Jan 2016, Lars Hupel wrote:

> 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.

I've looked a bit through the sources and the history to infer the 
intended semantics.  The condition ISABELLE_FULL_TEST was introduced to 
guard sessions that are slow and relatively irrelevant for meaningful 
testing, typical "benchmarks".

There are also some exceptional situations like HOL/ex/Sudoko.thy and 
AFP/thys/Flyspeck-Tame/ArchComp.thy, but the special case for Sudoko looks 
irrelevant today, so Flyspeck is just a singularity; it needs special 
treatment anyway.


What remains are various benchmarks.  We could move these sessions to 
~~/src/Benchmarks and omit that directory in ~~/ROOTS.  Thus it can be 
included on demand like this:

   isabelle build -d '~~/src/Benchmarks' -a

or like this:

   isabelle build -D '~~/src/Benchmarks'

This avoids more sophisticated Boolean algebra on session groups.  It also 
makes clear from the source structure, what is normally not tested.

I basically do the same with -d '$AFP' all the time.


Meta-remark: I am presently still on the isabelle-release branch, with 
some modifications of ROOT files that still need to be merged back.  This 
explains my reluctance to make bigger changes right now.


 	Makarius