author | Walther Neuper <neuper@ist.tugraz.at> |
Sun, 14 Jul 2013 14:48:14 +0200 | |
changeset 52056 | f5d9bceb4dc0 |
parent 37871 | 875b6efa7ced |
permissions | -rw-r--r-- |
neuper@37871 | 1 |
WN1900721 copy from Isabelle2009-1 |
neuper@37871 | 2 |
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! |
neuper@37871 | 3 |
|
neuper@37871 | 4 |
Isabelle installation notes |
neuper@37871 | 5 |
=========================== |
neuper@37871 | 6 |
|
neuper@37871 | 7 |
1) System installation |
neuper@37871 | 8 |
---------------------- |
neuper@37871 | 9 |
|
neuper@37871 | 10 |
The Isabelle distribution includes both complete sources and |
neuper@37871 | 11 |
precompiled binary packages for common Unix-like platforms. |
neuper@37871 | 12 |
|
neuper@37871 | 13 |
|
neuper@37871 | 14 |
Quick installation |
neuper@37871 | 15 |
------------------ |
neuper@37871 | 16 |
|
neuper@37871 | 17 |
Ready-to-go packages are provided for the ML compiler and runtime |
neuper@37871 | 18 |
system, the Isabelle sources, and some major object-logics. A minimal |
neuper@37871 | 19 |
site installation of Isabelle on Linux/x86 works like this: |
neuper@37871 | 20 |
|
neuper@37871 | 21 |
tar -C /usr/local -xzf Isabelle.tar.gz |
neuper@37871 | 22 |
tar -C /usr/local -xzf polyml.tar.gz |
neuper@37871 | 23 |
tar -C /usr/local -xzf HOL_x86-linux.tar.gz |
neuper@37871 | 24 |
|
neuper@37871 | 25 |
The install prefix given above may be changed as appropriate; there is |
neuper@37871 | 26 |
no need to install into a system directory like /usr/local at all. By |
neuper@37871 | 27 |
default the ML system (and other contributed packages) are expected in |
neuper@37871 | 28 |
any of the following locations: |
neuper@37871 | 29 |
|
neuper@37871 | 30 |
1) [ISABELLE_HOME]/contrib |
neuper@37871 | 31 |
2) [ISABELLE_HOME]/.. |
neuper@37871 | 32 |
4) /usr/local |
neuper@37871 | 33 |
3) /usr/share |
neuper@37871 | 34 |
5) /opt |
neuper@37871 | 35 |
|
neuper@37871 | 36 |
This may be changed by editing [ISABELLE_HOME]/etc/settings manually. |
neuper@37871 | 37 |
|
neuper@37871 | 38 |
The installation may be finished as follows: |
neuper@37871 | 39 |
|
neuper@37871 | 40 |
cd [ISABELLE_HOME] |
neuper@37871 | 41 |
./bin/isabelle install -p /usr/local/bin |
neuper@37871 | 42 |
|
neuper@37871 | 43 |
The install utility creates global references to the present Isabelle |
neuper@37871 | 44 |
installation, enabling users to invoke the Isabelle executables |
neuper@37871 | 45 |
without explicit path names. This is the only place where a static |
neuper@37871 | 46 |
reference to [ISABELLE_HOME] is created; thus isabelle install has to |
neuper@37871 | 47 |
be run again whenever the Isabelle distribution is moved later. |
neuper@37871 | 48 |
|
neuper@37871 | 49 |
|
neuper@37871 | 50 |
Compiling logics |
neuper@37871 | 51 |
---------------- |
neuper@37871 | 52 |
|
neuper@37871 | 53 |
The Isabelle.tar.gz archive already contains all Isabelle sources (and |
neuper@37871 | 54 |
documentation). Precompiled object-logics are provided for |
neuper@37871 | 55 |
convenience. |
neuper@37871 | 56 |
|
neuper@37871 | 57 |
Assuming proper configuration of the underlying ML system |
neuper@37871 | 58 |
(cf. Isabelle's etc/settings), further object-logics may be compiled |
neuper@37871 | 59 |
like this: |
neuper@37871 | 60 |
|
neuper@37871 | 61 |
[ISABELLE_HOME]/build FOL |
neuper@37871 | 62 |
|
neuper@37871 | 63 |
Special object-logic targets may be specified as follows: |
neuper@37871 | 64 |
|
neuper@37871 | 65 |
[ISABELLE_HOME]/build -m HOL-Algebra HOL |
neuper@37871 | 66 |
|
neuper@37871 | 67 |
|
neuper@37871 | 68 |
2) User installation |
neuper@37871 | 69 |
-------------------- |
neuper@37871 | 70 |
|
neuper@37871 | 71 |
Running the Isabelle binaries |
neuper@37871 | 72 |
----------------------------- |
neuper@37871 | 73 |
|
neuper@37871 | 74 |
Users may invoke the main Isabelle binaries (isabelle and |
neuper@37871 | 75 |
isabelle-process) directly from their location within the distribution |
neuper@37871 | 76 |
directory [ISABELLE_HOME] like this: |
neuper@37871 | 77 |
|
neuper@37871 | 78 |
[ISABELLE_HOME]/bin/isabelle tty -l HOL |
neuper@37871 | 79 |
|
neuper@37871 | 80 |
This starts an interactive Isabelle session within the current text |
neuper@37871 | 81 |
terminal. [ISABELLE_HOME]/bin may be put into the shell's search |
neuper@37871 | 82 |
PATH. An alternative is to create global references to the Isabelle |
neuper@37871 | 83 |
executables as follows: |
neuper@37871 | 84 |
|
neuper@37871 | 85 |
[ISABELLE_HOME]/bin/isabelle install -p ~/bin |
neuper@37871 | 86 |
|
neuper@37871 | 87 |
Note that the site-wide Isabelle installation may already provide |
neuper@37871 | 88 |
Isabelle executables in some global bin directory (such as |
neuper@37871 | 89 |
/usr/local/bin). |