Building AFP

This entry summarizes and explains how to build AFP with the new build system introduced in Isabelle 2012 post-release mode.

The Long Story: original explanation by Makarius

This explanation comes from this email:

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.

The Short Story: for busy people

• AFP has to be registed as a component in Isabelle. This can be achieved in different ways. The most common approach is to add the following line to ~/.isabelle/etc/settings:

init_component "path_to_AFP"

• It's quite handy to supply parameters -nv to the build tool. The effect is that names of sessions which are going to be built are printed but nothing is actually built.
  • It's useful if one is not sure about the effect of the command.

> isabelle build -nv HOL
Session Pure
Session HOL (main)
0:00:25 elapsed time, 0:02:40 cpu time, factor 6.40

• The following command builds all sessions from AFP and all sessions from Isabelle:

isabelle build -d '$AFP' -a

• The following command builds only specified sessions (in our example BDD and Refine_Monadic) from AFP (and of course their dependencies):

isabelle build -d '$AFP' BDD Refine_Monadic

• Another approach is to use afp_build tool. The following builds all sessions from AFP:
  • It's useful if one wants to build only AFP sessions but not necessarily all Isabelle sessions. Compare with isabelle build -d '$AFP' -a

isabelle afp_build -A

• Or specific ones:

isabelle afp_build BDD Refine_Monadic

• Additional parameters to the underlying build tool (like a maximum number of parallel jobs) can be provided after -- symbol:

isabelle afp_build BDD Refine_Monadic -- -j2