Reorganisation of registration code.
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; 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:
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:
39 ./bin/isatool install -p /usr/local/bin
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. Incidently, this is the only place where
44 a static reference to [ISABELLE_HOME] is created; thus isatool install
45 has to be run again whenever the Isabelle distribution is moved later.
51 The Isabelle.tar.gz archive already contains all Isabelle sources (and
52 documentation). Precompiled object-logics are provided for
55 Assuming proper configuration of the underlying ML system
56 (cf. Isabelle's etc/settings), further object-logics may be compiled
59 [ISABELLE_HOME]/build FOL
61 Special object-logic targets may be specified as follows:
63 [ISABELLE_HOME]/build -m HOL-Algebra HOL
69 Running the Isabelle binaries
70 -----------------------------
72 Users may invoke the Isabelle binaries (isatool, isabelle, Isabelle)
73 directly from their location within the distribution directory
74 [ISABELLE_HOME] like this:
76 [ISABELLE_HOME]/bin/isabelle HOL
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:
83 [ISABELLE_HOME]/bin/isatool install -p ~/bin
85 Note that the site-wide Isabelle installation may already provide
86 Isabelle executables in some global bin directory (such as