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