Reply-To: "Proof General Maintainer " To: coq-club@pauillac.inria.fr, isabelle-users@cl.cam.ac.uk, lego-club@dcs.ed.ac.uk, uitp@dcs.gla.ac.uk, bra-types@cs.chalmers.se, info-hol@leopard.cs.byu.edu, pvs@csl.sri.com, qed@mcs.anl.gov, theorem-provers@ai.mit.edu, types@cs.indiana.edu, formal-methods@cs.uidaho.edu, reliable_computing@interval.usl.edu, prog-lang@diku.dk Also newsgroups: comp.lang.sml gnu.emacs.sources comp.os.linux.announce freshmeat.net comp.*.xemacs Bring message about script management in other systems under "Emacs gurus" higher in text for non-theory postings. Subject: Proof General --- Version 2.1 release Announcing Proof General Version 2.1 A Generic Emacs interface for Interactive Proof Assistants http://zermelo.dcs.ed.ac.uk/home/proofgen ========================= Proof General is supplied ready-customised for LEGO, Coq, and Isabelle. It includes these features (amongst others): . Script management: files and regions of files processed by prover have a blue background and are read-only; the state of the proof assistant is reflected inside the editor. Script management works across multiple files for LEGO and Isabelle. . A toolbar for building and replaying proofs . Syntax highlighting of proof scripts and prover output . Simplified communication: the proof assistant is run in an Emacs shell buffer, but by default it is hidden from view and only the most recent messages and proofstate are displayed to the user, simplifying the dialogue. . Menu for jumping to theorems in a proof script, Emacs outlining of proof scripts . Provision to easily run proof assistant on a remote host Script management is the main feature. The user manual contains full details, and is available on-line at: http://zermelo.dcs.ed.ac.uk/~proofgen/ProofGeneral/doc/ProofGeneral_toc.html The rest of this announcement contains notes addressed to different user communities: LEGO, Coq, and Isabelle; users of other proof assistants, user-interface/theorem-proving researchers and, finally, Emacs gurus. To users of LEGO, Coq, and Isabelle: ------------------------------------ This release of Proof General has numerous bug fixes and improvements over version 2.0. It also supports the latest theorem prover versions: LEGO 1.3.1, Coq 6.3 and Isabelle 99. Please try it and let us know what you think of it! We have put a lot of work into the user documentation for Proof General and making it robust and easy to install. Ideally you should use it with XEmacs, but it also works with limited features in FSF GNU Emacs. We have tested on XEmacs 20.4,21.1 and Emacs 20.2, 20.3. (It probably works with earlier versions of either Emacs but we cannot guarantee this). To users of other proof assistants: ----------------------------------- Our aim is provide a powerful and configurable Emacs mode which helps user-interaction with interactive proof assistants. Please help us with this aim! The code of Proof General is designed to be adaptable to other proof assistants, by writing a little bit of Emacs Lisp (mainly regular expressions). If you are using or designing another proof assistant, please try configuring Proof General for it, and let us know how you get on. To user-interface/theorem-proving researchers: ---------------------------------------------- Proof General provides a unified interface to different theorem provers. The advantage is that a novice who understands the Proof General interface can inspect and replay proofs in any of the theorem provers supported, without knowing the specific commands needed to drive them. Moreover, by implementing your user-interface ideas in the Proof General framework, your contributions automatically reach a large community of both novice and expert proof assistant users. A desirable avenue towards further and easier unification would be to invent a unified proof script (input) language and proof-state (output) language for theorem provers. The Proof General experience could provide useful insight into such a project. We'd be interested to hear from workers interested in collaborating in this area. To Emacs gurus: --------------- If you are an Emacs guru and want to contribute to the development of Proof General, please join in! There are plenty of exciting avenues for improving this tool, for example, to add proof by pointing facilities (a basis already exists for LEGO), and a theory browser. Apart from proof assistants, script management makes sense for many other systems or languages with an interactive shell-like interpreter. We would be interested to hear from any Emacs developers interesting in using Proof General's script management for development in Lisp, SML, or other languages. -- David Aspinall August 1999.