[isabelle-dev] Grouping ISABELLE_FULL_TEST?

Lars Hupel hupel at in.tum.de
Tue Feb 2 14:28:52 CET 2016


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

Sounds reasonable. There's no pressure to do it just yet; I'd be happy
to wait for post-release mode.

Cheers
Lars



More information about the isabelle-dev mailing list