2 Isabelle compilation and installation notes
3 ===========================================
8 After unpacking the Isabelle distribution archive (using tar and gzip)
9 you are left with some directory IsabelleYY-X. You may install this
10 anywhere, but please just *not* as ~/isabelle!!!
12 The place where you put the contents of IsabelleYY-X will be referred
13 to as [ISABELLE_HOME] subsequently.
19 There are some minor adaptions to be made of the Isabelle distribution
20 to your system environment. Simply type:
25 This does not store any references to [ISABELLE_HOME]. You may safely
26 move the system later, without running ./configure again.
29 ML system settings and compilation
30 ----------------------------------
32 Before actual compilation you have to tell Isabelle about your
33 Standard ML system. These settings reside in ./etc/settings, which
34 may be also overridden by ~/isabelle/etc/settings. There are already
35 various sample configurations in ./etc/settings commented out.
37 To build the core Isabelle/Pure and the default object-logic, just
42 More object-logics can be made similarly:
50 Provided that compilation was successful, you can now run something
53 [ISABELLE_HOME]/bin/isabelle FOL
55 This starts an interactive Isabelle session within your current text
56 terminal. You may want to put [ISABELLE_HOME]/bin into your shell's
59 Please do *not* copy (or link) the Isabelle scripts anywhere else, or
60 they just won't work! If you really feel the urge to install
61 independent Isabelle binaries anywhere else do it like this:
63 [ISABELLE_HOME]/bin/isatool install -p /usr/local/bin