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 Clicking on that icon will invoke the interface wrapper script
46 (capital Isabelle), which may be configured to run your favorite
47 Isabelle user interface via the ISABELLE_INTERFACE setting.
48 Additional options may be passed by editing the application's command
49 line (by using the standard KDE desktop functionality).
52 2) System installation
53 ----------------------
55 The Isabelle distribution is available both as traditional source-only
56 tar.gz archives, and as binary packages (currently only RPM for
57 Linux/x86). In any case, the resulting Isabelle installation always
58 contains the full sources, thus any part of the system be recompiled
62 2a) Binary installation
63 ----------------------
65 Ready-to-go RPM packages are provided for the ML compiler and runtime
66 system, the Isabelle sources, and some major object-logics. These
67 packages should work on any major RPM-based Linux/x86 platform (such
68 as SuSE, RedHat etc.). A typical installation procedure would be like
69 this (executed as root):
71 rpm -i smlnj-110.0-3.i386.rpm
72 rpm -i --prefix /usr/share isabelle.rpm
73 rpm -i --prefix /usr/share isabelle-HOL.i386.rpm
75 The install prefix may be changed as indicated. By default the ML
76 system is expected to be at the same directory level as Isabelle
77 itself; changing this arrangement requires
78 [ISABELLE_HOME]/etc/settings to be adapted manually.
81 Note that isabelle.rpm and isabelle-pdfdocs.rpm already contain all of
82 Isabelle as platform independent sources. Precompiled object-logics
83 are provided for convenience.
89 Some people prefer to be able to reconstruct the full system from the
90 sources, rather than installing RPM packages blindly. We do not
91 provide source RPMs, yet any parts of Isabelle may be recompiled after
92 installation of the main isabelle.rpm package (which contains only
95 Assuming proper configuration of the underlying ML system, Isabelle
96 object-logics may be recompiled like this:
98 [ISABELLE_HOME]/build HOL FOL
104 Traditional tar.gz archives are provided for the full Isabelle sources
105 and documentation as well. Make sure your ML system (SML/NJ, Poly/ML
106 etc.) has already been installed properly; then proceed as follows.
109 * Unpacking the archives. After unpacking the Isabelle distribution
110 archives (using tar and gzip) you are left with some directory
111 IsabelleYY-X. Basically, this may be installed anywhere --- just note
112 that ~/isabelle would be a really bad idea, though. The place where
113 you put the contents of IsabelleYY-X will be referred to as
114 [ISABELLE_HOME] subsequently.
117 * Auto configuration. There are some minor adaptions to be made of
118 the Isabelle distribution to your system environment (mostly locations
119 of bash and perl). Simply do it like this:
124 Note that this does not store any references to [ISABELLE_HOME]. You
125 may safely move the system later, without having to run ./configure
129 * ML system settings and compilation. Before actual compilation you
130 have to tell Isabelle about your Standard ML system. These settings
131 reside in ./etc/settings, which may be also overridden by
132 ~/isabelle/etc/settings. There are already various sample
133 configurations in ./etc/settings commented out.
135 To build the core Isabelle/Pure and the default object-logic, just
140 More object-logics can be made in a similar fashion:
144 After successful compilation you are ready to run the system, see 1)
145 above for more information.