diff options
Diffstat (limited to 'html/oldnews.html')
| -rw-r--r-- | html/oldnews.html | 417 |
1 files changed, 417 insertions, 0 deletions
diff --git a/html/oldnews.html b/html/oldnews.html new file mode 100644 index 00000000..510f0904 --- /dev/null +++ b/html/oldnews.html @@ -0,0 +1,417 @@ +<?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>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.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(); +?> |