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
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
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.0 release
Announcing Proof General Version 2.0
A Generic Emacs interface for Interactive Proof Assistants
http://www.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.
See http://www.dcs.ed.ac.uk/proofgen/ProofGeneral/ProofGeneral.html
for the user manual which contains full details.
To users of LEGO, Coq, and Isabelle:
------------------------------------
This release of Proof General should be stable enough for you to use
happily. 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 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 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.
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.
An obvious 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.
-- David Aspinall & Thomas Kleymann
(Please contact via proofgen@dcs.ed.ac.uk)
|
