As Proof General becomes a more complex system, we badly need some way of performing automatic functional testing, to ensure that changes and extensions preserve functional correctness. Although classical testing of interfaces involves manually following a checklist of actions and observations, it should be straightforward to automate this using Emacs Lisp. Interactive actions can be simulated by certain function calls, and their results can be determined by examining the contents of the edit buffers. This project proposes the design and implementation of a test harness and accompanying test suite to test some of the core functions of Proof General. Ultimately, the tests should be run as part of the build process before each development release is allowed to go ahead.
Skills: An interesting in testing user interfaces. Basic knowledge of Emacs Lisp.
Proposer: David Aspinall.