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.
The projects are divided into those which are specific to Proof General, and those which would be useful more widely and do not depend on Proof General. For more information on a project, click on its title.
Some projects involve Emacs Lisp. This is the embedded programming language inside Emacs. It is very easy to learn, since it is small, has a good manual, and has an interactive interpreter. It is easy to use, not least because of its self-documenting nature: each variable or function is compiled together with documentation of its purpose. (Other languages would do well to follow this). It also has a powerful source-level debugger, edebug.
If you are interested in working on any of these projects, feel free to discuss with the project proposer or on the .
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 efforts. NB: the proposer of the project 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).
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).