2 Isabelle installation notes
3 ===========================
8 The Isabelle distribution includes both complete sources and
9 precompiled binary packages for common Unix platforms.
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:
19 tar -C /usr/local -xzf Isabelle.tar.gz
20 tar -C /usr/local -xzf polyml_base.tar.gz
21 tar -C /usr/local -xzf polyml_x86-linux.tar.gz
22 tar -C /usr/local -xzf HOL_x86-linux.tar.gz
24 The install prefix given above may be changed as appropriate. By
25 default the ML system (and other contributed packages) are expected in
26 any of the following locations:
28 1) [ISABELLE_HOME]/contrib
34 This may be changed by editing [ISABELLE_HOME]/etc/settings manually.
36 The installation may be finished as follows:
40 ./bin/isatool install -p /usr/local/bin
42 Note that the configure script is only required for systems that do
43 not have bash and perl in the canonical places (/bin/bash and
46 The install utility creates global references to the present Isabelle
47 installation, enabling users to invoke the Isabelle executables
48 without explicit path names. Incidently, this is the only place where
49 a static reference to [ISABELLE_HOME] is created; thus isatool install
50 has to be run again whenever the Isabelle distribution is moved later.
56 The Isabelle.tar.gz archive already contains all Isabelle sources (and
57 documentation). Precompiled object-logics are provided for
60 Assuming proper configuration of the underlying ML system
61 (cf. Isabelle's etc/settings), further object-logics may be compiled
64 [ISABELLE_HOME]/build FOL
66 Special object-logic targets may be specified as follows:
68 [ISABELLE_HOME]/build -m HOL-Complex HOL
74 Running the Isabelle binaries
75 -----------------------------
77 Users may invoke the Isabelle binaries (isatool, isabelle, Isabelle)
78 directly from their location within the distribution directory
79 [ISABELLE_HOME] like this:
81 [ISABELLE_HOME]/bin/isabelle HOL
83 This starts an interactive Isabelle session within the current text
84 terminal. [ISABELLE_HOME]/bin may be put into the shell's search
85 PATH. An alternative is to create global references to the Isabelle
86 executables as follows:
88 [ISABELLE_HOME]/bin/isatool install -p ~/bin
90 Note that the site-wide Isabelle installation may already provide
91 Isabelle executables in some global bin directory (such as
95 Isabelle as KDE application
96 ---------------------------
98 Users may install an Isabelle application icon on the KDE desktop as
101 [ISABELLE_HOME]/bin/isatool install -k 1
103 This will install the KDE icon in ~/.kde
105 [ISABELLE_HOME]/bin/isatool install -k 2
107 does the same, but in ~/.kde2
109 Clicking on Isabelle will invoke the interface wrapper script (capital
110 Isabelle), which is usually configured to run Proof General (cf. the
111 ISABELLE_INTERFACE setting). Additional options may be passed to
112 Isabelle by editing the application's command line using the standard
113 KDE properties editing facilities.