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 firstname.lastname@example.org:/usr/proj/isabelle-repository/archive co isabelleThis creates the directory "isabelle" (if not already present). Change directory to "isabelle/Distribution/bin" and execute:
./isatool install -p ~/binThis will install Isabelle executables in ~/bin. Then issue in directory "isabelle/Distribution"
ln -s .. srcand
ln -s /usr/proj/isabelle/ contribThe 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
makeNow 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).
|$ISABELLE_HOME||is the directory "isabelle/Distribution" from above.|
|$ISABELLE_HOME_USER||is the directory "~/isabelle".|
ISABELLE_OUTPUT="$ISABELLE_HOME/heaps"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.