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
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
|
<h2>What is Proof General?</h2>
<p>
<b>Proof General</b> is a generic interface for proof assistants,
currently based on Emacs.
It has been developed at the
<a href="http://www.lfcs.informatics.ed.ac.uk/">LFCS</a>
in the <a href="http://www.ed.ac.uk/">University of Edinburgh</a>.
Proof General
works best under
<a href="http://www.xemacs.org/">XEmacs</a>, but can also be used with
<a href="http://www.gnu.org/software/emacs/">GNU Emacs</a>.
You need a recent version in either case.
</p>
<p>
To read more about what Proof General
is and what it provides,
<a href="features">check the features list</a>.
To see what Proof General looks like in use, have a look at these
<a href="screenshot">screenshots</a>.
To download Proof General, visit the
<a href="download">download page</a>.
To contact the developers, click
<?php hlink("feedback","here","Feedback form")?>.
</p>
<h2>What systems does Proof General work with?</h2>
<p>
Proof General comes ready-customized for these proof assistants:
</p>
<table width="90%">
<tr>
<td align="center">
<?php hlink("http://pauillac.inria.fr/coq/",
"<img src=\"images/coqlogo4.gif\" width=66 height=61 border=0 alt=\"Coq badge\">","The Coq Home Page") ?>
</td>
<td>
<b><?php fileshow("ProofGeneral/coq/README","Coq Proof General "); ?></b> for
<?php hlink("http://pauillac.inria.fr/coq/",
"Coq","The Coq Home Page") ?>
<br>
<div style="font-size: smaller">
First crafted by
<a href="http://www.dcs.ed.ac.uk/~hhg">Healfdene Goguen</a>.
<br>
Contributions by Patrick Loiseleur.
<br>
Maintained by
<a href="mailto:courtieu@lri.fr">Pierre Courtieu</a>.
</div>
</td>
</tr>
<tr>
<td align="center">
<?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/",
"<img src=\"images/isabelle.gif\" width=74 height=64 border=0 alt=\"Isabelle badge\">",
"The Isabelle Home Page"); ?>
</td>
<td><b><?php fileshow("ProofGeneral/isa/README","Isabelle Proof General "); ?></b> for
<?php hlink("http://www.cl.cam.ac.uk/Research/HVG/Isabelle/",
"Isabelle", "The Isabelle Home Page"); ?>
<br>
<div style="font-size: smaller">
Crafted and maintained by
<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
<br>
Additional maintainance, support for
<a href="http://isabelle.in.tum.de/Isar">Isabelle/Isar</a>
by
<a href="http://www.in.tum.de/~wenzelm/">Markus Wenzel</a>.
</div>
</td>
</tr>
<tr>
<td align="center">
<?php hlink("http://www.dcs.ed.ac.uk/home/lego",
"<img src=\"images/lego-badge.gif\" width=123 height=33 border=0 alt=\"LEGO badge\">",
"The LEGO Home Page") ?>
</td>
<td><b><?php fileshow("ProofGeneral/lego/README","LEGO Proof General "); ?></b> for
<?php hlink("http://www.dcs.ed.ac.uk/home/lego",
"LEGO","The LEGO Home Page") ?>
<br>
<div style="font-size: smaller">
First crafted by <a href="http://www.dcs.ed.ac.uk/~tms">Thomas Kleymann</a>
and
<a href="http://www.dcs.ed.ac.uk/~djs/welcome.html">Dilip Sequeira</a>.
<br>
Maintained by
<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>
and
<a href="http://www.dur.ac.uk/p.c.callaghan/">Paul Callaghan</a>.
</div>
</td>
</tr>
<tr>
<td align="center">
<?php hlink("http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html",
"PhoX",
"The PhoX Home Page") ?>
</td>
<td><b><?php fileshow("ProofGeneral/phox/README","PhoX Proof General "); ?></b> for
<?php hlink("http://www.lama.univ-savoie.fr/~RAFFALLI/af2.html",
"PhoX","The PhoX Home Page") ?>
<br>
<div style="font-size: smaller">
Crafted and maintained by
<a href="http://www.lama.univ-savoie.fr/~RAFFALLI">Christophe Raffalli</a>
and
<a href="mailto:roziere@logique.jussieu.fr">Paul Roziere</a>.
</div>
</td>
</tr>
</table>
<p>
There are also <i>experimental</i> instances of Proof General:
<ul>
<li><b><?php fileshow("ProofGeneral/hol98/README","HOL Proof General"); ?></b>,
for <a href="http://www.cl.cam.ac.uk/Research/HVG/HOL/HOL.html">HOL98</a>.
</li>
<li><b><?php fileshow("ProofGeneral/twelf/README","Twelf Proof General"); ?></b>,
for <a href="http://www.twelf.org">Twelf</a>.
</li>
<li><b><?php fileshow("ProofGeneral/acl2/README","ACL2 Proof General"); ?></b>,
for <a href="http://www.cs.utexas.edu/users/moore/acl2">ACL2</a>.
</li>
</ul>
<p>
These instances of Proof General are functional, but only show a bare
fraction of what is possible. We are
seeking volunteers to support and improve each of these
(please <a href="feedback">send a note to
<tt><?php print $project_feedback; ?></tt></a> if you're interested).
</p>
<p>
Proof General is ready to be customized to new proof assistants.
It can be <?php fileshow("ProofGeneral/demoisa/demoisa-easy.el",
"very easy"); ?> to get basic support working.
Full <a href="ProofGeneral/doc/PG-adapting.pdf">documentation on
configuration</a> is provided.
</p>
|
