1.1 --- a/INSTALL Sun Jul 14 15:02:09 2013 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,89 +0,0 @@
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).