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 proof-toolbar-use-button-enablers). The patch also removes the use of an "interval timer" when proof-toolbar-use-button-enablers 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.
New! For developers, a web-browsable mirror of the Proof General cvs is available here.
New! Proof General . Please send questions or suggestions for inclusion to proofgen@dcs.ed.ac.uk, thanks.
A minor patch to Proof General 3.1 is released today. To check what version you have, look at the variable proof-general-version set in proof-site.el. (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 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.
Further improvements are being introduced in the new 3.2 pre-releases, see the development download page, as usual.
Proof General 3.1 is now available from the . Enjoy!
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.
New: HOL Proof General! It took me only a couple of hours to add a basic instantiation of ProofGeneral for HOL98. 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.
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.
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.
The HOL support is shipping in the current development release.
There is now a new . 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.
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.
In the meantime, please that you would like to see fixed, and consider trying out the current development release.
I'm pleased to say that Proof General will be demonstrated at ETAPS 2000. Here are some draft slides for the presentation (any comments would be welcome). A presentation of Proof General based on these slides was given at Rutherford Appleton Laboratory last week.
Proof General 3.0 is released!
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 pre-release, 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.
New! With Proof General 3.0, adapting to a new prover is easier than ever before! It includes an 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!
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 pre-release for Isabelle 99.
Some recent changes have been made to the support for X-Symbol, so that it is easier to turn on and off, and support is now properly generic. At the moment only Isabelle has support implemented.
See what Proof General 3.0 will look like! The screenshot has been updated.
The next version of Proof General will be 3.0.
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!
Version 3.0 is planned for release in November. Please test a Version 3.0 pre-release if you can and report any problems.
I'm very grateful to
Pierre Courtieu <courtieu@lri.fr>
for offering to help work on Coq Proof General.
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...
Recently there has been a flurry of work on the next version of Proof
General. It has quite a number of improvements (see the file), made by myself
and Markus Wenzel.
The next version is aimed to coincide
roughly with the release of Isabelle 99.
At the moment we urgently need 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. Please offer to help, it needn't be a heavy commitment.
I've just returned from the
Types Summer School, Giens, France
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.
Print pictures from the new gallery of publicity shots of Proof General!
Proof General version 2.1 is released.
Check the file
for a summary of changes since Proof General 2.0.
It is recommended that all users upgrade except
those still using Isabelle 98-1.
Proof General 2.1 supports only the 99 version of Isabelle.
New Proof General web pages go live!
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.
Please explore the new web pages and report any problems or suggestions to . 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.
A new instantiation of Proof General has been added by Paul Callaghan for Plastic, a new proof assistant based on Luo's Typed Logical Framework and implemented in Haskell.
A new instantiation of Proof General has been added by Markus Wenzel for Isabelle/Isar, a new proof language for Isabelle to be included with Isabelle 99.
News items by David Aspinall.