Friday 16 December 2016, 10:30: Out-of-order processing of Coq documents, Enrico Tassi (INRIA Sophia-Antipolis).

Coq 8.5 is capable of processing formal documents out-of-order: it focuses his resources on the parts of the document the user is interested in. As a consequence Coq is much more reactive and user interfaces can behave like regular programming environments: the user freely edits the text while the interactive prover checks it in the background, promptly annotating the text with errors or other piece of data, like goal prints.

Coqoon is a user interface for Coq based on Eclipse that takes advantage of this new capability.

In this talk we first demo Coqoon, then we describe how Coq represents the document to be checked and finally we highlight the challenges in processing Coq documents out-of-order.