+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. +
+ + + -- cgit v1.2.3