2 Isabelle installation and compilation notes
3 ===========================================
8 Here we assume that Isabelle has already been installed at your site.
9 Otherwise see 2) below of how to get the Isabelle system installed in
13 1a) Running the Isabelle binaries
14 ---------------------------------
16 The Isabelle binaries (isatool, isabelle, Isabelle) may be invoked
17 directly from their location within the distribution directory
18 [ISABELLE_HOME] like this:
20 [ISABELLE_HOME]/bin/isabelle HOL
22 This starts an interactive Isabelle session within your current text
23 terminal. You may want to put [ISABELLE_HOME]/bin into your shell's
24 search PATH, but this is not strictly necessary.
27 Please do *not* copy (or link) the Isabelle scripts anywhere else ---
28 they just won't work! If you really want to install independent
29 Isabelle binaries somewhere else then do it like this:
31 [ISABELLE_HOME]/bin/isatool install -p ~/bin
33 Your site-wide Isabelle installation may already provide Isabelle
34 executables in some global bin directory (such as /usr/bin).
37 1b) Isabelle as KDE application
38 -------------------------------
40 Isabelle may be installed as application icon on the KDE desktop like
43 [ISABELLE_HOME]/bin/isatool install -k
45 You may have to refresh the KDE desktop in order to see the new icon.
46 Clicking on Isabelle will invoke the interface wrapper script (capital
47 Isabelle), which is usually configured to run Proof General (see also
48 the ISABELLE_INTERFACE setting). Additional options may be passed to
49 Isabelle by editing the application's command line using the standard
50 KDE desktop functionality.
53 2) System installation
54 ----------------------
56 The Isabelle distribution is available both as traditional source-only
57 tar.gz archives, and as binary packages (currently only RPM for
58 Linux/x86). In any case, the resulting Isabelle installation always
59 contains the full sources, thus any part of the system be recompiled
63 2a) Binary installation
64 ----------------------
66 Ready-to-go RPM packages are provided for the ML compiler and runtime
67 system, the Isabelle sources, and some major object-logics. These
68 packages should work on any major Linux/x86 platform based on RPM
71 A minimal installation would work like this (executed as root):
73 rpm -i --prefix /usr/share polyml.i386.rpm
74 rpm -i --prefix /usr/share isabelle.rpm
75 rpm -i --prefix /usr/share isabelle-HOL.i386.rpm
77 Note that installed RPMs may be removed like this:
79 rpm -e isabelle-HOL isabelle polyml
81 The install prefix given above may be changed. By default the ML
82 system (and other contributed packages) are expected in either of the
83 following three locations:
85 1) [ISABELLE_HOME]/contrib
90 This may be changed further by editing [ISABELLE_HOME]/etc/settings
93 Note that isabelle.rpm and isabelle-pdfdocs.rpm already contain all of
94 Isabelle as platform independent sources. Precompiled object-logics
95 are provided for convenience.
101 Some people prefer to be able to reconstruct the full system from the
102 sources, rather than installing precompiled packages blindly. We do
103 not provide source RPMs, yet any parts of Isabelle may be recompiled
104 after installation of the main isabelle.rpm package (which contains
105 only sources anyway).
107 Assuming proper configuration of the underlying ML system, Isabelle
108 object-logics may be recompiled like this:
110 [ISABELLE_HOME]/build HOL FOL
116 Traditional tar.gz archives are provided for the full Isabelle sources
117 and documentation as well. Make sure your ML system (e.g. Poly/ML
118 etc.) has already been installed properly; then proceed as follows.
120 * Unpacking the archives. After unpacking the Isabelle distribution
121 archives (using tar and gzip) you are left with some directory
124 * Auto configuration. There are some minor adaptions to be made of
125 the Isabelle distribution to your system environment (locations of
126 bash and perl). Simply do it like this:
131 Note that this does not store any references to [ISABELLE_HOME]. You
132 may safely move the system later, without having to run ./configure
135 * ML system settings and compilation. Before actual compilation you
136 have to tell Isabelle about your Standard ML system. These settings
137 reside in ./etc/settings, which may be also overridden by
138 ~/isabelle/etc/settings. There are already various sample
139 configurations in ./etc/settings commented out.
141 To build the core Isabelle/Pure and the default object-logic, just
146 More object-logics can be made in a similar fashion:
150 Explicit make targets may be given as follows:
152 ./build -m HOL-Real HOL
154 After successful compilation you are ready to run the system, see 1)
155 above for more information.