--- a/Admin/website/TODO Mon Jun 06 11:30:57 2005 +0200
+++ b/Admin/website/TODO Mon Jun 06 12:17:59 2005 +0200
@@ -1,10 +1,24 @@
For the next release:
-- integrate into makedist (Florian), deploy on Munich site
+- use "//" paths for alle internal static resources, due to link consistency
+
+- integrate into makedist-chain (Florian)
+
+- more concise installation instructions for MaxOS X
+
+- make preview second section in "overview"
+
+- centralize scattered project partners informations at "community"
+
+- move projects from "overview" to "community"
+
+- reduce prominence of license issue at "overview"
In the mid-time:
--
+- clarify relationship of "overview" and "logics":
+ * overview: Isabelle/HOL
+ * logics: Isabelle system
Visionary:
--- a/Admin/website/build/pypager.py Mon Jun 06 11:30:57 2005 +0200
+++ b/Admin/website/build/pypager.py Mon Jun 06 12:17:59 2005 +0200
@@ -105,11 +105,23 @@
handler.endElement(wrapTagname)
handler.endElement(u"li")
+ def downloadLink(self, handler, **args):
+
+ target = args[u"target"].encode("latin-1")
+ targetReal = self._pc.absDstPathOf(target)
+ title = args.get(u"title", unicode(posixpath.split(targetReal)[1], 'latin-1'))
+ size = os.stat(targetReal).st_size
+ handler.startElement(u"a", {
+ u"href": target
+ })
+ handler.characters(title)
+ handler.endElement(u"a")
+
def downloadCells(self, handler, **args):
target = args[u"target"].encode("latin-1")
targetReal = self._pc.absDstPathOf(target)
- title = args.get(u"title", unicode(posixpath.split(target)[0], 'latin-1'))
+ title = args.get(u"title", unicode(posixpath.split(targetReal)[1], 'latin-1'))
size = os.stat(targetReal).st_size
handler.startElement(u"td", {})
handler.startElement(u"a", {
--- a/Admin/website/dist/download.html Mon Jun 06 11:30:57 2005 +0200
+++ b/Admin/website/dist/download.html Mon Jun 06 12:17:59 2005 +0200
@@ -4,7 +4,7 @@
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
- <title>Download</title>
+ <title>Packages</title>
<?include file="//include/htmlheader.include.html"?>
</head>
@@ -37,7 +37,7 @@
<p>For the curious we provide a nightly generated
CVS <a href="http://isabelle.in.tum.de/devel/">development snapshot</a> of
- Isabelle.</p>
+ Isabelle. <em>Use at your own risk!</em></p>
<h2>Past releases</h2>
--- a/Admin/website/dist/installation.html Mon Jun 06 11:30:57 2005 +0200
+++ b/Admin/website/dist/installation.html Mon Jun 06 12:17:59 2005 +0200
@@ -15,86 +15,145 @@
<div class="hr"><hr/></div>
<div id="content">
- <h2>Prerequisites</h2>
-
- <p>Isabelle runs on common Unix platforms (Linux, Solaris, etc.).
- Below we provide also some <a href="#other_platforms">hints</a>
- on how to use Isabelle on other, not-quite-Unix platforms.</p>
-
- <p>
- The packages available from our <a href="download.html">download page</a>
- expect the following software to be installed:
- </p>
-
- <ul>
- <li>bash 1.x or 2.x</li>
- <li>Perl 5.x</li>
- <li>optionally, XEmacs 21 or Emacs 21 with mule support (for ProofGeneral)</li>
- <li>optionally, Java 1.1 or above (for theory graph browsing)</li>
- </ul>
-
- <p>
- Our download page includes packages for a suitable implementation of Standard ML
- (<a href="http://www.polyml.org">Poly/ML</a>) and
- <a
- href="http://proofgeneral.inf.ed.ac.uk/">ProofGeneral</a>
- (please <a
- href="http://proofgeneral.inf.ed.ac.uk/register">register</a>). The
- Proof General distribution now already includes the <a
- href="http://x-symbol.sourceforge.net">X-Symbol</a> package,
- there is no need to download it separately.
- </p>
-
- <h2>Installation</h2>
+ <h2>General</h2>
- <p>In fact, there is no
- installation required. Users may just unpack all required packages within the
- same directory. The default settings of Isabelle should be reasonable for
- most circumstances.</p>
-
- <p>A typical Linux/x86 site installation of Isabelle/HOL works as follows:</p>
- <ul>
- <li>By using GNU <tt class="shellcmd">tar</tt>, the archives are uncompressed and unpacked into the
- <tt class="shellcmd">/usr/local</tt> directory (this location may be changed to anything
- appropriate):
- <ul class="shellcmd">
- <li>tar -C /usr/local -xzf <?value key="distname"?>.tar.gz</li>
- <li>tar -C /usr/local -xzf ProofGeneral.tar.gz</li>
- <li>tar -C /usr/local -xzf polyml_base.tar.gz</li>
- <li>tar -C /usr/local -xzf polyml_x86-linux.tar.gz</li>
- <li>tar -C /usr/local -xzf HOL_x86-linux.tar.gz</li>
- </ul>
- </li>
- <li>
- Users may now invoke Isabelle without further ado, e.g. run the main
- executable <tt class="shellcmd">/usr/local/Isabelle/bin/Isabelle</tt> to launch the Proof
- General interface for Isabelle/Isar. 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>
+ <p>
+ Isabelle runs on common Unix platforms.
+ For Linux and Solaris, we provide ready-to-install bundles;
+ for other Unices, Isabelle has to be built from scratch.
+ We provide also some hints on how to use Isabelle on other, not-quite-Unix platforms.
+ </p>
+
+ <p>
+ A usable Isabelle system consists of the following components:
+ </p>
+
+ <ul>
+ <li>a suitable Standard ML environment</li>
+ <li>the Isabelle system itself, including the desired object logic(s)
+ (e. g. HOL)</li>
+ <li>the ProofGeneral user interface</li>
+ </ul>
+
+ <p>Optionally, theory graph browsing may be used if a Java JRE 1.1 or above
+ is installed.</p>
+
+ <p>For operating-system-specific instructions:</p>
+
+ <ul>
+ <li><a href="#install_linux">Linux (x86)</a></li>
+ <li><a href="#install_solaris">Solaris (sparc)</a></li>
+ <li><a href="#install_darwin">MacOS X / Darwin</a></li>
+ <li><a href="#install_cygwin">Windows / Cygwin</a></li>
+ </ul>
+
+ <h2 id="#install_linux">Linux</h2>
+
+ <p>Commonly, an installation of Isabelle could work as follows:</p>
+
+ <ul>
+ <li>Ensure that your system has a running XEmacs 21 or Emacs 21
+ with mule support (for ProofGeneral)</li>
+ <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 you 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>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2004.tar.gz"?></li>
+ <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/ProofGeneral.tar.gz"?></li>
+ <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_base.tar.gz"?></li>
+ <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_x86-linux.tar.gz"?></li>
+ <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_x86-linux.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>
- <p>For more information, see the file <a href="//dist/packages/Isabelle/INSTALL">INSTALL</a> included in
- <?value key="distname"?>.tar.gz.</p>
+ <p>For more information, see the file <a href="//dist/packages/Isabelle/INSTALL">INSTALL</a>.</p>
+
+ <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>
+ </ul>
+
+ <p>Then, an installation on Solaris is analogous to Linux:</p>
- <h2 id="other_platforms">Other platforms</h2>
-
- <p>Although Isabelle is natively designed for Unix environments,
- it may also run under similar, Unix-like platforms. The
- following installation instructions are hints contributed by
- Isabelle users. Please feel free to contact us for any suggestions,
- corrections or improvements.</p>
-
- <ul>
- <li><a href="installation_notes_macosx.html">Installation notes for Mac OS
- X</a></li>
-
- <li><a href="installation_notes_cygwin.html">Installation notes for
- Cygwin/Windows</a></li>
- </ul>
+ <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 you 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_sparc-solaris.tar.gz"?></li>
+ <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_sparc-solaris.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>
+
+ <p>For more information, see the file <a href="//dist/packages/Isabelle/INSTALL">INSTALL</a>.</p>
+
+ <h2 id="#install_darwin">MaxOS / Darwin</h2>
+
+ <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>
+
+ <h2 id="#install_cygwin">Windows / Cygwin</h2>
+
+ <p>See <a href="installation_notes_cygwin.html">Installation notes for
+ Cygwin/Windows</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>
</div>
<div class="hr"><hr/></div>
--- a/Admin/website/include/navigation_dist.include.html Mon Jun 06 11:30:57 2005 +0200
+++ b/Admin/website/include/navigation_dist.include.html Mon Jun 06 12:17:59 2005 +0200
@@ -6,7 +6,7 @@
<ul>
<?navitem target="index.html" title="Mirrors" ?>
<?navitem target="installation.html" title="Installation" ?>
- <?navitem target="download.html" title="Download" ?>
+ <?navitem target="download.html" title="Packages" ?>
<?navitem target="documentation.html" title="Documentation" ?>
<?navitem target="others.html" title="Other links" ?>
</ul>
--- a/Admin/website/index.html Mon Jun 06 11:30:57 2005 +0200
+++ b/Admin/website/index.html Mon Jun 06 12:17:59 2005 +0200
@@ -49,8 +49,7 @@
<p>New features in the upcoming Isabelle 2005 will include</p>
<ul>
<li>New commands for instantiating locales</li>
- <li>New command for finding matching rewrite rules</li>
- <li>Finding theorems by term patterns</li>
+ <li>New command for finding theorems (by term patterns, as intro/elim/simp rules, etc.)</li>
<li>New automatic transitivity reasoner</li>
<li>New command for ad-hoc theory viewing and printing</li>
<li>Much extended and improved theory of finite sets</li>
--- a/Admin/website/overview.html Mon Jun 06 11:30:57 2005 +0200
+++ b/Admin/website/overview.html Mon Jun 06 12:17:59 2005 +0200
@@ -35,13 +35,20 @@
(University of Cambridge, UK) and Tobias Nipkow (Technical
University of Munich, Germany).</p>
- <h2>What Isabelle offers</h2>
+ <h2>Preview on Isabelle</h2>
- <a href="//img/isabelle_pg_screenshot_big.png">
+ <a href="//media/pg_preview.mov">
<img class="left" src="//img/isabelle_pg_screenshot_small.png" alt="Sreenshot "
width="250" height="277" />
</a>
+ <p>Here is a <a href="//media/pg_preview.mov">hyperlinked preview</a> demonstrating
+ Isabelle and ProofGeneral, in <a href="http://www.apple.com/quicktime/download/">QuickTime
+ format</a>, and also as a <a href="//media/pg_preview.pdf">non-hyperlinked preview</a> in PDF.</p>
+ <br clear="all"/>
+
+ <h2>What Isabelle offers</h2>
+
<p>Isabelle provides excellent notational support: new notations
can be introduced, using normal mathematical symbols. Proofs can
be written in a structured notation based upon traditional proof
@@ -75,17 +82,11 @@
eases the task of writing and maintaining proof scripts.</p>
<br clear="all" />
- <h2>Preview</h2>
-
- <p>We provide a <a href="media/pg_preview.mov">hyperlinked preview</a> demonstrating
- Isabelle and ProofGeneral, in <a href="http://www.apple.com/quicktime/download/">QuickTime
- format</a>, and also as a <a href="media/pg_preview.pdf">non-hyperlinked preview</a> in PDF.</p>
-
<p>Ample <a href="dist/documentation.html">documentation</a> is available
about using Isabelle and its inner concepts, including a
<a href="http://www4.in.tum.de/~nipkow/LNCS2283/">Tutorial</a> published by
Springer-Verlag.</p>
-
+
<h2>Projects</h2>
<p>There is an (incomplete) list of past and present <a href=