path: root/html/oldnews.html

<?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: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">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 &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">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://www.dcs.ed.ac.uk/~da">David Aspinall</a>.</i>
</p>


<?php
   click_to_go_back();
   footer();
?>