author | wenzelm |
Thu, 16 Oct 2008 22:44:24 +0200 | |
changeset 28615 | 4c8fa015ec7f |
parent 28504 | 7ad7d7d6df47 |
permissions | -rw-r--r-- |
27461 | 1 |
How to install a CVS repository version of Isabelle. |
14583 | 2 |
|
3 |
The following assumes that you have successfully checked out Isabelle |
|
4 |
from CVS into a directory $ISABELLE (by default 'isabelle') |
|
5 |
||
27461 | 6 |
The directory structure of the CVS is different from the |
14583 | 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: |
|
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
27630
diff
changeset
|
14 |
./isabelle install -p ~/bin |
14583 | 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 |
||
27461 | 22 |
In $ISABELLE/Distribution/contrib install Poly/ML and |
23 |
Proof General. Download the corresponding packages from |
|
14585 | 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 |
|
27461 | 27 |
the main Poly/ML and ProofGeneral directories. The links should be |
14585 | 28 |
called 'polyml' and 'ProofGeneral'. |
14583 | 29 |
|
27461 | 30 |
Building logic images with browser info generation (which is the |
31 |
default setting) requires a compiled version of the browser JVM |
|
27630 | 32 |
application. Invoking ``$ISABELLE/Admin/build browser'' will do the |
33 |
job. |
|
14583 | 34 |
|
35 |
Now you can build images by going to corresponding folders and issuing: |
|
28504
7ad7d7d6df47
simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents:
27630
diff
changeset
|
36 |
isabelle make |
14583 | 37 |
|
38 |
(for instance, in "$ISABELLE/HOL" in order to make HOL). This |
|
39 |
will create the directory "~/isabelle" (if not already present). |
|
40 |
||
41 |
After setting up the local copy of Isabelle, changes in the repository |
|
42 |
can be imported by: |
|
43 |
cvs update -d -P |
|
44 |
||
45 |
(-d causes cvs to create directories that have appeared in the |
|
46 |
repository since the last update, -P causes directories that have been |
|
47 |
removed from the repository to be pruned). |
|
48 |
||
27461 | 49 |
Default Isabelle settings: |
14583 | 50 |
|
51 |
$ISABELLE_HOME is the directory "isabelle/Distribution" from above. |
|
52 |
$ISABELLE_HOME_USER is the directory "~/isabelle". |
|
53 |
||
54 |
||
14584 | 55 |
$Id$ |