2759
|
1 |
|
8809
|
2 |
Isabelle installation and compilation notes
|
6486
|
3 |
===========================================
|
2759
|
4 |
|
8809
|
5 |
1) User installation
|
|
6 |
--------------------
|
|
7 |
|
|
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
|
|
10 |
the first place.
|
|
11 |
|
|
12 |
|
|
13 |
1a) Running the Isabelle binaries
|
|
14 |
---------------------------------
|
|
15 |
|
|
16 |
The Isabelle binaries (isatool, isabelle, Isabelle) may be invoked
|
|
17 |
directly from their location within the distribution directory
|
|
18 |
[ISABELLE_HOME] like this:
|
|
19 |
|
|
20 |
[ISABELLE_HOME]/bin/isabelle HOL
|
|
21 |
|
|
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.
|
|
25 |
|
|
26 |
|
|
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:
|
|
30 |
|
|
31 |
[ISABELLE_HOME]/bin/isatool install -p ~/bin
|
2759
|
32 |
|
8809
|
33 |
Your site-wide Isabelle installation may already provide Isabelle
|
|
34 |
executables in some global bin directory (such as /usr/bin).
|
|
35 |
|
|
36 |
|
|
37 |
1b) Isabelle as KDE application
|
|
38 |
-------------------------------
|
|
39 |
|
|
40 |
Isabelle may be installed as application icon on the KDE desktop like
|
|
41 |
this:
|
|
42 |
|
|
43 |
[ISABELLE_HOME]/bin/isatool install -k
|
2759
|
44 |
|
8809
|
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).
|
|
50 |
|
|
51 |
|
|
52 |
2) System installation
|
|
53 |
----------------------
|
|
54 |
|
|
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
|
|
59 |
later, too.
|
2759
|
60 |
|
|
61 |
|
8809
|
62 |
2a) Binary installation
|
|
63 |
----------------------
|
|
64 |
|
|
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):
|
|
70 |
|
|
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
|
|
74 |
|
|
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.
|
|
79 |
|
|
80 |
|
|
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.
|
|
84 |
|
|
85 |
|
|
86 |
Recompiling logics
|
3263
|
87 |
------------------
|
2759
|
88 |
|
8809
|
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
|
|
93 |
sources anyway).
|
|
94 |
|
|
95 |
Assuming proper configuration of the underlying ML system, Isabelle
|
|
96 |
object-logics may be recompiled like this:
|
|
97 |
|
|
98 |
[ISABELLE_HOME]/build HOL FOL
|
|
99 |
|
|
100 |
|
|
101 |
Source installation
|
|
102 |
-------------------
|
|
103 |
|
|
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.
|
|
107 |
|
|
108 |
|
|
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.
|
|
115 |
|
|
116 |
|
|
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:
|
2759
|
120 |
|
|
121 |
cd [ISABELLE_HOME]
|
|
122 |
./configure
|
|
123 |
|
8809
|
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
|
|
126 |
again.
|
6258
|
127 |
|
2759
|
128 |
|
8809
|
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.
|
2759
|
134 |
|
3117
|
135 |
To build the core Isabelle/Pure and the default object-logic, just
|
8809
|
136 |
type
|
2759
|
137 |
|
|
138 |
./build
|
|
139 |
|
8809
|
140 |
More object-logics can be made in a similar fashion:
|
2759
|
141 |
|
|
142 |
./build FOL HOL
|
|
143 |
|
8809
|
144 |
After successful compilation you are ready to run the system, see 1)
|
|
145 |
above for more information.
|
2759
|
146 |
|
|
147 |
|
|
148 |
$Id$
|