[isabelle-dev] Working with more than one local repository of Isabelle and AFP

[Florian Haftmann]

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
and testing.

--

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
that.

2. repositories

Each Isabelle repository resides in

  $DATA_ROOT/isabelle/$WORKING_DIR

where $WORKING_DIR is an arbitrary name, e.g.

  $DATA_ROOT/isabelle/master
  $DATA_ROOT/isabelle/devel

Similar for AFP.

  $DATA_ROOT/afp/$WORKING_DIR
  $DATA_ROOT/afp/master
  $DATA_ROOT/afp/devel

There is no need that for a one-to-one correspondences between Isabelle
and AFP.

3. provide contrib directory

Each Isabelle repository needs a proper »contrib« directory.  This can
be achieved easily by

  cd $DATA_ROOT/isabelle/$WORKING_DIR
  mkdir contrib
  cd contrib
  for NAME in $PATH_TO_CONTRIB_OF_LAST_ISABELLE_RELEASE/*; do ln -s
$NAME; done

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:

  cd $DATA_ROOT/isabelle/$WORKING_DIR
  mkdir contrib
  ln -s $PATH_TO_CORRESPONDING_AFP_REPOSITORY

4. Adjust ~/.isabelle/etc/settings

  # store sessions results in working directory
  if [ -z "$ISABELLE_IDENTIFIER" ]
  then
    ISABELLE_OUTPUT="$ISABELLE_HOME/heaps"
    ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info"
  fi

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" ]
  then
    init_component "$ISABELLE_HOME/contrib/afp"
  fi

This links AFP as a component (as specified in $ISABELLE_HOME/contrib by
a symlink).

See the system manual for further details.

--

I hope this is useful for everybody heavy on testing and refactoring.

Comment welcome.

    Florian
-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20110831/f394b229/attachment.asc>