|
2759
|
1 |
|
|
|
2 |
***************************************************************************
|
|
|
3 |
|
|
|
4 |
IMPORTANT NOTE: This file describes the *new* installation procedure
|
|
|
5 |
using various scripts that are still supposed beta for Isabelle94-8.
|
|
3322
|
6 |
If you encounter serious problems, you may want to consider compiling
|
|
3263
|
7 |
Isabelle the olden way, as described in README.old.
|
|
2759
|
8 |
|
|
|
9 |
***************************************************************************
|
|
|
10 |
|
|
|
11 |
|
|
|
12 |
Isabelle installation notes
|
|
|
13 |
===========================
|
|
|
14 |
|
|
3263
|
15 |
Unpacking the archive
|
|
|
16 |
---------------------
|
|
2759
|
17 |
|
|
3263
|
18 |
After unpacking the Isabelle distribution archive (using tar and gzip)
|
|
|
19 |
you are left with some directory IsabelleYY-X. You may install this
|
|
3117
|
20 |
anywhere, but please just *not* as ~/isabelle!!!
|
|
2759
|
21 |
|
|
|
22 |
The place where you put the contents of IsabelleYY-X will be referred
|
|
|
23 |
to as [ISABELLE_HOME] subsequently.
|
|
|
24 |
|
|
|
25 |
|
|
3263
|
26 |
Auto configuration
|
|
|
27 |
------------------
|
|
2759
|
28 |
|
|
|
29 |
There are some minor adaptions to be made of the Isabelle distribution
|
|
|
30 |
to your system environment. Simply type:
|
|
|
31 |
|
|
|
32 |
cd [ISABELLE_HOME]
|
|
|
33 |
./configure
|
|
|
34 |
|
|
|
35 |
|
|
3263
|
36 |
ML system settings and compilation
|
|
|
37 |
----------------------------------
|
|
2759
|
38 |
|
|
|
39 |
Before actual compilation you have to tell Isabelle about your
|
|
|
40 |
Standard ML system. These settings reside in ./etc/settings, which
|
|
|
41 |
may be also overridden by ~/isabelle/etc/settings. There are already
|
|
|
42 |
various sample configurations in ./etc/settings commented out.
|
|
|
43 |
|
|
3117
|
44 |
To build the core Isabelle/Pure and the default object-logic, just
|
|
|
45 |
type:
|
|
2759
|
46 |
|
|
|
47 |
./build
|
|
|
48 |
|
|
3117
|
49 |
More object-logics can be made similarly:
|
|
2759
|
50 |
|
|
|
51 |
./build FOL HOL
|
|
|
52 |
|
|
|
53 |
|
|
3263
|
54 |
Running the system
|
|
|
55 |
------------------
|
|
2759
|
56 |
|
|
3263
|
57 |
Provided that compilation was successful, you can now run something
|
|
2759
|
58 |
like:
|
|
|
59 |
|
|
|
60 |
[ISABELLE_HOME]/bin/isabelle FOL
|
|
|
61 |
|
|
3263
|
62 |
This starts an interactive Isabelle session within your current text
|
|
2759
|
63 |
terminal. You may want to put [ISABELLE_HOME]/bin into your shell's
|
|
3263
|
64 |
search PATH. Please do *not* copy (or link) the Isabelle scripts
|
|
|
65 |
somewhere else -- or they just won't work!
|
|
2759
|
66 |
|
|
|
67 |
|
|
|
68 |
$Id$
|