-We plan to release version 3.4 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.
-
-Please, please, please do test some development releases for us in the
-meantime and report any difficulties,
-to help make the next release of Proof General as
-robust as possible. Thanks!
-
-The current development release 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. -
--Proof General 3.3 is released, with - to -increase your proof script editing efficiency. Happy proving! -
-
-The past few months have seen a few more improvements and
-bug fixes to Proof General: many thanks to those who have
-sent us useful feedback.
-It's time that we made a proper release, so please try
-out the development release
-and help us iron out as many more problems as we can.
-
-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.
-
-Proof General has had a few quiet improvements since October, which -appear in the current -development release. -This version also has some compatibility fixes -for the recent releases of Emacs (20.7) and XEmacs (21.4). -
- --Proof General 3.2 is released today. Happy proving! -
- --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 -pre-release, 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 -, - -or -, -and the separate "adapting" manual, in -, - -or -. -(Info files are included in the distribution). -
--Improvements to web pages. Graphics made smaller, text more concise. -Please -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). -
--We're starting the testing phase for Proof General 3.2. -It has several new features and improvements. -Please try out the pre-release -version, and report any problems to us. Your -feedback is very important because we have no resources available for -serious compatibility testing ourselves. -
--We hope to release 3.2 by the end of September. -
--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! -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 -download page. 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 -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. -
--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. -
--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. -
- - - -- cgit v1.2.3