New development pages added, more links

8 files changed, 295 insertions, 103 deletions

diff --git a/html/devel.phtml b/html/devel.phtml
index 4cc3ef6e..c8b9abcb 100644
--- a/html/devel.phtml
+++ b/html/devel.phtml
@@ -1,98 +1,33 @@
-<?php  
-  require('functions.php3');
-  small_header("Proof General Development"); 
-  ?>
-
-<p>
-Here is the latest pre-release of Proof General.  For developers,
-it is also available as a complete archive, including
-forthcoming support for more proof assistants.
-</p>
 <p>
-Pre-releases of Proof General may be buggy as we add new features and
-experiment with them.  Nonetheless, we welcome bug reports.  But
-please make sure you are using the current pre-release before
-reporting problems.
+Proof General follows an open development method.  
+<br>
+We welcome code contributions, suggestions, and bug reports, from all
+users and hackers!
 </p>
 
-<!-- WARNING!  Line below automatically edited by makefile. -->
-<h2><a name="prerel">Pre-release: ProofGeneral-3.1pre000209</a></h2>
-<!-- End Warning. -->
-
-<p>
-Check the 
-<!-- WARNING!  Line below automatically edited by makefile. -->
-<?php fileshow("ProofGeneral-3.1pre000209/CHANGES","CHANGES"); ?> file
-<!-- End Warning. -->
-for a summary of changes since the last stable version, and
-the planned changes to come.
-</p>
 <ul>
-<!-- WARNING!  Lines below automatically edited by makefile. -->
-  <li> gzip'ed tar file: 
-      <?php download_link("ProofGeneral-3.1pre000209.tar.gz") ?>
-  </li>
-  <li> Linux RPM package 
-      <?php download_link("ProofGeneral-3.1pre000209-1.noarch.rpm") ?>
-     <br>
-     You probably don't need the 
-    <?php download_link("ProofGeneral-3.1pre000209-1.src.rpm","source RPM") ?>.
-  </li>
-<!-- End Warning. -->
+<li>
+Download the current <a href="develdownload.phtml">development release</a>.
+</li>
 </ul>
-
-
-<h2><a name="devel">Complete Archive of ProofGeneral-3.1pre000209</a></h2>
-
-<p>
-This archive is a snapshot from our CVS repository. 
-</p>
 <ul>
-  <li> gzip'ed tar file: 
-<!-- WARNING!  Line below automatically edited by makefile. -->
-      <?php download_link("ProofGeneral-3.1pre000209-devel.tar.gz") ?>
-<!-- End Warning. -->
-  </li>
+<li>
+Read the Proof General white paper (available soon)
+</li>
 </ul>
-<p>
-What's the difference from the working version above?
-The complete archive also includes:
-</p>
 <ul>
-  <li> provisional instantiations of Proof General to new provers <br>
-	(mentioned in the 
-   <!-- WARNING!  Line below automatically edited by makefile. -->
-  <?php fileshow("ProofGeneral-3.1pre000209/CHANGES","CHANGES"); ?> file),
-   <!-- End Warning. -->
-  </li>
-  <li> the 
-   <!-- WARNING!  Line below automatically edited by makefile. -->
-   <?php fileshow("ProofGeneral-3.1pre000209/todo","low-level list of things to do"); ?>
-   <!-- End Warning. -->
-   and the detailed
-   <!-- WARNING!  Line below automatically edited by makefile. -->
-   <?php fileshow("ProofGeneral-3.1pre000209/ChangeLog","ChangeLog"); ?>,
-   <!-- End Warning. -->
- </li>
-  <li> developer's Makefile used to generate documentation files <br>
-       and the release itself from our CVS repository,  </li>
-  <li> some test files, </li>
-  <li> sources for some of the images, 
-  <li> the web pages.  
+<li>
+Take a look at the Proof General <a href="projects.phtml">project proposals</a>.
+</li>
 </ul>
-<p>
-Note: there are no pre-built documentation files in the developer's
-release, because developers should have the right tools!
-</p>
-<p>
-You probably <em>don't</em> need to download this if you're only
-interested in hacking the Emacs lisp part of the program for
-a prover that is currently supported.  But you may
-still like to check the latest
-<!-- WARNING!  Line below automatically edited by makefile. -->
-<?php fileshow("ProofGeneral-3.1pre000209/todo","low-level to-do list"); ?>.
-<!-- End Warning. -->
-</p>
+<ul>
+<li>
+<?php hlink("feedback.phtml","Send us a message ","Feedback form")?>
+about any development issues.
+</li>
+</ul>
+
+<h2><a name="develmail">Developers Mailing List</a></h2>
 
 <p>
 We have a mailing list for developers, at
@@ -108,12 +43,8 @@ with the words "<tt>subscribe proofgeneral-devel</tt>"
 </p>
 
 <p>
-If you are interested in developing the core of Proof General,
-we can make our CVS repository accessible to you.  Please 
-<a href="feedback.phtml">ask</a>.
+If you are interested in becoming an official developer of Proof
+General, we can make our CVS repository accessible to you.  Please 
+<a href="feedback.phtml">ask here</a>.
 </p>
 
-<?php
-   click_to_go_back();
-   footer();
-?>
diff --git a/html/develdownload.phtml b/html/develdownload.phtml
new file mode 100644
index 00000000..b6527a50
--- /dev/null
+++ b/html/develdownload.phtml
@@ -0,0 +1,101 @@
+<?php  
+  require('functions.php3');
+  small_header("Proof General Development Release"); 
+  ?>
+
+<p>
+Here is the latest pre-release of Proof General, made available
+for those who wish to test the latest features or bug fixes.  
+For developers, this release is also available as a complete archive,
+including forthcoming support for more proof assistants.
+</p>
+<p>
+Pre-releases of Proof General may be buggy as we add new features and
+experiment with them.  Nonetheless, we welcome bug reports.  But
+please make sure you are using the current pre-release before
+reporting problems.
+</p>
+
+<!-- WARNING!  Line below automatically edited by makefile. -->
+<h2><a name="prerel">Pre-release: ProofGeneral-3.1pre000209</a></h2>
+<!-- End Warning. -->
+
+<p>
+Check the 
+<!-- WARNING!  Line below automatically edited by makefile. -->
+<?php fileshow("ProofGeneral-3.1pre000209/CHANGES","CHANGES"); ?> file
+<!-- End Warning. -->
+for a summary of changes since the last stable version, and
+the planned changes to come.
+</p>
+<ul>
+<!-- WARNING!  Lines below automatically edited by makefile. -->
+  <li> gzip'ed tar file: 
+      <?php download_link("ProofGeneral-3.1pre000209.tar.gz") ?>
+  </li>
+  <li> Linux RPM package 
+      <?php download_link("ProofGeneral-3.1pre000209-1.noarch.rpm") ?>
+     <br>
+     You probably don't need the 
+    <?php download_link("ProofGeneral-3.1pre000209-1.src.rpm","source RPM") ?>.
+  </li>
+<!-- End Warning. -->
+</ul>
+
+
+<h2><a name="devel">Complete Archive of ProofGeneral-3.1pre000209</a></h2>
+
+<p>
+This archive is a snapshot from our CVS repository. 
+</p>
+<ul>
+  <li> gzip'ed tar file: 
+<!-- WARNING!  Line below automatically edited by makefile. -->
+      <?php download_link("ProofGeneral-3.1pre000209-devel.tar.gz") ?>
+<!-- End Warning. -->
+  </li>
+</ul>
+<p>
+What's the difference from the working version above?
+The complete archive also includes:
+</p>
+<ul>
+  <li> provisional instantiations of Proof General to new provers <br>
+	(mentioned in the 
+   <!-- WARNING!  Line below automatically edited by makefile. -->
+  <?php fileshow("ProofGeneral-3.1pre000209/CHANGES","CHANGES"); ?> file),
+   <!-- End Warning. -->
+  </li>
+  <li> the 
+   <!-- WARNING!  Line below automatically edited by makefile. -->
+   <?php fileshow("ProofGeneral-3.1pre000209/todo","low-level list of things to do"); ?>
+   <!-- End Warning. -->
+   and the detailed
+   <!-- WARNING!  Line below automatically edited by makefile. -->
+   <?php fileshow("ProofGeneral-3.1pre000209/ChangeLog","ChangeLog"); ?>,
+   <!-- End Warning. -->
+ </li>
+  <li> developer's Makefile used to generate documentation files <br>
+       and the release itself from our CVS repository,  </li>
+  <li> some test files, </li>
+  <li> sources for some of the images, 
+  <li> the web pages.  
+</ul>
+<p>
+Note: there are no pre-built documentation files in the developer's
+release, because developers should have the right tools!
+</p>
+<p>
+You probably <em>don't</em> need to download this if you're only
+interested in hacking the Emacs lisp part of the program for
+a prover that is currently supported.  But you may
+still like to check the latest
+<!-- WARNING!  Line below automatically edited by makefile. -->
+<?php fileshow("ProofGeneral-3.1pre000209/todo","low-level to-do list"); ?>.
+<!-- End Warning. -->
+</p>
+
+<?php
+   click_to_go_back();
+   footer();
+?>
diff --git a/html/download.phtml b/html/download.phtml
index 22e3fe45..49a4c025 100644
--- a/html/download.phtml
+++ b/html/download.phtml
@@ -27,7 +27,7 @@ Proof General
 
 <p>
 Developers and beta-testers may like to download
-a <a href="devel.phtml">development release</a>
+a <a href="develdownload.phtml">development release</a>
 of Proof General.
 </p>
 <p>
@@ -81,6 +81,8 @@ Proof General:
 For displaying logical and mathematical symbols, the excellent
 <a href="http://www.fmi.uni-passau.de/~wedler/x-symbol/">X-Symbol</a>
 package. 
+<br>It's very easy to install.  See <a href="#xsyminstall">here</a> 
+for installation notes.
 <br>X-Symbol presently only works with XEmacs.  
 </li>
 <li>
@@ -150,10 +152,12 @@ for a summary of changes since version 2.1.
 Check the latest <?php fileshow("ProofGeneral/BUGS","BUGS"); ?> file
 before reporting problems.  If you find a problem not mentioned
 there, please 
-<?php hlink("feedback.phtml","send us a note.","Feedback form")?>.
+<?php hlink("feedback.phtml","send us a note","Feedback form")?>.
 </p>
 
 
+<br>
+<br>
 <h3> Easy installation! </h3> 
 <p>
 To use Proof General, simply unpack the sources with 
@@ -189,3 +193,21 @@ any problems, suggestions, or patches.
 
 
 
+<br>
+<br>
+<h3><a name="xsyminstall">Easy installation of X-Symbol!</a></h3> 
+
+<p>
+Contrary to what you may expect from the documentation of
+X-Symbol, it's very easy to install and configures itself
+automatically.
+</p>
+<p>
+Simply download the binary package file, and do something
+like this to install in your home directory:
+</p>
+<blockquote><tt>
+ mkdir -p ~/.xemacs<br>
+ cd ~/.xemacs<br>
+ tar xzf ../x-symbol-pkg.tar.gz<br>
+</tt></blockquote>
diff --git a/html/features.phtml b/html/features.phtml
index 63426bf6..c2c6dc89 100644
--- a/html/features.phtml
+++ b/html/features.phtml
@@ -1,5 +1,3 @@
-<!-- <h2><a name="why">Why should I use Proof General?</a></h2> -->
-
 <p>
 It doesn't matter if you're an Emacs militant or a pacifist!
 </p>
diff --git a/html/header.phtml b/html/header.phtml
index 0415a7b9..3cdc722c 100644
--- a/html/header.phtml
+++ b/html/header.phtml
@@ -24,6 +24,7 @@
 	  "Features"	  =>  "features",
 	  "Download"      =>  "download",
           "Documentation" =>  "doc",
+	  "Development"	  =>  "devel",
 	  "About"	  =>  "about",
 	  "Links"	  =>  "links"
     );
diff --git a/html/links.phtml b/html/links.phtml
index 5a85c3a6..08c4df2b 100644
--- a/html/links.phtml
+++ b/html/links.phtml
@@ -31,8 +31,45 @@ for links to include here, or find broken links, please
 </ul>
 <ul>
 <li>
-  <a href="http://www.ags.uni-sb.de/~omega/">OMEGA</a>,
+  <a href="http://www.ags.uni-sb.de/~omega/">OMEGA</a> is
   a collection of web-based distributed tools for supporting
   theorem proving.
 </li>
 </ul>
+<ul>
+<li>
+  <a href="http://www.dcs.gla.ac.uk/prosper/">Prosper</a> is a project
+  to develop an extensible, open proof tool architecture for
+  incorporating formal verification into industrial CAD/CASE tool
+  flows and design methodologies. The tools include novel
+  user-friendly interfaces.
+</li>
+</ul>
+<ul>
+<li>
+  As a possible foundation for generic proof environments,
+  <a href="http://www.nag.co.uk/projects/openmath/omsoc/">OpenMath</a>
+  is a standard representation form for mathematical objects, which
+  links in with the <a href="http://www.w3.org/Math/">MathML</a>
+  markup language.
+</li>
+</ul>
+<ul>
+<li>
+  As a possible foundation for generic proof environments,
+  <a href="http://www.nag.co.uk/projects/openmath/omsoc/">OpenMath</a>
+  is a standard representation form for mathematical objects, which
+  links in with the <a href="http://www.w3.org/Math/">MathML</a>
+  markup language.
+</li>
+</ul>
+<ul>
+<li>
+  <a href="http://www.mrg.dist.unige.it/omrs/index.html">Open Mechanized Reasoning System (OMRS)</a>
+</li>
+</ul>
+<ul>
+<li>
+  <a href="http://eti.cs.uni-dortmund.de:8080/servlet/ETI">ETI</a>
+</li>
+</ul>
diff --git a/html/news.phtml b/html/news.phtml
index 9214f1ab..b38005f9 100644
--- a/html/news.phtml
+++ b/html/news.phtml
@@ -2,24 +2,36 @@
 <!-- da: Put this line in instead if you're not me -->
 <!-- <i>(News items entered by <a href="http://www.dcs.ed.ac.uk/~da">David Aspinall</a> -->
 <!--     unless noted.)</i> -->
-<i>News items by <a href="http://www.dcs.ed.ac.uk/~da">David Aspinall</a>.</i>
+<i>News items by <a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.</i>
 </p>
 
 <ul>
-<li><b>9th February 2000</b><br> 
+<li><b>15th February 2000</b>
+<p>
+There is now a new 
+<?php link_root("devel","page for developers") ?>.
+I plan to apply for funding to continue managing the evolution
+and development of Proof General, once my own job position
+is more secure.  Now is the time to flesh out ideas
+for the future!  Check the development page for the
+latest proposals.
+</p>
+<li><b>9th February 2000</b>
+<p>
 Countdown to Proof General 3.1 begins.  This will be a bug fix releaase.
 A few bugs have been fixed in
 recent Proof General development releases, one important one is fixing
 support for non-mule versions of FSF Emacs (thanks to Pierre Courtieu
 for raising it to my attention).  I would like to release PG 3.1 next
 month so that everyone can benefit.
+</p>
 <p>
 In the meantime, please 
 <?php hlink("feedback.phtml","report any important problems","Feedback form")?>
 that you would like to see fixed, and consider trying out 
 the current <a href="devel.phtml">development release</a>.
-
-<li><b>14th December 1999</b><br>
+</p>
+<li><b>14th December 1999</b>
 <p>
 I'm pleased to say that Proof General will be demonstrated at
 <a href="http://iks.cs.tu-berlin.de/etaps2000/etaps.html">ETAPS 2000</a>.
@@ -29,7 +41,7 @@ the presentation
 A presentation of Proof General based on these slides was given at 
 <a href="http://www.clrc.ac.uk/">Rutherford Appleton Laboratory</a> last week.
 </p>
-<li><b>26th November 1999</b><br>
+<li><b>26th November 1999</b>
 <p>
 Proof General 3.0 is released!
 </p>
diff --git a/html/projects.phtml b/html/projects.phtml
new file mode 100644
index 00000000..281c043d
--- /dev/null
+++ b/html/projects.phtml
@@ -0,0 +1,90 @@
+<?php  
+  require('functions.php3');
+  small_header("Proof General Project Proposals"); 
+  ?>
+
+<p>
+Here are some proposals for projects connected to Proof General.
+</p>
+<p>
+The projects are designed as fairly self-contained contributions,
+involving code development and possibly a small amount of supporting
+research.  They would be ideal projects for interested students
+or researchers.
+</p>
+
+<ul>
+<li><b>Proof-by-pointing support for Coq</b>
+<p>
+Coq already has sophisticated notions of proof-by-pointing,
+and old work on support for Proof General may be helpful.  
+We want to integrate with the latest version of Coq's
+proof-by-pointing, possibly improving Proof General's
+support along the way.
+</p>
+<p>
+<b>Skills:</b>
+ Some understanding of Coq implementation, co-operation with
+ the Coq developers to get any Coq modifications (if any) incorporated.
+ Minimal Emacs Lisp knowledge. 
+</p><p>
+<b>Proposer:</b>
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+</p>
+
+<li><b>Proof-by-pointing support for Isabelle</b>
+<p>
+Isabelle has a sophisticated concrete syntax mechanism which makes it
+difficult to add annotations to connect the displayed output back to
+the internal abstract syntax.  This issue needs to be solved to
+support proof-by-pointing (and other features) in Isabelle.
+A 
+<a href="http://www.informatik.uni-bremen.de/~bu/isa_contrib/isabelle.html">
+patch by Burkhart Wolff</a> 
+providing term structure annotations for a previous release of
+Isabelle may be useful here.  To implement proof-by-pointing itself,
+tactics using the gesture information must be written.
+</p>
+<p>
+<b>Skills:</b>
+ Some understanding of Isabelle implementation, 
+ co-operation with the Isabelle developers to get
+ Isabelle modifications incorporated.
+ Skill in writing Isabelle tactics.
+ Minimal Emacs Lisp knowledge.
+</p><p>
+<b>Proposer:</b>
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+</p>
+</li>
+</ul>
+
+
+
+<p>
+If you are interested in working on any of these projects,
+feel free to discuss with the project proposer or on the 
+<?php link_root("devel#develmail","developer's mailing list") ?>.
+</p>
+<p>
+Note: the proposer of the project is just that; he or she does not
+guarantee to be available for formal supervision or intensive help
+with the project.  But it may be possible to find somebody else
+to do that.  Contact the project proposer first for more details.
+</p>
+
+<p>
+If you would like to submit a project proposal
+for an improvement or extension of Proof General,
+please send an email or write a description on the 
+<?php hlink("feedback.phtml","web feedback form","Feedback form")?>.
+Projects should be significant contributions rather than
+incremental improvements (although we welcome the suggestion of those
+too).
+</p>
+
+
+<?php
+   click_to_go_back();
+   footer();
+?>