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