blob: 8993d942337d652b081a0f153b75371d2b6107a8 (
plain)
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
|
<h2>A Generic Theory Browser</h2>
<p>
Proof General has very limited mechanisms for helping the user find
theorems and definitions during a proof. It has notion of displaying
a "current context" for a proof, and configuration with a proof
engine command for searching for theorems. It would be useful to
extend these facilities with a <i>theory browser</i> for investigating
the theories currently defined in (or available from) a running proof
assistant. This involves designing a small protocol to communicate
with the proof assistant and a generic way of displaying theories
which have different aspects from system to system. A way which would
fit in well with Emacs would be to use a <tt>dired</tt>-like buffer.
</p>
<p>
An alternative version of this project would be to write a standalone
theory browser which uses an extension of the forthcoming Proof
General standardized protocol for interaction (see white paper <a
href="/home/da/drafts/#white">here</a>). This could be implemented in
Java, or in a functional language, Perl, C or C++, so long as a nice
toolkit is chosen (Qt or GTK).
</p>
<p>
(For a related idea, see the browser integrated with OCaml).
</p>
<p>
<b>Skills:</b>
Interface programming skills.
Basic understanding of what theories are for several different proof
assistants.
</p><p>
<b>Proposer:</b>
<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
</p>
|
