From Isabelle Community Wiki
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:
- 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