|
14583
|
1 |
How to install a repository version of Isabelle.
|
|
|
2 |
|
|
|
3 |
The following assumes that you have successfully checked out Isabelle
|
|
|
4 |
from CVS into a directory $ISABELLE (by default 'isabelle')
|
|
|
5 |
|
|
|
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.
|
|
|
10 |
|
|
|
11 |
To work directly on a working copy of the repository, do the following:
|
|
|
12 |
|
|
|
13 |
Change directory to "$ISABELLE/Distribution/bin" and execute:
|
|
|
14 |
./isatool install -p ~/bin
|
|
|
15 |
|
|
|
16 |
This will install Isabelle executables in ~/bin. Then issue in
|
|
|
17 |
directory "$ISABELLE/Distribution"
|
|
|
18 |
ln -s .. src
|
|
|
19 |
|
|
|
20 |
This tells the Isabelle binaries where to find the theories.
|
|
|
21 |
|
|
14585
|
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'.
|
|
14583
|
29 |
|
|
|
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
|
|
|
33 |
make
|
|
|
34 |
|
|
|
35 |
Java JDK 1.1 or greater needs to be installed for this to work.
|
|
|
36 |
|
|
|
37 |
Now you can build images by going to corresponding folders and issuing:
|
|
|
38 |
isatool make
|
|
|
39 |
|
|
|
40 |
(for instance, in "$ISABELLE/HOL" in order to make HOL). This
|
|
|
41 |
will create the directory "~/isabelle" (if not already present).
|
|
|
42 |
|
|
|
43 |
After setting up the local copy of Isabelle, changes in the repository
|
|
|
44 |
can be imported by:
|
|
|
45 |
cvs update -d -P
|
|
|
46 |
|
|
|
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).
|
|
|
50 |
|
|
|
51 |
Internal environment variables
|
|
|
52 |
|
|
|
53 |
$ISABELLE_HOME is the directory "isabelle/Distribution" from above.
|
|
|
54 |
$ISABELLE_HOME_USER is the directory "~/isabelle".
|
|
|
55 |
|
|
|
56 |
|
|
14584
|
57 |
$Id$
|