[isabelle-dev] Grouping ISABELLE_FULL_TEST?

[Makarius]

On Mon, 1 Feb 2016, Makarius wrote:

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

I have now done this in Isabelle/705d4c4003ea.

It means that ISABELLE_FULL_TEST no longer occurs in the main Isabelle 
repository. The extra slow sessions are in ~~/src/Benchmarks, and only 
tested by special background jobs that take care of that. (Presently 
none!)

ISABELLE_FULL_TEST still has a purpose in 
AFP/thys/Flyspeck-Tame/ArchComp.thy -- the only occurrence and thus the 
defining position for the intended meaning. It means it could be reformed 
according to what is really required at that point.


 	Makarius