diff -r 8680677265c9 -r 1c816f2abb0e INSTALL --- a/INSTALL Tue Jun 08 17:45:39 2010 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,87 +0,0 @@ - -Isabelle installation notes -=========================== - -1) System installation ----------------------- - -The Isabelle distribution includes both complete sources and -precompiled binary packages for common Unix-like platforms. - - -Quick installation ------------------- - -Ready-to-go packages are provided for the ML compiler and runtime -system, the Isabelle sources, and some major object-logics. A minimal -site installation of Isabelle on Linux/x86 works like this: - - tar -C /usr/local -xzf Isabelle.tar.gz - tar -C /usr/local -xzf polyml.tar.gz - tar -C /usr/local -xzf HOL_x86-linux.tar.gz - -The install prefix given above may be changed as appropriate; there is -no need to install into a system directory like /usr/local at all. By -default the ML system (and other contributed packages) are expected in -any of the following locations: - - 1) [ISABELLE_HOME]/contrib - 2) [ISABELLE_HOME]/.. - 4) /usr/local - 3) /usr/share - 5) /opt - -This may be changed by editing [ISABELLE_HOME]/etc/settings manually. - -The installation may be finished as follows: - - cd [ISABELLE_HOME] - ./bin/isabelle install -p /usr/local/bin - -The install utility creates global references to the present Isabelle -installation, enabling users to invoke the Isabelle executables -without explicit path names. This is the only place where a static -reference to [ISABELLE_HOME] is created; thus isabelle install has to -be run again whenever the Isabelle distribution is moved later. - - -Compiling logics ----------------- - -The Isabelle.tar.gz archive already contains all Isabelle sources (and -documentation). Precompiled object-logics are provided for -convenience. - -Assuming proper configuration of the underlying ML system -(cf. Isabelle's etc/settings), further object-logics may be compiled -like this: - - [ISABELLE_HOME]/build FOL - -Special object-logic targets may be specified as follows: - - [ISABELLE_HOME]/build -m HOL-Algebra HOL - - -2) User installation --------------------- - -Running the Isabelle binaries ------------------------------ - -Users may invoke the main Isabelle binaries (isabelle and -isabelle-process) directly from their location within the distribution -directory [ISABELLE_HOME] like this: - - [ISABELLE_HOME]/bin/isabelle tty -l HOL - -This starts an interactive Isabelle session within the current text -terminal. [ISABELLE_HOME]/bin may be put into the shell's search -PATH. An alternative is to create global references to the Isabelle -executables as follows: - - [ISABELLE_HOME]/bin/isabelle install -p ~/bin - -Note that the site-wide Isabelle installation may already provide -Isabelle executables in some global bin directory (such as -/usr/local/bin).