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). +General standardized protocol for interaction (see white paper here). 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).
Skills: @@ -170,6 +171,79 @@ assistants.
++PGML is the proposed logical markup language for future versions of +Proof General. The basic version legitimizes the present markup +scheme which is used by Proof General (based on 8-bit characters). +Ideas for PGML are described in the white paper +here, but no complete description or +DTD is given there. This project is to specify PGML using XML or SGML, +and develop some tools for using it. Various tools are desirable, +including: (1) a display tool which displays PGML inside Emacs, or +converts it to HTML for display by a web browser; (2) a filter or +revised version of LEGO which converts its 8-bit markup into PGML, for +testing purposes. +
++Skills: +Understanding of markup languages and tools for using and specifying them. +Interest in representation of mathematical content. +Necessary programming skills. +
+Proposer: +David Aspinall. +
++PGIP is a protocol for interactive proof to be used in the next +version of Proof General. It is based around the present protocol, +but implemented with a standard collection of messages rather than +different messages for different proof assistants. An outline of PGIP +is given in the white paper. A +first implementation of PGIP will consist of (1) a filter (or +modification of the output routines) for an existing proof assistant, +which could be implemented in perl or some other language; and (2) a +new backend for Proof General in Emacs, which configures it for PGIP. +
++Skills: +Interest in interactive proof and basic understanding +of interaction mechanisms with at least one of +LEGO, Coq, Isabelle. Programmming in Emacs Lisp. +
+Proposer: +David Aspinall. +
++One of the nice features of Proof General is that it is very easy to +replay existing proofs, by mouse clicks alone. No low-level +understanding of a proof assistant is needed to step through proofs. +We would like to have a web-based version of Proof General which +allowed for this proof replay (at least), perhaps running a proof +assistant remotely. The main aspect is to implement an engine for +script management (colouring of lines of files), displaying in a web +browser, sending lines to a proof assistant process, and display the +results. Ideally, the ideas for new standard protocols for Proof +General in the white paper would +be followed. +
++Skills: +Strong web programming skills using scripting languages, +dynamic HTML, etc. +
+Proposer: +David Aspinall. +
+