[isabelle-dev] Working with more than one local repository of Isabelle and AFP
florian.haftmann at informatik.tu-muenchen.de
Wed Aug 31 22:03:27 CEST 2011
I give here a write-up of my Isabelle repository infrastructure, which
exploits the concept of Isabelle components to get a neat and flexible
integration of multiple instances of Isabelle and AFP for development
1. directory strucure
I'll assume you place your work relative to a $DATA_ROOT; some people
may prefer ~/ or ~/work or ~/data or (on single-user machines) /data for
Each Isabelle repository resides in
where $WORKING_DIR is an arbitrary name, e.g.
Similar for AFP.
There is no need that for a one-to-one correspondences between Isabelle
3. provide contrib directory
Each Isabelle repository needs a proper »contrib« directory. This can
be achieved easily by
for NAME in $PATH_TO_CONTRIB_OF_LAST_ISABELLE_RELEASE/*; do ln -s
If needed, single contribs can be added or replaced by adding or
tweaking symlinks appropriately, e.g. for testing new versions of polyml.
Then the association to a corresponding AFP repository:
ln -s $PATH_TO_CORRESPONDING_AFP_REPOSITORY
4. Adjust ~/.isabelle/etc/settings
# store sessions results in working directory
if [ -z "$ISABELLE_IDENTIFIER" ]
For proper releases, ISABELLE_IDENTIFIER is non-zero; the check prevents
that regular Isabelle releases on your machine will modify themselves.
If you choose ISABELLE_OUTPUT as above, you need not adjust
ISABELLE_PATH because it contains $ISABELLE_HOME/heaps already.
# treat afp as component
if [ -d "$ISABELLE_HOME/contrib/afp" ]
This links AFP as a component (as specified in $ISABELLE_HOME/contrib by
See the system manual for further details.
I hope this is useful for everybody heavy on testing and refactoring.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev