Admin/README.repos
author wenzelm
Thu Jul 03 13:17:19 2008 +0200 (2008-07-03 ago)
changeset 27461 c2bba6a4d750
parent 14585 6cf696e5ef7f
child 27630 5580fcca2b5d
permissions -rw-r--r--
specific to CVS;
some updates for Java etc.;
wenzelm@27461
     1
How to install a CVS repository version of Isabelle.
kleing@14583
     2
kleing@14583
     3
The following assumes that you have successfully checked out Isabelle
kleing@14583
     4
from CVS into a directory $ISABELLE (by default 'isabelle')
kleing@14583
     5
wenzelm@27461
     6
The directory structure of the CVS is different from the
kleing@14583
     7
distribution. The root directory $ISABELLE is the src
kleing@14583
     8
subdirectory in the distribution. The 'normal' distribution
kleing@14583
     9
directories are found in $ISABELLE/Distribution.
kleing@14583
    10
kleing@14583
    11
To work directly on a working copy of the repository, do the following:
kleing@14583
    12
kleing@14583
    13
Change directory to "$ISABELLE/Distribution/bin" and execute:
kleing@14583
    14
   ./isatool install -p ~/bin
kleing@14583
    15
kleing@14583
    16
This will install Isabelle executables in ~/bin.  Then issue in
kleing@14583
    17
directory "$ISABELLE/Distribution"
kleing@14583
    18
   ln -s .. src
kleing@14583
    19
kleing@14583
    20
This tells the Isabelle binaries where to find the theories.
kleing@14583
    21
wenzelm@27461
    22
In $ISABELLE/Distribution/contrib install Poly/ML and
wenzelm@27461
    23
Proof General. Download the corresponding packages from
kleing@14585
    24
http://isabelle.in.tum.de/dist/ and unpack them in
kleing@14585
    25
$ISABELLE/Distribution/contrib.  If you have already installed them
kleing@14585
    26
elsewhere, it is sufficient to create a symbolic link in contrib to
wenzelm@27461
    27
the main Poly/ML and ProofGeneral directories. The links should be
kleing@14585
    28
called 'polyml' and 'ProofGeneral'.
kleing@14583
    29
wenzelm@27461
    30
Building logic images with browser info generation (which is the
wenzelm@27461
    31
default setting) requires a compiled version of the browser JVM
wenzelm@27461
    32
application.  Change to the directory
wenzelm@27461
    33
"$ISABELLE/Distribution/lib/browser" and issue make; this requires
wenzelm@27461
    34
Java JDK 1.4 or greater.
kleing@14583
    35
kleing@14583
    36
Now you can build images by going to corresponding folders and issuing:
kleing@14583
    37
   isatool make
kleing@14583
    38
kleing@14583
    39
(for instance, in "$ISABELLE/HOL" in order to make HOL).  This
kleing@14583
    40
will create the directory "~/isabelle" (if not already present).
kleing@14583
    41
kleing@14583
    42
After setting up the local copy of Isabelle, changes in the repository
kleing@14583
    43
can be imported by:
kleing@14583
    44
   cvs update -d -P
kleing@14583
    45
kleing@14583
    46
(-d causes cvs to create directories that have appeared in the
kleing@14583
    47
repository since the last update, -P causes directories that have been
kleing@14583
    48
removed from the repository to be pruned).
kleing@14583
    49
wenzelm@27461
    50
Default Isabelle settings:
kleing@14583
    51
kleing@14583
    52
  $ISABELLE_HOME is the directory "isabelle/Distribution" from above.
kleing@14583
    53
  $ISABELLE_HOME_USER is the directory "~/isabelle".
kleing@14583
    54
kleing@14583
    55
kleing@14584
    56
$Id$