path: root/html/oldnews.phtml

<?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();
?>