PIDE for Asynchronous Interaction with Coq

TL;DR

This paper presents initial progress in integrating the Coq proof assistant with the PIDE architecture, enabling asynchronous, parallel interaction similar to Isabelle, through architectural generalizations and protocol adaptation.

Contribution

It introduces a generalized PIDE architecture for multiple proof assistants and adapts Coq to support asynchronous interaction, expanding PIDE's applicability beyond Isabelle.

Findings

Achieved a working Coq-PIDE integration in about two months.

Generalized PIDE architecture to support multiple proof assistants.

Demonstrated asynchronous interaction with Coq using the adapted protocol.

Abstract

This paper describes the initial progress towards integrating the Coq proof assistant with the PIDE architecture initially developed for Isabelle. The architecture is aimed at asynchronous, parallel interaction with proof assistants, and is tied in heavily with a plugin that allows the jEdit editor to work with Isabelle. We have made some generalizations to the PIDE architecture to accommodate for more provers than just Isabelle, and adapted Coq to understand the core protocol: this delivered a working system in about two man-months.