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. 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.
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).