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