Emilio J. Gallego Arias
Mines ParisTech, PSL Research University
Towards Hybrid Theorem Proving Interfaces
-----------------------------------------
[joint work with B. Pin, P. Jouvelot]
We will present recent work in jsCoq, a port of the Coq proof
assistant to the HTML5 platform, and SerAPI, a low-level interface for
Coq based on automatic datatype serialization.
jsCoq aims to enrich regular documents --- such as math proofs, books,
or teaching material --- with interactive theorem proving
capabilities.
jsCoq provides a self-contained, complete Coq system that can be run
in the browser, without external components or servers. The idea is to
distribute the Coq environment and libraries with the document,
avoiding painful installation and compatibility problems. Popular Coq
teaching texts are supported, as well as many popular third party
libraries. Running two different Coq versions is as easy as opening
two browser tabs.
The current working prototype(s) can be accessed at
https://github.com/ejgallego/jscoq; note that they still are in heavy
development.
The new browser environment provides a rich set of JavaScript
libraries and API that allow for new modes of document navigation and
display, however, we quickly hit some limitations of the current Coq
architecture --- still mainly targeted at console display.
In order to overcome this limitation, and based in our experience
implementing the first version of jsCoq, we have developed, SerAPI, a
new Coq protocol for UIs based on serialization. SerAPI is at the core
of the second version of jsCoq, and intends to provide general
advanced UI support to interested Coq IDEs.