kleing@14583: How to install a repository version of Isabelle.
kleing@14583: 
kleing@14583: The following assumes that you have successfully checked out Isabelle
kleing@14583: from CVS into a directory $ISABELLE (by default 'isabelle')
kleing@14583: 
kleing@14583: The directory structure of the repository is different from the
kleing@14583: distribution. The root directory $ISABELLE is the src
kleing@14583: subdirectory in the distribution. The 'normal' distribution
kleing@14583: directories are found in $ISABELLE/Distribution.
kleing@14583: 
kleing@14583: To work directly on a working copy of the repository, do the following:
kleing@14583: 
kleing@14583: Change directory to "$ISABELLE/Distribution/bin" and execute:
kleing@14583:    ./isatool install -p ~/bin
kleing@14583: 
kleing@14583: This will install Isabelle executables in ~/bin.  Then issue in
kleing@14583: directory "$ISABELLE/Distribution"
kleing@14583:    ln -s .. src
kleing@14583: 
kleing@14583: This tells the Isabelle binaries where to find the theories.
kleing@14583: 
kleing@14585: In $ISABELLE/Distribution/contrib install PolyML and
kleing@14585: ProofGeneral. Download the corresponding packages from
kleing@14585: http://isabelle.in.tum.de/dist/ and unpack them in
kleing@14585: $ISABELLE/Distribution/contrib.  If you have already installed them
kleing@14585: elsewhere, it is sufficient to create a symbolic link in contrib to
kleing@14585: the main PolyML and ProofGeneral directories. The links should be
kleing@14585: called 'polyml' and 'ProofGeneral'.
kleing@14583: 
kleing@14583: Before you can build logic images it is necessary to initialise
kleing@14583: generation of browser info.  Change to the directory
kleing@14583: "$ISABELLE/Distribution/lib/browser" and issue
kleing@14583:    make
kleing@14583: 
kleing@14583: Java JDK 1.1 or greater needs to be installed for this to work.
kleing@14583: 
kleing@14583: Now you can build images by going to corresponding folders and issuing:
kleing@14583:    isatool make
kleing@14583: 
kleing@14583: (for instance, in "$ISABELLE/HOL" in order to make HOL).  This
kleing@14583: will create the directory "~/isabelle" (if not already present).
kleing@14583: 
kleing@14583: After setting up the local copy of Isabelle, changes in the repository
kleing@14583: can be imported by:
kleing@14583:    cvs update -d -P
kleing@14583: 
kleing@14583: (-d causes cvs to create directories that have appeared in the
kleing@14583: repository since the last update, -P causes directories that have been
kleing@14583: removed from the repository to be pruned).
kleing@14583: 
kleing@14583: Internal environment variables
kleing@14583: 
kleing@14583:   $ISABELLE_HOME is the directory "isabelle/Distribution" from above.
kleing@14583:   $ISABELLE_HOME_USER is the directory "~/isabelle".
kleing@14583: 
kleing@14583: 
kleing@14584: $Id$