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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
