1 WN1900721 copy from Isabelle2009-1
2 !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
4 Isabelle installation notes
5 ===========================
10 The Isabelle distribution includes both complete sources and
11 precompiled binary packages for common Unix-like platforms.
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:
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
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:
30 1) [ISABELLE_HOME]/contrib
36 This may be changed by editing [ISABELLE_HOME]/etc/settings manually.
38 The installation may be finished as follows:
41 ./bin/isabelle install -p /usr/local/bin
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.
53 The Isabelle.tar.gz archive already contains all Isabelle sources (and
54 documentation). Precompiled object-logics are provided for
57 Assuming proper configuration of the underlying ML system
58 (cf. Isabelle's etc/settings), further object-logics may be compiled
61 [ISABELLE_HOME]/build FOL
63 Special object-logic targets may be specified as follows:
65 [ISABELLE_HOME]/build -m HOL-Algebra HOL
71 Running the Isabelle binaries
72 -----------------------------
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:
78 [ISABELLE_HOME]/bin/isabelle tty -l HOL
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:
85 [ISABELLE_HOME]/bin/isabelle install -p ~/bin
87 Note that the site-wide Isabelle installation may already provide
88 Isabelle executables in some global bin directory (such as