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