diff -r 8fb8c17d1cb5 -r 352412857003 INSTALL --- a/INSTALL Tue Sep 26 17:03:52 2000 +0200 +++ b/INSTALL Tue Sep 26 17:04:17 2000 +0200 @@ -1,158 +1,110 @@ -Isabelle installation and compilation notes -=========================================== +Isabelle installation notes +=========================== + +1) System installation +---------------------- + +The Isabelle distribution includes both complete sources and +precompiled binary packages for common Unix 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_base.tar.gz + tar -C /usr/local -xzf polyml_x86-linux.tar.gz + tar -C /usr/local -xzf HOL_x86-linux.tar.gz + +The install prefix given above may be changed as appropriate. By +default the ML system (and other contributed packages) are expected in +any of the following locations: + + 1) [ISABELLE_HOME]/contrib + 2) [ISABELLE_HOME]/.. + 3) /usr/share + 4) /usr/local + 5) /opt + +This may be changed by editing [ISABELLE_HOME]/etc/settings manually. -1) User installation +The installation may be finished as follows: + + cd [ISABELLE_HOME] + ./configure + ./bin/isatool install -p /usr/local/bin + +Note that the configure script is only required for systems that do +not have bash and perl in the canonical places (/bin/bash and +/usr/bin/perl). + +The install utility creates global references to the present Isabelle +installation, enabling users to invoke the Isabelle executables +without explicit path names. Incidently, this is the only place where +a static reference to [ISABELLE_HOME] is created; thus isatool 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-Real HOL + + +2) User installation -------------------- -Here we assume that Isabelle has already been installed at your site. -Otherwise see 2) below of how to get the Isabelle system installed in -the first place. - +Running the Isabelle binaries +----------------------------- -1a) Running the Isabelle binaries ---------------------------------- - -The Isabelle binaries (isatool, isabelle, Isabelle) may be invoked +Users may invoke the Isabelle binaries (isatool, isabelle, Isabelle) directly from their location within the distribution directory [ISABELLE_HOME] like this: [ISABELLE_HOME]/bin/isabelle HOL -This starts an interactive Isabelle session within your current text -terminal. You may want to put [ISABELLE_HOME]/bin into your shell's -search PATH, but this is not strictly necessary. - - -Please do *not* copy (or link) the Isabelle scripts anywhere else --- -they just won't work! If you really want to install independent -Isabelle binaries somewhere else then do it like this: +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/isatool install -p ~/bin -Your site-wide Isabelle installation may already provide Isabelle -executables in some global bin directory (such as /usr/bin). +Note that the site-wide Isabelle installation may already provide +Isabelle executables in some global bin directory (such as +/usr/local/bin). -1b) Isabelle as KDE application -------------------------------- +Isabelle as KDE application +--------------------------- -Isabelle may be installed as application icon on the KDE desktop like -this: +Users may install an Isabelle application icon on the KDE desktop as +follows: [ISABELLE_HOME]/bin/isatool install -k -You may have to refresh the KDE desktop in order to see the new icon. Clicking on Isabelle will invoke the interface wrapper script (capital -Isabelle), which is usually configured to run Proof General (see also -the ISABELLE_INTERFACE setting). Additional options may be passed to +Isabelle), which is usually configured to run Proof General (cf. the +ISABELLE_INTERFACE setting). Additional options may be passed to Isabelle by editing the application's command line using the standard -KDE desktop functionality. - - -2) System installation ----------------------- - -The Isabelle distribution is available both as traditional source-only -tar.gz archives, and as binary packages (currently only RPM for -Linux/x86). In any case, the resulting Isabelle installation always -contains the full sources, thus any part of the system be recompiled -later, too. - - -2a) Binary installation ----------------------- - -Ready-to-go RPM packages are provided for the ML compiler and runtime -system, the Isabelle sources, and some major object-logics. These -packages should work on any major Linux/x86 platform based on RPM -package management. - -A minimal installation would work like this (executed as root): - - rpm -i --prefix /usr/share polyml.i386.rpm - rpm -i --prefix /usr/share isabelle.rpm - rpm -i --prefix /usr/share isabelle-HOL.i386.rpm - -Note that installed RPMs may be removed like this: - - rpm -e isabelle-HOL isabelle polyml - -The install prefix given above may be changed. By default the ML -system (and other contributed packages) are expected in either of the -following three locations: - - 1) [ISABELLE_HOME]/contrib - 2) [ISABELLE_HOME]/.. - 3) /usr/share - 4) /usr/local - -This may be changed further by editing [ISABELLE_HOME]/etc/settings -manually. - -Note that isabelle.rpm and isabelle-pdfdocs.rpm already contain all of -Isabelle as platform independent sources. Precompiled object-logics -are provided for convenience. - - -Recompiling logics ------------------- - -Some people prefer to be able to reconstruct the full system from the -sources, rather than installing precompiled packages blindly. We do -not provide source RPMs, yet any parts of Isabelle may be recompiled -after installation of the main isabelle.rpm package (which contains -only sources anyway). - -Assuming proper configuration of the underlying ML system, Isabelle -object-logics may be recompiled like this: - - [ISABELLE_HOME]/build HOL FOL - - -Source installation -------------------- - -Traditional tar.gz archives are provided for the full Isabelle sources -and documentation as well. Make sure your ML system (e.g. Poly/ML -etc.) has already been installed properly; then proceed as follows. - -* Unpacking the archives. After unpacking the Isabelle distribution -archives (using tar and gzip) you are left with some directory -IsabelleYY-X. - -* Auto configuration. There are some minor adaptions to be made of -the Isabelle distribution to your system environment (locations of -bash and perl). Simply do it like this: - - cd [ISABELLE_HOME] - ./configure - -Note that this does not store any references to [ISABELLE_HOME]. You -may safely move the system later, without having to run ./configure -again. - -* ML system settings and compilation. Before actual compilation you -have to tell Isabelle about your Standard ML system. These settings -reside in ./etc/settings, which may be also overridden by -~/isabelle/etc/settings. There are already various sample -configurations in ./etc/settings commented out. - -To build the core Isabelle/Pure and the default object-logic, just -type - - ./build - -More object-logics can be made in a similar fashion: - - ./build FOL HOL - -Explicit make targets may be given as follows: - - ./build -m HOL-Real HOL - -After successful compilation you are ready to run the system, see 1) -above for more information. +KDE properties editing facilities. $Id$