--- a/Admin/website/build/localconf.at.template.mak Mon Jun 06 14:14:27 2005 +0200
+++ b/Admin/website/build/localconf.at.template.mak Mon Jun 06 15:09:47 2005 +0200
@@ -11,7 +11,7 @@
TIDY=tidy
# dirs to copy to build target
-STATICDIRS=img media dist/css dist/img dist/packages
+STATICDIRS=img media dist/css dist/img dist/packages dist/misc
# build target (attention: ~ will not work!)
OUTPUTROOT=/usr/proj/isabelle-repository/www
--- a/Admin/website/build/localconf.sun.template.mak Mon Jun 06 14:14:27 2005 +0200
+++ b/Admin/website/build/localconf.sun.template.mak Mon Jun 06 15:09:47 2005 +0200
@@ -11,7 +11,7 @@
TIDY=tidy
# dirs to copy to build target
-STATICDIRS=img media dist/css dist/img
+STATICDIRS=img media dist/css dist/img dist/packages dist/misc
# build target (attention: ~ will not work!)
OUTPUTROOT=$(HOME)/isabelle_website
--- a/Admin/website/dist/installation.html Mon Jun 06 14:14:27 2005 +0200
+++ b/Admin/website/dist/installation.html Mon Jun 06 15:09:47 2005 +0200
@@ -47,7 +47,7 @@
<li><a href="#install_cygwin">Windows / Cygwin</a></li>
</ul>
- <h2 id="#install_linux">Linux</h2>
+ <h2 id="install_linux">Linux</h2>
<p>Commonly, an installation of Isabelle could work as follows:</p>
@@ -61,7 +61,7 @@
either from our <a href="download.html">package page</a> or from the
links below. When you download ProofGeneral, please
<a href="http://proofgeneral.inf.ed.ac.uk/register">register</a></li>
- <li>Likewise download the compiled image(s) of you desired object logic(s)</li>
+ <li>Likewise download the compiled image(s) of your desired object logic(s)</li>
<li>Unpack the archives to an appropriate location, e. g.
<tt class="shellcmd">/usr/local</tt>:
<ul class="shellcmd">
@@ -88,16 +88,16 @@
<p>For more information, see the file <a href="//dist/packages/Isabelle/INSTALL">INSTALL</a>.</p>
- <h2 id="#install_solaris">Solaris</h2>
+ <h2 id="install_solaris">Solaris</h2>
<p>Before you start, ensure the following for your system:</p>
<ul>
- <li>running XEmacs 21 or Emacs 21
- with mule support (for ProofGeneral)</li>
<li>GNU bash 2.x</li>
<li>perl 5.x</li>
<li>GNU tar 1.13 or higher</li>
<li>GNU gzip 1.3 or higher</li>
+ <li>running XEmacs 21 or Emacs 21
+ with mule support (for ProofGeneral)</li>
</ul>
<p>Then, an installation on Solaris is analogous to Linux:</p>
@@ -110,7 +110,7 @@
either from our <a href="download.html">package page</a> or from the
links below. When you download ProofGeneral, please
<a href="http://proofgeneral.inf.ed.ac.uk/register">register</a></li>
- <li>Likewise download the compiled image(s) of you desired object logic(s)</li>
+ <li>Likewise download the compiled image(s) of your desired object logic(s)</li>
<li>Unpack the archives to an appropriate location, e. g.
<tt class="shellcmd">/usr/local</tt>:
<ul class="shellcmd">
@@ -137,16 +137,53 @@
<p>For more information, see the file <a href="//dist/packages/Isabelle/INSTALL">INSTALL</a>.</p>
- <h2 id="#install_darwin">MaxOS / Darwin</h2>
+ <h2 id="install_darwin">MaxOS / Darwin</h2>
+
+ <p>Before you start, ensure the following for your system:</p>
+ <ul>
+ <li>running MacOS X 10.2.2 or higher</li>
+ <li>running XEmacs 21 or Emacs 21 with mule support (for ProofGeneral)
+ – for further reference, see the
+ <a href="installation_macos_emacs.html">MacOS X Emacs hints</a>
+ </li>
+ </ul>
+
+ <p>Then, an installation on Darwin is analogous to Linux:</p>
- <p>See <a href="installation_notes_macosx.html">Installation notes for MacOS X</a>.</p>
- <p>Those
- installation instructions are hints contributed by
- Isabelle users. Please feel free to contact us for any suggestions,
- corrections or improvements.</p>
- <p>Ready-to-install bundles are available from our <a href="download.html">package page</a>.</p>
+ <ul>
+ <li>Get the packages for <a href="http://www.polyml.org">Poly/ML</a>,
+ <a href="http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a> (including
+ the Emacs <a href="http://x-symbol.sourceforge.net">X-Symbol</a> package)
+ and Isabelle,
+ either from our <a href="download.html">package page</a> or from the
+ links below. When you download ProofGeneral, please
+ <a href="http://proofgeneral.inf.ed.ac.uk/register">register</a></li>
+ <li>Likewise download the compiled image(s) of your desired object logic(s)</li>
+ <li>Unpack the archives to an appropriate location, e. g.
+ <tt class="shellcmd">/usr/local</tt>:
+ <ul class="shellcmd">
+ <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2004.tar.gz"?></li>
+ <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/ProofGeneral.tar.gz"?></li>
+ <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_base.tar.gz"?></li>
+ <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_ppc-darwin.tar.gz"?></li>
+ <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_ppc-darwin.tar.gz"?></li>
+ </ul>
+ </li>
+ <li>Under most circumstances, the default settings of Isabelle should be reasonable for
+ invoking Isabelle/ProofGeneral without further ado:
+ <ul class="shellcmd">
+ <li>/usr/local/Isabelle/bin/Isabelle</li>
+ </ul>
+ Note that there is a separate option in
+ the Proof General <em>Options</em> menu to enable X-Symbol.
+ </li>
+ <li>If Emacs appears to hang when the prover process is started, see the
+ <a href="http://proofgeneral.inf.ed.ac.uk/FAQ">ProofGeneral FAQ</a> for
+ advice.
+ </li>
+ </ul>
- <h2 id="#install_cygwin">Windows / Cygwin</h2>
+ <h2 id="install_cygwin">Windows / Cygwin</h2>
<p>See <a href="installation_notes_cygwin.html">Installation notes for
Cygwin/Windows</a>.</p>
Binary file Admin/website/dist/misc/isabelle_droplet.dmg has changed