8 The following source and binary packages of <!-- _GP_ distname -->
9 provide everything required for easy installation of the full Isabelle
10 working environment on common Unix platforms.
14 A <em>minimal</em> Isabelle installation requires only <tt>bash</tt>
15 and <tt>perl</tt> (usually provided by the operating system), and a
16 suitable implementation of Standard ML (e.g. Poly/ML as provided
21 A <em>comfortable</em> Isabelle working environment demands further
22 user interface support, as provided by <a
23 href="http://www.dcs.ed.ac.uk/home/proofgen/">Proof General</a>
24 together with the (optional) <a
25 href="http://www.fmi.uni-passau.de/~wedler/x-symbol/">X-Symbol</a>
26 package. Both of these require a recent version of <a
27 href="http://www.xemacs.org">XEmacs</a> (e.g. version 21).
31 Below we offer tuned distributions of Proof General and X-Symbol, such
32 that <em>no manual configuration</em> is required when used with
33 Isabelle. (In case that the original distributions are used instead,
34 refer to their included instructions for installation details.) Note
35 that XEmacs-21 is not included here -- most operating system
36 distributions already provide suitable packages, although not
42 <h2>(1) Linux/x86 systems with RPM</h2>
44 This version of the <!-- _GP_ distname --> distribution is for
45 Linux/x86 systems with RPM package management, as used by most Linux
46 distributions. Note that <tt>rpm</tt> requires root user access for
51 <!-- _GP_ setdowncolor("\"#E0E0E0\"") -->
53 <table border="0" cellspacing="5" cellpadding="4" width="520">
54 <!-- _GP_ download("Poly/ML system", "contrib/polyml.i386.rpm", "../..") -->
55 <!-- _GP_ download("Isabelle main system", "isabelle.rpm", "../..") -->
56 <!-- _GP_ download("Isabelle/HOL image", "isabelle-HOL.i386.rpm", "../..") -->
57 <!-- _GP_ download("Isabelle/HOL-Real image (optional)", "isabelle-HOL-Real.i386.rpm", "../..") -->
58 <!-- _GP_ download("Isabelle/ZF image (optional)", "isabelle-ZF.i386.rpm", "../..") -->
59 <!-- _GP_ download("Isabelle pdf documentation (optional)", "isabelle-pdfdocs.rpm", "../..") -->
60 <!-- _GP_ download("Proof General system (recommended)", "contrib/proofgeneral.rpm", "../..") -->
61 <!-- _GP_ download("X-Symbol package (recommended)", "contrib/xsymbol.rpm", "../..") -->
67 Example installation in <tt>/usr/share</tt> (the default location):
70 rpm -i --prefix /usr/share polyml.i386.rpm
71 rpm -i --prefix /usr/share isabelle.rpm
72 rpm -i --prefix /usr/share isabelle-HOL.i386.rpm
73 rpm -i --prefix /usr/share proofgeneral.rpm
74 rpm -i --prefix /usr/share xsymbol.rpm
80 <h2>(2) Generic Linux/x86 or Solaris/Sparc systems</h2>
82 The following <!-- _GP_ distname --> distribution works for any
83 Linux/x86 or Solaris/Sparc system -- actually only Poly/ML is platform
84 dependent. Installation does not rely on package management; it may
85 be performed by non-root users as well.
89 <!-- _GP_ setdowncolor("\"#E0E0E0\"") -->
91 <table border="0" cellspacing="5" cellpadding="4" width="520">
92 <!-- _GP_ download("Poly/ML base system", "contrib/polyml_base.tar.gz", "../..") -->
93 <!-- _GP_ download("Poly/ML module for Linux/x86", "contrib/polyml_x86-linux.tar.gz", "../..") -->
94 <!-- _GP_ download("Poly/ML module for Solaris/Sparc", "contrib/polyml_sparc-solaris.tar.gz", "../..") -->
95 <!-- _GP_ download("Isabelle main system", distname . ".tar.gz", "../..") -->
96 <!-- _GP_ download("Isabelle pdf documentation (optional)", distname . "_pdf.tar.gz", "../..") --> <!-- _GP_ download("Proof General system (recommended)", "contrib/ProofGeneral.tar.gz", "../..") -->
97 <!-- _GP_ download("X-Symbol package (recommended)", "contrib/x-symbol.tar.gz", "../..") -->
103 Example installation in <tt>/usr/local</tt> for Linux/x86:
106 tar -C /usr/local -x -z -f polyml_base.tar.gz
107 tar -C /usr/local -x -z -f polyml_x86-linux.tar.gz
108 tar -C /usr/local -x -z -f <!-- _GP_ distname . ".tar.gz"-->
109 tar -C /usr/local -x -z -f ProofGeneral.tar.gz
110 tar -C /usr/local -x -z -f x-symbol.tar.gz
112 cd <!-- _GP_ "/usr/local/" . distname -->
115 ./bin/isatool install -p /usr/local/bin