[isabelle-dev] Grouping ISABELLE_FULL_TEST?

[Florian Haftmann]

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

	Florian

-- 

PGP available:
http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

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