>> 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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
