News items by David Aspinall.
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!
Click here for old news.