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