[isabelle-dev] Grouping ISABELLE_FULL_TEST?

Makarius makarius at sketis.net
Sat Feb 13 12:31:18 CET 2016

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 

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.


More information about the isabelle-dev mailing list