diff options
author | 2000-02-17 19:35:43 +0000 | |
---|---|---|
committer | 2000-02-17 19:35:43 +0000 | |
commit | 34df59a32bfc2ffc0425a4d885e0f6077200a7af (patch) | |
tree | 91f2d8e617aaf050eb9ad15d21f5a2ff92ed0f34 /html | |
parent | 8535ec1728dfdd056c113a618dde89a8153720bd (diff) |
Added browser project
Diffstat (limited to 'html')
-rw-r--r-- | html/projects.phtml | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/html/projects.phtml b/html/projects.phtml index 4a364098..c6fc1fab 100644 --- a/html/projects.phtml +++ b/html/projects.phtml @@ -138,6 +138,38 @@ knowledge of scripting languages desirable. </p> </li> +<li><b>A Generic Theory Browser</b> +<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 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. 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> +<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> +</li> + <!-- <li><b> </b> --> <!-- <p> --> <!-- </p> --> |