(This is a fresh thread just for AFP build management.
Alex should probably also start another thread just for Mira, once he has
something there.
I will answer pending questions about isabelle build on their respective
threads later.)
First the summary of the situation in Isabelle/875a4657523e and
AFP/0453dd9dc01c:
* AFP as component provides settings $AFP_BASE and AFP="$AFP_BASE/thys"
as before. These will be turned into some use below.
* Each subdirectory in $AFP defines a session with its own ROOT, which
may refer to to parent session within AFP, although that is still
rare. This introduces a rather flat dependency relation between the
directories. AFP sessions that build on other AFP sessions are just
emerging.
Users who are interested in a few AFP sessions can include these
directories into the session name space manually like this:
isabelle build -d '$AFP/Simpl' -d '$AFP/BDD' -nv BDD
Command line options -d can be imagined as Prover IDE configuration at
some point, i.e. clicking on some checkbox to include it.
Note that -d '$AFP' works because the quoting prevents bash from
expanding the variable, but leaves it to Isabelle Path.explode/expand
later in Isabelle/Scala/ML.
* The collection of all subdirectry ROOT files is concatenated to just
one $AFP/ROOT which provides access to the whole name space like this:
isabelle build -d '$AFP' -nv -a
This is particularly useful for administration. Users can also
include the full name space and then select particular sessions:
isabelle build -d '$AFP' -nv BDD Refine_Monadic
Dependencies are already resolved by including the $AFP root.
* The isabelle afp_mkroot tool maintains the relation of the many ROOT
files with the central ROOT.
* The isabelle afp_build tool provides another abstraction specific for
AFP test builds. It emulates the old admin/testall to some extent.
* Neither $AFP/ROOT nor the individual $AFP/*/ROOT are active by the
default configuration of the AFP component. This is motivated by the
need for typical administrative tasks. Otherwise the build -a option
would become useless, or one would have to manage more session groups.
I also wanted to econimize size of terminal output in the normal
operation of Isabelle testing, without AFP.
I was occasionally tempted to introduce some kind of "query language" for
session selection, with inclusion or exclusion of individual sessions or
session groups. I've avoided that so far, because bash command line is
not for doing logic.
Note that sophisticated selections can be specified in Scala add-on tools
for isabelle.Build, say for the coming Wikipedia for Formal Proofs, once
there are sufficiently many users to run the experiment, as Larry said.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
