[Prev][Next][Index][Thread]
Proof General --- Version 3.0 release
Announcing Proof General Version 3.0
A Generic Emacs interface for Interactive Proof Assistants
http://zermelo.dcs.ed.ac.uk/~proofgen
contact: David Aspinall <da@dcs.ed.ac.uk>
=========================
Proof General is an Emacs interface for developing proof scripts.
It can be instantiated for the proof assistant of your choice,
and is supplied ready-customised for Isabelle, Coq, and LEGO.
Proof General includes these features, amongst others:
. Script management: proof assistant state reflected in editor
. Toolbar and menus: commands for building and replaying proofs
. Syntax highlighting of proof scripts and prover output
. Display of real logical symbols, greek letters, etc
. Simplified communication: proof assistant verbosity hidden
. Menu for jumping to theorems in a proof script
. Provision to easily run proof assistant on a remote host
. Works on any platform Emacs does, in window system or plain console
Summary of changes since 2.1:
. Eight new toolbar buttons, now enabled depending on context
. Improved and reorganized menus and key-bindings, options settings
. Much easier to adapt to new systems, comes with example (< 30 setqs)
. New function to search for theorems
. X-Symbol support for Coq, LEGO, and Isabelle
. Lots more fine-grained improvements, for full details
http://zermelo.dcs.ed.ac.uk/~proofgen/ProofGeneral-3.0/CHANGES
The user manual contains full details, and is available on-line at:
http://zermelo.dcs.ed.ac.uk/~proofgen/index.phtml?page=doc
Proof General needs a recent version of Emacs to run with, and it much
prefers XEmacs to FSF GNU Emacs. Proof General 3.0 has been tested
with XEmacs 21.1 and Emacs 20.4. (It should work back to XEmacs 20.4
and Emacs 20.2, though).
Installing Proof General is easy. Why not give it a try?
- David Aspinall <da@dcs.ed.ac.uk>
Appendix
========
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:
------------------------------------
Proof General 3.0 has several new features as well as bug fixes and
improvements over versions 2.1 and 2.0. It 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 worked hard on the user documentation, and on making Proof
General robust and easy to install.
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. I'd be keen to hear
from workers interested in collaborating in this area.
To Emacs gurus:
---------------
If you happen to be an Emacs guru also interested in interactive
proof, we want you 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.
I would be keen to hear from any Emacs developers interesting in
adapting Proof General's script management for development in Lisp,
SML, or other languages.
-- David Aspinall <da@dcs.ed.ac.uk>
December 1999.