[isabelle-dev] AFP build

[Makarius]

(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