[isabelle-dev] Grouping ISABELLE_FULL_TEST?

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Tue Feb 2 21:55:58 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.

I also like that.

FYI in my test setup there is currently a particular isabelle tool with
the following content:

> #!/usr/bin/env bash
> #
> # DESCRIPTION: pragmatic combined build of distribution and afp
> ISABELLE_FULL_TEST=true "${ISABELLE_TOOL}" build -d "${AFP}" -x Flyspeck-Tame "$@"
> ISABELLE_FULL_TEST= "${ISABELLE_TOOL}" build -d "${AFP}" Flyspeck-Tame

Maybe that distinction could also be tackled by an appropriate session
structure and / or grouping.



PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20160202/a6a9be10/attachment.sig>

More information about the isabelle-dev mailing list