Here are some proposals for projects connected to Proof General.
The projects are designed as fairly self-contained contributions, involving code development and possibly a portion of supporting research. They would be ideal projects for interested students or researchers.
Coq already has sophisticated notions of proof-by-pointing, and old work on support for Proof General may be helpful. We want to integrate with the latest version of Coq's proof-by-pointing, possibly improving Proof General's support along the way.
Skills: Some understanding of Coq implementation, co-operation with the Coq developers to get any Coq modifications (if any) incorporated. Minimal Emacs Lisp knowledge.
Proposer: David Aspinall.
Isabelle has a sophisticated concrete syntax mechanism which makes it difficult to add annotations to connect the displayed output back to the internal abstract syntax. This issue needs to be solved to support proof-by-pointing (and other features) in Isabelle. A patch by Burkhart Wolff providing term structure annotations for a previous release of Isabelle may be useful here. To implement proof-by-pointing itself, tactics using the gesture information must be written.
Skills: Some understanding of Isabelle implementation, co-operation with the Isabelle developers to get Isabelle modifications incorporated. Skill in writing Isabelle tactics. Minimal Emacs Lisp knowledge.
Proposer: David Aspinall.
Emacs already provides powerful outline facilities (cf. the outl-minor-mode setup for the well-known auc-tex package). Similarly, proof systems such as Isabelle/Isar are inherently based on block-structured proof texts, with compositional proof checking.
But Proof General currently offers a mostly linear model of incremental script management. The aim of this project is to extend that model to a hierarchic one: e.g. sub-proofs could be suppressed in the presentation, or even temporarily suspended (to achieve top-down development).
Outline support would be useful for the large scale structure of formal developments as well, e.g. support the basic arrangement into logical section (cf. Coq), or even just traditional layout-based ones (cf. LaTeX).
Skills: Some understanding of the workings of Emacs outline mode and Proof General script management. Good portion of Emacs lisp knowledge.
Proposer: Markus Wenzel.
Emacs has a mechanism for customizing the editing behaviour of buffers based on their major mode. A buffer can only have one major mode, but in literate styles of programming and proving we want to mix program text with documentation in a single file. A way of multiplexing major modes is needed, so that different regions of a buffer can be edited in different modes. One approach may be to use "views" onto untangled buffers, although it isn't clear how search and replace, etc, should behave in this case.
Emacs hackers may already have worked on this problem and solved it sufficiently well (does anybody know?), in which case this project might degenerate into applying the work for Coq and Isabelle/Isar, as a feasibility demonstration.
Skills: A passion for Emacs and Emacs Lisp.
Proposer: David Aspinall.
Proof General is based around a core system of script management for proof scripts. But the idea of script management is not restricted to proof assistants, it makes sense for many interactive scripting languages. It deserves to be better known and used. A worthwhile project would be to rewrite the core script management features of Proof General so that they could work for arbitrary interactive scripting languages, and instantiate to Proof General as well as languages such as ML, Haskell, LISP, Scheme, Python, and even Emacs Lisp itself.
An alternative version of this project is to implement a generic basis for script management which does not depend on Emacs, but uses a similar protocol to communicate with other text editors or display widgets. This could be implemented in SML, OCaml, Java, C++, or any other suitable language.
Skills: Proficient Emacs Lisp (or other programming language), knowledge of scripting languages desirable.
Proposer: David Aspinall.
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 theory browser 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 dired-like buffer.
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 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: Interface programming skills. Basic understanding of what theories are for several different proof assistants.
Proposer: David Aspinall.
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.
If you are interested in working on any of these projects, feel free to discuss with the project proposer or on the .
Note: the proposer of the project is just that; he or she does not guarantee to be available for formal supervision or intensive help with the project. But it may be possible to find somebody else to do that. Contact the project proposer first for more details.
If you would like to use any of these ideas as a formal project proposal for students at your institution, please feel free but do if some work is begun, to help coordinate effort.
If you would like to submit a project proposal for an improvement or extension of Proof General, please send an email or write a description on the . Projects should be significant contributions rather than incremental improvements (although we welcome the suggestion of those too).