Coqoon
Coqoon
复制标题
DOI：
10.1007/s10009-017-0457-2
复制
发表时间：
2016-04
影响因子：
1.5
通讯作者：
A. Faithfull;Jesper Bengtson;Enrico Tassi;C. Tankink
中科院分区：
文献类型：
--
作者：
A. Faithfull;Jesper Bengtson;Enrico Tassi;C. Tankink
交互式证明助手的用户界面始终落后于主流编程语言的用户界面。虽然集成开发环境 (IDE) 支持项目管理、版本控制、依赖关系分析和增量项目编译等功能，但用于证明助手的“IDE”通常仅单独操作文件，依赖外部工具将这些文件集成到更大的项目中。在本文中，我们介绍了 Coqoon，一个集成到 Eclipse 中的 Coq 项目的 IDE。 Coqoon 将证明作为项目而不是孤立的源文件进行管理，并使用 Eclipse 通用构建系统来编译这些项目。 Coqoon 利用 Coq 的最新功能，包括证明的异步和并行处理，并且当与 Eclipse 的第三方 OCaml 扩展一起使用时，甚至可以用于包含 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.