diff options
Diffstat (limited to 'html/oldnews.html')
| -rw-r--r-- | html/oldnews.html | 411 |
1 files changed, 0 insertions, 411 deletions
diff --git a/html/oldnews.html b/html/oldnews.html deleted file mode 100644 index 47d7ebd7..00000000 --- a/html/oldnews.html +++ /dev/null @@ -1,411 +0,0 @@ -<?php - require('functions.php3'); - small_header("Proof General Old News"); - ?> -<ul> - - -<li><b>19th June 2002</b> -<p> -We plan to release version <b>3.4</b> of Proof General -in August. This update will have several significant -improvements -(notably to the synchronization support for Coq), and also includes -fixes and updates for recent versions of Emacs (notably GNU Emacs 21.x) -and various proof assistants. -<br> -<b>Please, please, please</b> do test some <a -href="develdownload.html">development releases</a> for us in the -meantime and <a href="feedback">report any difficulties</a>, -to help make the next release of Proof General as -robust as possible. Thanks! -</p> -</li> - -<li><b>14th December 2001</b> -<p> -The current <a href="develdownload.html">development release</a> takes -advantage of the new fancy features available in GNU Emacs 21, to add -toolbar support and other features there. As usual, maintaining the -code to work with both Emacs versions is quite troublesome, so bug -reports and patches from users are very welcome. -</p> -</li> - -<li><b>10th September 2001</b> -<p> -<a href="download">Proof General 3.3</a> is released, with -<?php fileshow("ProofGeneral-3.3/CHANGES","new features"); ?> to -increase your proof script editing efficiency. Happy proving! -</p> -</li> -<li><b>1st August 2001</b> -<p> -The past few months have seen a few more improvements and -bug fixes to Proof General: many thanks to those who have -sent us <a href="feedback">useful feedback</a>. -It's time that we made a proper release, so please try -out the <a href="develdownload.html">development release</a> -and help us iron out as many more problems as we can. -<br> -Emacs Lisp and the Emacsen libraries has to be one of the -worst moving target platforms to develop an application on, -so please help us! Once things are looking good, we'll -release PG 3.3. -</p> -<li><b>8th May 2001</b> -<p> -Proof General has had a few quiet improvements since October, which -appear in the current -<a href="develdownload.html">development release</a>. -This version also has some compatibility fixes -for the recent releases of Emacs (20.7) and XEmacs (21.4). -</p> - -<li><b>2nd October 2000</b> -<p> -Proof General 3.2 is released today. Happy proving! -</p> - -<li><b>25th Sep 2000</b> -<p> -Final week of testing for Proof General 3.2. -The last chance to report bugs or request (minor) improvements for this release. -Please help us by trying out the -<a href="develdownload.html">pre-release</a>, especially if you are -relying on an older or non-standard Emacs version. -Also check to see if the new -manuals are useful: now split into -the user manual in -<?php htmlshow("ProofGeneral/doc/ProofGeneral_toc.html","HTML","Proof General manual") ?>, -<?php download_link("ProofGeneral/doc/ProofGeneral.ps.gz", "ps") ?> -or -<?php download_link("ProofGeneral/doc/ProofGeneral.pdf", "pdf") ?>, -and the separate "adapting" manual, in -<?php htmlshow("ProofGeneral/doc/PG-adapting_toc.html","HTML","Adapting Proof General manual") ?>, -<?php download_link("ProofGeneral/doc/PG-adapting.ps.gz", "ps") ?> -or -<?php download_link("ProofGeneral/doc/PG-adapting.pdf", "pdf") ?>. -(Info files are included in the distribution). -</p> -<li><b>14th Sep 2000</b> -<p> -Improvements to web pages. Graphics made smaller, text more concise. -Please <?php hlink("feedback","send me suggestions ","Feedback form")?> -for further improvements. -(I know some pages display poorly in Netscape 4.7x because -of patchy stylesheet support; they appear much better in IE5 -or the rather impressive recent versions of KDE's Konqueror). -</p> -<li><b>28th Aug 2000</b> -<p> -We're starting the testing phase for Proof General 3.2. -It has several new features and improvements. -Please try out the <a href="develdownload.html">pre-release</a> -version, and report any problems to us. Your -feedback is very important because we have no resources available for -serious compatibility testing ourselves. -</p> -<p> -We hope to release 3.2 by the end of September. -</p> -</li> -<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> -<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.html">development download</a> page, as usual. -</p> -<li><b>23rd March 2000</b> -<p> -Proof General 3.1 is now available from the -<a href="download">download page</a>. 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.html">development release</a>. -</p> -</li> -<li><b>15th February 2000</b> -<p> -There is now a new -<a href="devel">page for developers</a>. -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 GNU 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","report any important problems ","Feedback form")?> -that you would like to see fixed, and consider trying out -the current <a href="devel">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:David.Aspinall@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">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="develdownload.html">pre-release</a> -for Isabelle 99. -</p> -<p> -Some recent changes have been made to the support for -<a href="http://x-symbol.sourceforge.net/">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.html">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 <courtieu@lri.fr></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">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">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://homepages.inf.ed.ac.uk/da">David Aspinall</a>.</i> -</p> - - -<?php - click_to_go_back(); - footer(); -?> |