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@8809: Clicking on that icon will invoke the interface wrapper script wenzelm@8809: (capital Isabelle), which may be configured to run your favorite wenzelm@8809: Isabelle user interface via the ISABELLE_INTERFACE setting. wenzelm@8809: Additional options may be passed by editing the application's command wenzelm@8809: line (by using the standard 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@8809: packages should work on any major RPM-based Linux/x86 platform (such wenzelm@8809: as SuSE, RedHat etc.). A typical installation procedure would be like wenzelm@8809: this (executed as root): wenzelm@8809: wenzelm@9927: rpm -i --prefix /usr/share polyml.i386.rpm wenzelm@8809: rpm -i --prefix /usr/share isabelle.rpm wenzelm@8809: rpm -i --prefix /usr/share isabelle-HOL.i386.rpm wenzelm@8809: wenzelm@8809: The install prefix may be changed as indicated. By default the ML wenzelm@8809: system is expected to be at the same directory level as Isabelle wenzelm@9927: itself; see [ISABELLE_HOME]/etc/settings of how to change this. 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@8809: sources, rather than installing RPM packages blindly. We do not wenzelm@8809: provide source RPMs, yet any parts of Isabelle may be recompiled after wenzelm@8809: installation of the main isabelle.rpm package (which contains only wenzelm@8809: 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@8809: and documentation as well. Make sure your ML system (SML/NJ, 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@8809: IsabelleYY-X. Basically, this may be installed anywhere --- just note wenzelm@8809: that ~/isabelle would be a really bad idea, though. The place where wenzelm@8809: you put the contents of IsabelleYY-X will be referred to as wenzelm@8809: [ISABELLE_HOME] subsequently. wenzelm@8809: wenzelm@8809: * Auto configuration. There are some minor adaptions to be made of wenzelm@8809: the Isabelle distribution to your system environment (mostly locations wenzelm@8809: of 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$