Home Page of Cezary Kaliszyk |
ProofWeb - Web interface for Proof Assistants
General
The prototype offers a web interface for Coq, Isabelle, Matita (and incomplete for Lego, Plastic ). Functionality is similar to those offered by ProofGeneral or CoqIde, but it works inside a web browser, without the need to install anything, no plugins, flush or java. It is developed to work with:- Mozilla based browsers: Mozilla, Firefox, Galeon, ...
- Opera (version 9)
- Internet Explorer (version 5.5, 6, 7) - here some features may not work, due to minor differences in browsers. Since there is noone developing it that uses Windows, as well as little interest, they did not get fixed recently.
Screenshots
(click to see full-size)| Coq in Firefox | Coq in Internet Explorer |
| Lego in Opera (experimental) | Plastic in Konqueror (experimental) |
Try it!
A public version is running on our group server, to try it go to: http://prover.cs.ru.nl/Motivation
The initial idea came from Henk Barendregt, who would like 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:- Showing the proof assistant without installing it
- Giving a proof in an interactive mode on the web (eg Coq Tutorial)
- Presenting libraries (the server includes C-CoRN)
- Experimental features of proof assistants (the server includes Pierre Corbineaus Declarative Proof Language, see documentation)
- 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.
Running the server
Requirements:-
Download the source: Version from Feb 2007 (tgz)
license: GPL.
It is uncommented and undocumented, but this web page is an attempt to change it. - Get CVS/SVN Coq. The undo mechanism uses BackTrack instruction which is available only in those versions
- Get a current OCaml compiler with OCaml-Pcre and OCamlNet (Debian Sid packages are OK)
When running a public server it's highly suggested to do it in a chrooted environment. Creating it is not described here. The server process automatically drops root privileges after binding port 80 (or any other if '-port' is specified). To have internal links working correctly, external address of the server has to be provided with '-localhost' parameter. Example command for running it in a chrooted environment, with a particular version of Coq and with CoRN provided:
sudo chroot ~/coqchroot/ /coqserve -coqtop "nice -n 10 /bin/coqtop.opt -R /files/CoRN--mainline--0--patch-8/ CoRN" -localhost hair-dryer.cs.ru.nl -lego none &> ~/coqchroot/log
Ideas and suggestions
(More are welcome)- Combine it with a Wiki (We are working on it)
- 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)
Security
Security is particularly important in a centralized approach.
The current implementation already provides security by the following means:
- Access is password protected
- The main process runs as a user with no permissions
- It runs in a minimal chrooted environment
- Drop is disabled
- Prover-subprocesses are reniced
- Cpu quota
- Disc quota
- Further Virtualization (Xen and similar solutions)
- Recreation of filesystem
Other provers
The interface has been initially created as a web interface for Coq, and now works also with secure mode Isabelle, and includes preliminary support for Lego and Plastic. 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)
On the other hand, it is hard to imagine a possible adaptation of such an interface to a prover for which the language is the toplevel of a programming language, as it is for example with HOL4 or HOL Light. Both due to lack of a buffer to edit, and due to security concerns (SELinux might help).