[Prev][Next][Index][Thread]
Proof General --- Version 3.1 release
-
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@jaguar.cs.byu.edu, pvs@csl.sri.com, qed@mcs.anl.gov, theorem-provers@ai.mit.edu, types@cis.upenn.edu, formal-methods@cs.uidaho.edu, reliable_computing@interval.usl.edu, prog-lang@diku.dk
-
Subject: Proof General --- Version 3.1 release
-
From: David Aspinall <da@dcs.ed.ac.uk>
-
Date: Fri, 16 Jun 2000 11:59:14 +0100 (BST)
[ Apologies for multiple copies. Also, this is a rather delayed
announcement: Proof General 3.1 was actually released back
in March but only advertised on the PG mailing list. ]
Announcing Proof General Version 3.1
A Generic Emacs interface for Interactive Proof Assistants
http://www.lfcs.informatics.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, LEGO, and HOL.
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 3.0:
. New instantiation for HOL98!
. Minor cosmetic improvements
. Bug fixes for Emacs compatibility (FSF, Japanese versions, XEmacs on win32)
. Fix for infamous Solaris ^G bug
. Several other bug fixes
. For full details, see
http://www.lfcs.ed.ac.uk/proofgen/ProofGeneral-3.1/CHANGES
The user manual contains full details, and is available on-line at:
http://www.lfcs.informatics.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.1 has been tested
with XEmacs 21.1 and Emacs 20.5. (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>
June 2000.