Renamed file

1 files changed, 309 insertions, 0 deletions

diff --git a/html/oldnews.html b/html/oldnews.html
new file mode 100644
index 00000000..4078fd73
--- /dev/null
+++ b/html/oldnews.html
@@ -0,0 +1,309 @@
+<?php  
+  require('functions.php3');
+  small_header("Proof General Old News"); 
+  ?>
+<ul>
+<li><b>25th May 2000</b>
+<p>
+Minor patch 3.1.6 released today.  This turns off toolbar enablers if
+you're running XEmacs on Solaris; because of strange Solaris problems,
+buttons are disabled too often there.  (You can live without
+this part of the patch by customizing the variable
+<tt>proof-toolbar-use-button-enablers</tt>). 
+The patch also removes 
+the use of an "interval timer" when 
+<tt>proof-toolbar-use-button-enablers</tt> is off, since a user 
+reported being unable to start itimers unless
+running as root (likely an operating system configuration problem).
+Thanks to Markus Wenzel and Pierre Lescanne for reporting problems.
+</p>
+<li><b>9th May 2000</b>
+<p>
+New! For developers, a web-browsable
+mirror of the Proof General cvs is available
+<a href="http://www.proofgeneral.org/cgi-bin/cvsweb.cgi">here</a>.
+</p>
+<li><b>5th May 2000</b>
+<p>
+New!  
+Proof General <?php fileshow("ProofGeneral/FAQ", "FAQ");?>.
+Please send questions or suggestions for inclusion to
+<a href="mailto:proofgen@dcs.ed.ac.uk">proofgen@dcs.ed.ac.uk</a>,
+thanks.
+</p>
+<li><b>28th April 2000</b>
+<p>
+A minor patch to Proof General 3.1 is released today.  To check what
+version you have, look at the variable <tt>proof-general-version</tt>
+set in <tt>proof-site.el</tt>.  (It is not recorded in the tar file
+name or package version).  The current patch, to 3.1.4, was made to
+fix a problem with Isabelle and theory file retraction, accidently
+introduced in 3.1.  See <?php
+fileshow("ProofGeneral-3.1-devel/etc/release-log.txt","the developer's
+release log"); ?> for details.
+NB: This patch was first made on 4th April, but didn't quite solve the
+problem.  Thanks to Mike Squire for sending a patch to fix the fix.
+</p>
+<p>
+Further improvements are being introduced in the new 3.2 pre-releases,
+see the 
+<a href="develdownload.phtml">development download</a> page, as usual.
+</p>
+<li><b>23rd March 2000</b>
+<p>
+Proof General 3.1 is now available from the
+<?php link_root("download","download page") ?>.  Enjoy!
+</p>
+</li>
+<li><b>14th March 2000</b>
+<p>
+Release candidate for Proof General 3.1 available.
+Pre-releases from now on are release candidates for version 3.1.
+Please test and report any problems you find
+(check the CHANGES and BUGS lists for issues known about
+and/or resolved).  Version 3.1 should be released next week.
+</p>
+</li>
+<li><b>10th March 2000</b>
+<p>
+New: <b>HOL Proof General</b>!
+It took me only a couple of hours to add a basic instantiation of
+ProofGeneral for 
+<a href="http://www.cl.cam.ac.uk/Researc/HVG/HOL/HOL.html">HOL98</a>.
+Most of this time was in trying to find out how to do things in HOL,
+I could have done with a HOL user to hand.  But I thought it was high time
+HOL got a look-in.
+</p>
+<p>
+HOL Proof General provides script management support, automatic
+multiple files, decoration of proof scripts and output.
+Character-sequence X Symbols as in Coq and LEGO.  Although this is a
+basic feature set for Proof General, the result is still an enormous
+improvement over shell interaction.
+</p>
+<p>
+My hope is to entice HOL users so that one of them may improve HOL
+Proof General.  I don't plan to maintain or seriously improve this
+instantiation myself.
+</p>
+<p>
+The HOL support is shipping in the 
+current <a href="develdownload.phtml">development release</a>.
+</p>
+</li>
+<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.  These include some desirable contributions 
+which could be undertaken as self-contained projects.
+</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>.
+</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>.
+Here are some draft <a href="papers/pgtalk.pdf">slides</a> for 
+the presentation 
+(any <a href="mailto:da@dcs.ed.ac.uk">comments</a> would be welcome).
+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>
+<p>
+Proof General 3.0 is released!
+</p>
+<li><b>17th November 1999</b><br>
+<p>
+Proof General 3.0 is currently in final testing, and will be released
+in a small number of days.  Please help me with this by testing the
+current <a href="devel.phtml">pre-release</a>, so I can iron out as
+many bugs as possible before making the release.  It's very easy to
+install or upgrade Proof General, so it shouldn't be much effort to
+test it quickly.  Particularly if you're already running an earlier
+version.
+</p>
+<li><b>16th November 1999</b><br>
+<p>
+New!  With Proof General 3.0, adapting to a new prover is easier
+than ever before!
+It includes an 
+ <?php fileshow("ProofGeneral/demoisa/demoisa-easy.el", "example instance ");?>
+of Proof General for Isabelle, which 
+configures the main core of the interface with less than 30 lines of
+code.  Not bad for getting about 4000 lines worth of code in benefit!
+</p>
+<li><b>9th November 1999</b><br>
+<p>
+Isabelle 99 was released last week, and Proof General 3.0 should
+be ready for release in the next week or so.  In
+the meantime, please use the current 
+<a href="devel.phtml">pre-release</a>
+for Isabelle 99.
+</p>
+<p>
+Some recent changes have been made to the support for
+<a href="http://www.fmi.uni-passau.de/~wedler/x-symbol/">X-Symbol</a>,
+so that it is easier to turn on and off, and support is now
+properly generic.  At the moment only Isabelle has 
+support implemented.
+</p>
+<li><b>21st October 1999</b><br>
+ <p>
+ See what Proof General 3.0 will look like!
+ The <a href="screenshot.phtml">screenshot</a> has been updated.
+ </p>
+<li><b>14th October 1999</b><br>
+ <p>
+ The next version of Proof General will be 3.0.
+ </p>
+ <p>
+ There have been significant changes to the core of 
+ Proof General and many improvements in the code.
+ Extra features have been added, and the ones already
+ there improved upon.  Usability has been a particular
+ focus.  Adding new provers has been made easier.
+ Installation will be made even easier.
+ All of these changes warrant moving to a major release!
+ </p>
+ <p>
+ Version 3.0 is planned for release in November.
+ Please test a Version 3.0 pre-release if you can
+ and report any problems.
+ </p>
+<li><b>12th October 1999</b><br>
+ <p>
+ I'm very grateful to 
+ <a href="mailto:courtieu@lri.fr">Pierre Courtieu &lt;courtieu@lri.fr&gt;</a>
+ for offering to help work on Coq Proof General.
+ <br>
+ If anyone else in the Coq community would like to assist, please
+ offer still, 
+ there is plenty to do to add: better recognition of proof scripts,
+ multiple file management, proof by pointing, etc...
+ </p>
+<li><b>1st October 1999</b><br>
+ <p>
+ Recently there has been a flurry of work on the next version of Proof
+ General.  It has quite a number of improvements (see the <?php
+ fileshow("ProofGeneral/CHANGES","CHANGES"); ?> file), made by myself
+ and Markus Wenzel.  <br> The next version is aimed to coincide 
+ roughly with the release of Isabelle 99.
+ </p>
+ <p>
+ At the moment we <b>urgently need</b> somebody from the Coq world to
+ maintain and improve Coq Proof General, since Patrick Loiseleur 
+ can no longer work on it.  
+ Support from the Coq community is vital for Proof General to
+ be a useful tool there. <a href="feedback.phtml">Please offer to help</a>, 
+ it needn't be a heavy commitment.
+ </p>
+<li><b>13th September 1999</b><br>
+ <p>
+ I've just returned from the 
+ <a href="http://www-sop.inria.fr/types-project/types-sum-school.html">Types Summer School, Giens, France</a>
+ where Proof General was used for a class of
+ about 50 students who were learning
+ Coq, Isabelle, and LEGO.  I received
+ many useful comments and feedback,
+ which will be
+ used to improve the next version.
+ Thanks to everyone who gave suggestions and bug reports
+ to me, including: 
+ Michael Abbott,
+ Bernd Grobauer,
+ Sebastian Skalberg,
+ Thierry Massart,
+ Darmalingum Muthiayen.
+ <br>
+ </p>
+<li><b>27th August 1999</b><br>
+ <p>
+ Print pictures from the new 
+ <a href="gallery.phtml">gallery</a>
+ of publicity shots of Proof General!
+ </p>
+<li><b>24th August 1999</b><br>
+ <p>
+ Proof General version 2.1 is released.
+ <br>
+  Check the <?php fileshow("ProofGeneral-2.1/CHANGES","CHANGES"); ?> file
+  for a summary of changes since Proof General 2.0.
+ </p>
+ <p>
+  It is recommended that all users upgrade except
+  those still using Isabelle 98-1.  
+  <br> 
+  Proof General 2.1 supports only the 99 version of Isabelle.
+ </p>
+</li>
+
+<li><b>24th June 1999</b><br>
+  <p>
+  New Proof General web pages go live!
+  </p>
+  <p>
+  The general is now more serious looking.
+  Appropriate, because there are some serious improvements 
+  in the pipeline...
+  Before that, we will release Proof General 2.1,
+  mainly a bug-fix improvement of 2.0.
+  </p>
+  <p>
+  Please explore the new web pages and report any problems 
+  or suggestions to <?php mlink($project_email); ?>.
+  Please also try out the latest pre-release of Proof General,
+  this is the final chance to get fixes and tweaks
+  sorted before 2.1.
+  </p>
+</li>
+
+<li><b>11th May 1999</b><br>
+  <p>A new instantiation of Proof General has been added by
+  <a href="http://www.dur.ac.uk/~dcs1pcc/">Paul Callaghan</a>
+  for 
+  <a href="http://www.dur.ac.uk/CARG/plastic.html">Plastic</a>,
+  a new proof assistant based on
+  Luo's Typed Logical Framework and
+  implemented in Haskell. 
+  </p>
+</li>
+
+<li><b>16th April 1999</b><br>
+  <p>A new instantiation of Proof General has been added by
+  <a href="http://www.in.tum.de/~wenzelm/">Markus Wenzel</a>
+  for <a href="http://isabelle.in.tum.de/Isar/">Isabelle/Isar</a>,
+  a new proof language for Isabelle to be included with Isabelle 99. 
+  </p>
+</li>
+</ul>
+<p>
+<i>News items by <a href="http://www.dcs.ed.ac.uk/~da">David Aspinall</a>.</i>
+</p>
+
+
+<?php
+   click_to_go_back();
+   footer();
+?>