author | paulson |
Thu, 02 Sep 2004 16:52:21 +0200 | |
changeset 15172 | 73069e033a0b |
parent 14024 | 213dcc39358f |
child 16476 | baa008d0fee9 |
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_base.tar.gz |
wenzelm@10081 | 21 |
tar -C /usr/local -xzf polyml_x86-linux.tar.gz |
wenzelm@10081 | 22 |
tar -C /usr/local -xzf HOL_x86-linux.tar.gz |
wenzelm@10081 | 23 |
|
wenzelm@10081 | 24 |
The install prefix given above may be changed as appropriate. 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@10081 | 30 |
3) /usr/share |
wenzelm@10081 | 31 |
4) /usr/local |
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 |
./configure |
wenzelm@10081 | 40 |
./bin/isatool install -p /usr/local/bin |
wenzelm@10081 | 41 |
|
wenzelm@10081 | 42 |
Note that the configure script is only required for systems that do |
wenzelm@10081 | 43 |
not have bash and perl in the canonical places (/bin/bash and |
wenzelm@10081 | 44 |
/usr/bin/perl). |
wenzelm@10081 | 45 |
|
wenzelm@10081 | 46 |
The install utility creates global references to the present Isabelle |
wenzelm@10081 | 47 |
installation, enabling users to invoke the Isabelle executables |
wenzelm@10081 | 48 |
without explicit path names. Incidently, this is the only place where |
wenzelm@10081 | 49 |
a static reference to [ISABELLE_HOME] is created; thus isatool install |
wenzelm@10081 | 50 |
has to be run again whenever the Isabelle distribution is moved later. |
wenzelm@10081 | 51 |
|
wenzelm@10081 | 52 |
|
wenzelm@10081 | 53 |
Compiling logics |
wenzelm@10081 | 54 |
---------------- |
wenzelm@10081 | 55 |
|
wenzelm@10081 | 56 |
The Isabelle.tar.gz archive already contains all Isabelle sources (and |
wenzelm@10081 | 57 |
documentation). Precompiled object-logics are provided for |
wenzelm@10081 | 58 |
convenience. |
wenzelm@10081 | 59 |
|
wenzelm@10081 | 60 |
Assuming proper configuration of the underlying ML system |
wenzelm@10081 | 61 |
(cf. Isabelle's etc/settings), further object-logics may be compiled |
wenzelm@10081 | 62 |
like this: |
wenzelm@10081 | 63 |
|
wenzelm@10081 | 64 |
[ISABELLE_HOME]/build FOL |
wenzelm@10081 | 65 |
|
wenzelm@10081 | 66 |
Special object-logic targets may be specified as follows: |
wenzelm@10081 | 67 |
|
kleing@14024 | 68 |
[ISABELLE_HOME]/build -m HOL-Complex HOL |
wenzelm@10081 | 69 |
|
wenzelm@10081 | 70 |
|
wenzelm@10081 | 71 |
2) User installation |
wenzelm@8809 | 72 |
-------------------- |
wenzelm@2759 | 73 |
|
wenzelm@10081 | 74 |
Running the Isabelle binaries |
wenzelm@10081 | 75 |
----------------------------- |
wenzelm@2759 | 76 |
|
wenzelm@10081 | 77 |
Users may invoke the Isabelle binaries (isatool, isabelle, Isabelle) |
wenzelm@8809 | 78 |
directly from their location within the distribution directory |
wenzelm@8809 | 79 |
[ISABELLE_HOME] like this: |
wenzelm@8809 | 80 |
|
wenzelm@8809 | 81 |
[ISABELLE_HOME]/bin/isabelle HOL |
wenzelm@8809 | 82 |
|
wenzelm@10081 | 83 |
This starts an interactive Isabelle session within the current text |
wenzelm@10081 | 84 |
terminal. [ISABELLE_HOME]/bin may be put into the shell's search |
wenzelm@10081 | 85 |
PATH. An alternative is to create global references to the Isabelle |
wenzelm@10081 | 86 |
executables as follows: |
wenzelm@8809 | 87 |
|
wenzelm@8809 | 88 |
[ISABELLE_HOME]/bin/isatool install -p ~/bin |
wenzelm@8809 | 89 |
|
wenzelm@10081 | 90 |
Note that the site-wide Isabelle installation may already provide |
wenzelm@10081 | 91 |
Isabelle executables in some global bin directory (such as |
wenzelm@10081 | 92 |
/usr/local/bin). |
wenzelm@8809 | 93 |
|
wenzelm@8809 | 94 |
|
wenzelm@10081 | 95 |
Isabelle as KDE application |
wenzelm@10081 | 96 |
--------------------------- |
wenzelm@8809 | 97 |
|
kleing@14009 | 98 |
Users may install an Isabelle application icon on the KDE desktop as |
kleing@14009 | 99 |
follows: |
kleing@14009 | 100 |
|
kleing@14009 | 101 |
[ISABELLE_HOME]/bin/isatool install -k 1 |
kleing@14009 | 102 |
|
kleing@14009 | 103 |
This will install the KDE icon in ~/.kde |
wenzelm@8809 | 104 |
|
wenzelm@11126 | 105 |
[ISABELLE_HOME]/bin/isatool install -k 2 |
wenzelm@8809 | 106 |
|
kleing@14009 | 107 |
does the same, but in ~/.kde2 |
kleing@14009 | 108 |
|
wenzelm@10029 | 109 |
Clicking on Isabelle will invoke the interface wrapper script (capital |
wenzelm@10081 | 110 |
Isabelle), which is usually configured to run Proof General (cf. the |
wenzelm@10081 | 111 |
ISABELLE_INTERFACE setting). Additional options may be passed to |
wenzelm@10029 | 112 |
Isabelle by editing the application's command line using the standard |
wenzelm@10081 | 113 |
KDE properties editing facilities. |
wenzelm@2759 | 114 |
|
wenzelm@2759 | 115 |
|
wenzelm@2759 | 116 |
$Id$ |