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