Coqoon

Abstract : User interfaces for interactive proof assistants have always lagged behind those for mainstream programming languages. Whereas integrated development environments (IDEs) have support for features like project management, version control, dependency analysis and incremental project compilation, " IDE " s for proof assistants typically only operate on files in isolation, relying on external tools to integrate those files into larger projects. In this paper we present Coqoon, an IDE for Coq projects integrated into Eclipse. Coqoon manages proofs as projects rather than isolated source files, and compiles these projects using the Eclipse common build system. Coqoon takes advantage of the latest features of Coq, including asynchronous and parallel processing of proofs, and—when used together with a third-party OCaml extension for Eclipse—can even be used to work on large developments containing Coq plugins.
Complete list of metadatas

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/hal-01410450
Contributor : Enrico Tassi <>
Submitted on : Tuesday, December 6, 2016 - 4:20:45 PM
Last modification on : Friday, March 22, 2019 - 4:46:03 PM
Long-term archiving on : Thursday, March 23, 2017 - 1:16:13 AM

File

main-sttt.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01410450, version 1

Collections

Citation

Alexander Faithfull, Jesper Bengtson, Enrico Tassi, Carst Tankink. Coqoon. International Journal on Software Tools for Technology Transfer, Springer Verlag, 2017. ⟨hal-01410450⟩

Share

Metrics

Record views

233

Files downloads

105