author | wenzelm |
Thu, 11 Nov 1999 11:27:31 +0100 | |
changeset 8007 | c29e27ee4933 |
parent 6486 | 1f1d5e00e0a5 |
child 8809 | 85539b33be03 |
permissions | -rw-r--r-- |
wenzelm@2759 | 1 |
|
wenzelm@6486 | 2 |
Isabelle compilation and installation notes |
wenzelm@6486 | 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@6258 | 25 |
This does not store any references to [ISABELLE_HOME]. You may safely |
wenzelm@6258 | 26 |
move the system later, without running ./configure again. |
wenzelm@6258 | 27 |
|
wenzelm@2759 | 28 |
|
wenzelm@3263 | 29 |
ML system settings and compilation |
wenzelm@3263 | 30 |
---------------------------------- |
wenzelm@2759 | 31 |
|
wenzelm@2759 | 32 |
Before actual compilation you have to tell Isabelle about your |
wenzelm@2759 | 33 |
Standard ML system. These settings reside in ./etc/settings, which |
wenzelm@2759 | 34 |
may be also overridden by ~/isabelle/etc/settings. There are already |
wenzelm@2759 | 35 |
various sample configurations in ./etc/settings commented out. |
wenzelm@2759 | 36 |
|
wenzelm@3117 | 37 |
To build the core Isabelle/Pure and the default object-logic, just |
wenzelm@3117 | 38 |
type: |
wenzelm@2759 | 39 |
|
wenzelm@2759 | 40 |
./build |
wenzelm@2759 | 41 |
|
wenzelm@3117 | 42 |
More object-logics can be made similarly: |
wenzelm@2759 | 43 |
|
wenzelm@2759 | 44 |
./build FOL HOL |
wenzelm@2759 | 45 |
|
wenzelm@2759 | 46 |
|
wenzelm@3263 | 47 |
Running the system |
wenzelm@3263 | 48 |
------------------ |
wenzelm@2759 | 49 |
|
wenzelm@3263 | 50 |
Provided that compilation was successful, you can now run something |
wenzelm@2759 | 51 |
like: |
wenzelm@2759 | 52 |
|
wenzelm@2759 | 53 |
[ISABELLE_HOME]/bin/isabelle FOL |
wenzelm@2759 | 54 |
|
wenzelm@3263 | 55 |
This starts an interactive Isabelle session within your current text |
wenzelm@2759 | 56 |
terminal. You may want to put [ISABELLE_HOME]/bin into your shell's |
wenzelm@5395 | 57 |
search PATH. |
wenzelm@5395 | 58 |
|
wenzelm@6345 | 59 |
Please do *not* copy (or link) the Isabelle scripts anywhere else, or |
wenzelm@6345 | 60 |
they just won't work! If you really feel the urge to install |
wenzelm@6345 | 61 |
independent Isabelle binaries anywhere else do it like this: |
wenzelm@5396 | 62 |
|
wenzelm@6416 | 63 |
[ISABELLE_HOME]/bin/isatool install -p /usr/local/bin |
wenzelm@5396 | 64 |
|
wenzelm@2759 | 65 |
|
wenzelm@2759 | 66 |
|
wenzelm@2759 | 67 |
$Id$ |