1 |
|
2 Isabelle installation notes |
|
3 =========================== |
|
4 |
|
5 1) System installation |
|
6 ---------------------- |
|
7 |
|
8 The Isabelle distribution includes both complete sources and |
|
9 precompiled binary packages for common Unix-like platforms. |
|
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 |
|
20 tar -C /usr/local -xzf polyml.tar.gz |
|
21 tar -C /usr/local -xzf HOL_x86-linux.tar.gz |
|
22 |
|
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 |
|
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]/.. |
|
30 4) /usr/local |
|
31 3) /usr/share |
|
32 5) /opt |
|
33 |
|
34 This may be changed by editing [ISABELLE_HOME]/etc/settings manually. |
|
35 |
|
36 The installation may be finished as follows: |
|
37 |
|
38 cd [ISABELLE_HOME] |
|
39 ./bin/isabelle install -p /usr/local/bin |
|
40 |
|
41 The install utility creates global references to the present Isabelle |
|
42 installation, enabling users to invoke the Isabelle executables |
|
43 without explicit path names. This is the only place where a static |
|
44 reference to [ISABELLE_HOME] is created; thus isabelle install has to |
|
45 be run again whenever the Isabelle distribution is moved later. |
|
46 |
|
47 |
|
48 Compiling logics |
|
49 ---------------- |
|
50 |
|
51 The Isabelle.tar.gz archive already contains all Isabelle sources (and |
|
52 documentation). Precompiled object-logics are provided for |
|
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 |
|
63 [ISABELLE_HOME]/build -m HOL-Algebra HOL |
|
64 |
|
65 |
|
66 2) User installation |
|
67 -------------------- |
|
68 |
|
69 Running the Isabelle binaries |
|
70 ----------------------------- |
|
71 |
|
72 Users may invoke the main Isabelle binaries (isabelle and |
|
73 isabelle-process) directly from their location within the distribution |
|
74 directory [ISABELLE_HOME] like this: |
|
75 |
|
76 [ISABELLE_HOME]/bin/isabelle tty -l HOL |
|
77 |
|
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: |
|
82 |
|
83 [ISABELLE_HOME]/bin/isabelle install -p ~/bin |
|
84 |
|
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). |
|