A Web Based Replayer For Proof General

Abstract

Proof General is a generic interface for proof assistants, based on Emacs. It has been developed at the LFCS in the University of Edinburgh. 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 the proofs. The aim of this project is to have a web-based version of Proof General which allowed for this proof replay, 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 displaying the results.