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