PIDE for Asynchronous Interaction with Coq

Carst Tankink 1, *
* Corresponding author
Abstract : This paper describes the initial progress towards integrating the Coq proof assistant with the PIDE architecture initially developed for Isabelle [3]. 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.
Complete list of metadatas

Cited literature [3 references]  Display  Hide  Download

https://hal.inria.fr/hal-01091907
Contributor : Carst Tankink <>
Submitted on : Sunday, December 7, 2014 - 5:26:02 PM
Last modification on : Thursday, February 9, 2017 - 3:47:59 PM
Long-term archiving on: Monday, March 9, 2015 - 6:08:55 AM

File

uitp-2014.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Collections

Citation

Carst Tankink. PIDE for Asynchronous Interaction with Coq. User Interfaces for Theorem Provers, Jul 2014, Vienna, Austria. pp.73 - 83, ⟨10.4204/EPTCS.167.9⟩. ⟨hal-01091907⟩

Share

Metrics

Record views

298

Files downloads

147