Treffer: Coqoon: An IDE for interactive proof development in Coq.

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 plug-ins. [ABSTRACT FROM AUTHOR]

Copyright of International Journal on Software Tools for Technology Transfer is the property of Springer Nature and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)