[isabelle-dev] Grouping ISABELLE_FULL_TEST?
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