1 How to install a repository version of Isabelle.
3 The following assumes that you have successfully checked out Isabelle
4 from CVS into a directory $ISABELLE (by default 'isabelle')
6 The directory structure of the repository is different from the
7 distribution. The root directory $ISABELLE is the src
8 subdirectory in the distribution. The 'normal' distribution
9 directories are found in $ISABELLE/Distribution.
11 To work directly on a working copy of the repository, do the following:
13 Change directory to "$ISABELLE/Distribution/bin" and execute:
14 ./isatool install -p ~/bin
16 This will install Isabelle executables in ~/bin. Then issue in
17 directory "$ISABELLE/Distribution"
20 This tells the Isabelle binaries where to find the theories.
22 In $ISABELLE/Distribution/contrib install PolyML and
23 ProofGeneral. Download the corresponding packages from
24 http://isabelle.in.tum.de/dist/ and unpack them in
25 $ISABELLE/Distribution/contrib. If you have already installed them
26 elsewhere, it is sufficient to create a symbolic link in contrib to
27 the main PolyML and ProofGeneral directories. The links should be
28 called 'polyml' and 'ProofGeneral'.
30 Before you can build logic images it is necessary to initialise
31 generation of browser info. Change to the directory
32 "$ISABELLE/Distribution/lib/browser" and issue
35 Java JDK 1.1 or greater needs to be installed for this to work.
37 Now you can build images by going to corresponding folders and issuing:
40 (for instance, in "$ISABELLE/HOL" in order to make HOL). This
41 will create the directory "~/isabelle" (if not already present).
43 After setting up the local copy of Isabelle, changes in the repository
47 (-d causes cvs to create directories that have appeared in the
48 repository since the last update, -P causes directories that have been
49 removed from the repository to be pruned).
51 Internal environment variables
53 $ISABELLE_HOME is the directory "isabelle/Distribution" from above.
54 $ISABELLE_HOME_USER is the directory "~/isabelle".