[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