Local installation of Isabelle

How to install a repository version of Isabelle.

Set the CVS_RSH environment variable to ssh:

   export CVS_RSH=ssh  (or setenv CVS_RSH ssh)

Change to the directory where the Isabelle sources are to be installed. Check out Isabelle sources:

   cvs -d username@cvsbroy.informatik.tu-muenchen.de:/usr/proj/isabelle-repository/archive co isabelle

This creates the directory "isabelle" (if not already present). Change directory to "isabelle/Distribution/bin" and execute:

   ./isatool install -p ~/bin

This will install Isabelle executables in ~/bin. Then issue in directory "isabelle/Distribution"

   ln -s .. src

and

   ln -s /usr/proj/isabelle/ contrib

The latter links the directory where Proof General and other utilities are installed. On local machines (*broy.in.tum.de) this is "/usr/proj/isabelle/". Before making the wanted logics it is necessary to initialise generation of browser info. Change to the directory "isabelle/Distribution/lib/browser" and issue

   make

Now you can make the wanted theories by going to corresponding folders and issuing:

   isatool make

(for instance, in "isabelle/HOL" in order to make HOL). This will create the directory "~/isabelle" (if not already present).

After setting up the local copy of Isabelle, changes in the repository can be imported by:

   cvs update -d -P

(-d causes cvs to create directories that have appeared in the repository since the last update, -P causes directories that have been removed from the repository to be pruned).

Internal environment variables

$ISABELLE_HOME	is the directory "isabelle/Distribution" from above.
$ISABELLE_HOME_USER	is the directory "~/isabelle".

Maintaining several working versions

Information on built theories is stored in subdirectories of $ISABELLE_HOME_USER. In particular, "heaps" contains heap images, and "browser_info" is where proof documents are stored. The location of these directories is fixed, not relative to your working copy of the repository. This is inconvenient if you want serveral working copies at the same time. By setting

   ISABELLE_OUTPUT="$ISABELLE_HOME/heaps"
   ISABELLE_BROWSER_INFO="$ISABELLE_HOME/browser_info"

in your ~/isabelle/etc/settings file, "isatool make" is instructed to put the "heaps" and "browser_info" directories in $ISABELLE_HOME instead. The corresponding executables are found in $ISABELLE_HOME/bin.

Last updated 7 March 2008.