1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
|
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@cis.upenn.edu,
formal-methods@cs.uidaho.edu,
reliable_computing@interval.usl.edu,
prog-lang@diku.dk
Also newsgroups:
comp.lang.ml
comp.lang.functional
gnu.emacs.sources
comp.emacs.xemacs
comp.os.linux.announce
freshmeat.net
tag for comp.lang.ml, comp.lang.functional:
[Posted here because ML and functional languages generally are
traditional for implementing interactive theorem provers.
Implementors of such systems may be interested in Proof General.
Apologies for multiple copies]
Subject: Proof General --- Version 3.3 release
Announcing Proof General Version 3.3
A Generic Emacs interface for Interactive Proof Assistants
http://www.proofgeneral.org
contact: David Aspinall <da@proofgeneral.org>
Proof General is a generic (X)Emacs interface for proof assistants.
It can be instantiated for the proof assistant of your choice, and is
supplied ready-customised for Isabelle, Coq, LEGO, and PhoX, and,
experimentally, for HOL, Twelf, and ACL2.
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; hiding proofs
. 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.2:
. Visibility control for completed proofs
. Dependency browsing/highlighting (currently Isabelle only)
. Bug fixes
. Compatibility improvements: XEmacs 21.4, Coq 7, Windows
For details of changes since 3.2, see
http://www.proofgeneral.org/fileshow.php?file=ProofGeneral-3.3%2FCHANGES
For the latest user manual, see http://www.proofgeneral.org/doc
Proof General needs a recent version of Emacs to run with, and it much
prefers XEmacs to FSF GNU Emacs. Proof General 3.3 has been tested
with XEmacs 21.4 and Emacs 20.7. (It may 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>
September 2001.
|
