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_x86-linux.tar.gz
21 tar -C /usr/local -xzf HOL_x86-linux.tar.gz
23 The install prefix given above may be changed as appropriate. By
24 default the ML system (and other contributed packages) are expected in
25 any of the following locations:
27 1) [ISABELLE_HOME]/contrib
33 This may be changed by editing [ISABELLE_HOME]/etc/settings manually.
35 The installation may be finished as follows:
38 ./bin/isatool install -p /usr/local/bin
40 The install utility creates global references to the present Isabelle
41 installation, enabling users to invoke the Isabelle executables
42 without explicit path names. Incidently, this is the only place where
43 a static reference to [ISABELLE_HOME] is created; thus isatool install
44 has to be run again whenever the Isabelle distribution is moved later.
50 The Isabelle.tar.gz archive already contains all Isabelle sources (and
51 documentation). Precompiled object-logics are provided for
54 Assuming proper configuration of the underlying ML system
55 (cf. Isabelle's etc/settings), further object-logics may be compiled
58 [ISABELLE_HOME]/build FOL
60 Special object-logic targets may be specified as follows:
62 [ISABELLE_HOME]/build -m HOL-Algebra HOL
68 Running the Isabelle binaries
69 -----------------------------
71 Users may invoke the Isabelle binaries (isatool, isabelle, Isabelle)
72 directly from their location within the distribution directory
73 [ISABELLE_HOME] like this:
75 [ISABELLE_HOME]/bin/isabelle HOL
77 This starts an interactive Isabelle session within the current text
78 terminal. [ISABELLE_HOME]/bin may be put into the shell's search
79 PATH. An alternative is to create global references to the Isabelle
80 executables as follows:
82 [ISABELLE_HOME]/bin/isatool install -p ~/bin
84 Note that the site-wide Isabelle installation may already provide
85 Isabelle executables in some global bin directory (such as