[isabelle-dev] Grouping ISABELLE_FULL_TEST?
makarius at sketis.net
Mon Feb 1 16:29:15 CET 2016
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:
> 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
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.
More information about the isabelle-dev