Proof in Context -- Web Editing with Rich, Modeless Contextual Feedback

TL;DR

This paper introduces Agora, a web-based collaborative system for formal mathematics that features a reusable, context-aware proof editor supporting various tools, including interactive theorem provers like Coq.

Contribution

It presents the design of a generic, asynchronous proof editor supporting multiple tools and contextual feedback, with detailed focus on integration with Coq.

Findings

Designed a flexible, reusable proof editor component.

Enabled collaborative formal mathematics editing online.

Integrated interactive theorem prover support, exemplified with Coq.

Abstract

The Agora system is a prototypical Wiki for formal mathematics: a web-based system for collaborating on formal mathematics, intended to support informal documentation of formal developments. This system requires a reusable proof editor component, both for collaborative editing of documents, and for embedding in the resulting documents. This paper describes the design of Agora's asynchronous editor, that is generic enough to support different tools working on editor content and providing contextual information, with interactive theorem proverss being a special, but important, case described in detail for the Coq theorem prover.