Local installation of Isabelle


The content below is outdated. For instructions on working with the Mercurial repository, please refer to the Isabelle Community Wiki.

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 16 August 2012.