Motivation

The initial idea came from Henk Barendregt, who envisioned a web-portal for formalization of mathematics, that would include Wiki functionality. We already had proof checkers, and libraries for them, but there were no useful web interfaces to them. Possible uses of our the interface already include:

• See a proof assistant, experimental feature or library without installing it
• Have interactive proofs on web pages
• Cooperation in proof development (proofs are saved on the server, so no versioning system is necessary)

Implementation

The system consists of a server part and a client part:

• The client part is 30kB of Javascript. It is downloaded by the client's browser when a user accesses the web page. Most of it are routines for managing the buffer, locking the already verified statements and finding whole expressions.
• The server is about 1000 lines of OCaml code, which is a web-server, that runs coqtop subprocesses.

Security

Security is particularly important in a centralized approach. The current implementation already provides security by the following means:

• Minimal chrooted environment
• Runs as a user with no permissions
• Dropping to ML toplevel is disabled where possible

Possible other security enhancements include cpu, memory and disc quotas, further virtualization (Xen and similar solutions) and automatic recreation of the filesystem.

Other provers

The interface has been initially created as a web interface for Coq, then for Isabelle and now includes preliminary support for Lego, Plastic, Matita and Hol Light. The functionality that is prover specific is:

• Client part: Recognition of expressions that need to be sent to the server that are not in comments or quotes
• Server part: Interaction with the server process, in particular checking if a given command succeeded or failed, and knowing how to undo (Backtrack)

In principle adapting the interface to work with a prover with which proof-general is able to work, should be straight-forward.

Ideas and suggestions (more are welcome)

• Combine it with a Wiki
• HELM / WHELP / CoqDoc / Syntax Highlighting
• Do more tests with Internet Explorer (jumping cursor?)
• Stopping Prover (Ctrl-C)
• Hide prompt and toplevel in errors
• Local download/upload and file listing
• Using Unicode in proofs and not only in comments
• Two browser sessions editing the same file
• Autoscroll (not sure if possible)