INSTALL
changeset 37368 1c816f2abb0e
parent 37367 8680677265c9
child 37369 e0460bbf6b39
     1.1 --- a/INSTALL	Tue Jun 08 17:45:39 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,87 +0,0 @@
     1.4 -
     1.5 -Isabelle installation notes
     1.6 -===========================
     1.7 -
     1.8 -1) System installation
     1.9 -----------------------
    1.10 -
    1.11 -The Isabelle distribution includes both complete sources and
    1.12 -precompiled binary packages for common Unix-like platforms.
    1.13 -
    1.14 -
    1.15 -Quick installation
    1.16 -------------------
    1.17 -
    1.18 -Ready-to-go packages are provided for the ML compiler and runtime
    1.19 -system, the Isabelle sources, and some major object-logics.  A minimal
    1.20 -site installation of Isabelle on Linux/x86 works like this:
    1.21 -
    1.22 -  tar -C /usr/local -xzf Isabelle.tar.gz
    1.23 -  tar -C /usr/local -xzf polyml.tar.gz
    1.24 -  tar -C /usr/local -xzf HOL_x86-linux.tar.gz
    1.25 -
    1.26 -The install prefix given above may be changed as appropriate; there is
    1.27 -no need to install into a system directory like /usr/local at all.  By
    1.28 -default the ML system (and other contributed packages) are expected in
    1.29 -any of the following locations:
    1.30 -
    1.31 -  1) [ISABELLE_HOME]/contrib
    1.32 -  2) [ISABELLE_HOME]/..
    1.33 -  4) /usr/local
    1.34 -  3) /usr/share
    1.35 -  5) /opt
    1.36 -
    1.37 -This may be changed by editing [ISABELLE_HOME]/etc/settings manually.
    1.38 -
    1.39 -The installation may be finished as follows:
    1.40 -
    1.41 -  cd [ISABELLE_HOME]
    1.42 -  ./bin/isabelle install -p /usr/local/bin
    1.43 -
    1.44 -The install utility creates global references to the present Isabelle
    1.45 -installation, enabling users to invoke the Isabelle executables
    1.46 -without explicit path names.  This is the only place where a static
    1.47 -reference to [ISABELLE_HOME] is created; thus isabelle install has to
    1.48 -be run again whenever the Isabelle distribution is moved later.
    1.49 -
    1.50 -
    1.51 -Compiling logics
    1.52 -----------------
    1.53 -
    1.54 -The Isabelle.tar.gz archive already contains all Isabelle sources (and
    1.55 -documentation).  Precompiled object-logics are provided for
    1.56 -convenience.
    1.57 -
    1.58 -Assuming proper configuration of the underlying ML system
    1.59 -(cf. Isabelle's etc/settings), further object-logics may be compiled
    1.60 -like this:
    1.61 -
    1.62 -  [ISABELLE_HOME]/build FOL
    1.63 -
    1.64 -Special object-logic targets may be specified as follows:
    1.65 -
    1.66 -  [ISABELLE_HOME]/build -m HOL-Algebra HOL
    1.67 -
    1.68 -
    1.69 -2) User installation
    1.70 ---------------------
    1.71 -
    1.72 -Running the Isabelle binaries
    1.73 ------------------------------
    1.74 -
    1.75 -Users may invoke the main Isabelle binaries (isabelle and
    1.76 -isabelle-process) directly from their location within the distribution
    1.77 -directory [ISABELLE_HOME] like this:
    1.78 -
    1.79 -  [ISABELLE_HOME]/bin/isabelle tty -l HOL
    1.80 -
    1.81 -This starts an interactive Isabelle session within the current text
    1.82 -terminal.  [ISABELLE_HOME]/bin may be put into the shell's search
    1.83 -PATH.  An alternative is to create global references to the Isabelle
    1.84 -executables as follows:
    1.85 -
    1.86 -  [ISABELLE_HOME]/bin/isabelle install -p ~/bin
    1.87 -
    1.88 -Note that the site-wide Isabelle installation may already provide
    1.89 -Isabelle executables in some global bin directory (such as
    1.90 -/usr/local/bin).