Building AFP

From Isabelle Community Wiki
Jump to navigation Jump to search

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

    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