Coqoon is an Eclipse plugin providing a
feature-complete development environment for Coq
projects.
Coqoon works well with other Eclipse plugins — add more to add new features like version control or support for embedded OCaml plugins.
Automatically rebuild dependencies when proof scripts change, and forget about manual load path configuration.
Structure Coq developments like Java
projects, manage project
interdependencies with a user
interface, and avoid cluttering source
folders with .vo files.
All Coqoon projects come with a configure
script, so they can be built and developed even without
using Coqoon.
Coqoon takes advantage of all the latest changes to Coq: edit proofs asynchronously and get automatic feedback, or use the quick compilation chain to compile a colossal project in just a few minutes.
Coqoon uses the coqidetop protocol supported by recent
versions of Coq to provide an editor with interactive responses.
This editor is not yet the default; to use it, right-click on
a .v file and choose the
Open With →
Coq Editor (v8.7+, coqidetop) item.
Coqoon uses the PIDEtop plugin to provide an editor with interactive
responses when used with Coq 8.5 and Coq 8.6.
For Windows users, a binary
version of the plugin for Coq 8.5pl2 is available; for other
platforms, or for other versions of Coq, the plugin should be built
from the
latest version of the source code. (When building PIDEtop, note that the trailing
slash in the COQBIN variable is required.)
Note that PIDEtop can also be installed using the OPAM integration feature; see the PIDEtop installation instructions for more details.
See the PIDEtop installation instructions for more details.
The PIDEtop plugin was last updated on February 16th, 2016; we recommend that all users update to the latest version.
Coqoon should work with any recent version of the Java virtual machine. See Oracle's Java downloads page.
Coqoon requires version 4.2 (Juno) or later of Eclipse, available from the Eclipse downloads page.
As the examples are hosted in a Git repository, we recommend a package that includes Git support out of the box, such as the Eclipse IDE for Java Developers.
Coqoon is tested regularly on Windows, Mac OS X and Linux.
Coqoon - https://www.itu.dk/research/tomeso/coqoon/e42into the Work with: text box, and press Enter.
The Coqoon repository contains a compiled copy of OcaIDE; in order to comply with its licence, we also make a copy of its source code available.
New versions of Coqoon are released frequently to add new features, fix bugs, and improve performance. To update Coqoon to the most recent version, select the Help → Check for Updates menu option.
The most recent version of Coqoon is v0.8.4, released on December 12th, 2018; for more information, see the Coqoon changelog.
Coqoon will search some system folders for Coq, but if it can't find it—or if it finds the wrong version—you may need to manually specify the the folder that contains the coqtop program.
If you're using the OPAM integration feature, then the version of Coq installed in the active OPAM root will automatically be used.
To specify the path, select the
Window → Preferences (or
Eclipse → Preferences on
Mac OS X) menu option, choose the Coqoon
category, and then click Browse
to choose the correct folder.
If you're using Coqoon with OCaml integration, note that OcaIDE ignores this setting, and will only look for Coq in your configured path, or in the folder specified by the COQBIN environment variable. (We expect to fix this issue soon.)
The default Eclipse user interface configuration does not show any Coq-specific views. To enable these, select the Window → Open Perspective → Other... menu option, choose Coq, and click OK.
To show that Coqoon can be used to work with even the most complex Coq projects, we provide a pre-packaged version of the Microsoft Research / INRIA formalisation of the odd order theorem.
We recommend that this project be compiled using the quick compilation chain. To enable it, select the Window → Preferences (or Eclipse → Preferences on Mac OS X) menu option, choose the Coqoon category, and then tick the box labelled Enable the quick compilation process (experimental, Coq 8.5+).
This project contains an embedded OCaml plugin, so the OcaIDE integration for Coqoon feature and its dependencies must be installed to build it correctly.
To import this project into Coqoon, follow these steps:
The packaged version omits several non-Coq files from the Mathematical Components library; in order to comply with its licence, we also make a copy of the full source code available.
We also provide a version of Benjamin Pierce's Software Foundations course, modified to be compatible with the Coq 8.5 series. The easiest way to import it is to use Eclipse's integrated Git support:
This process will create a local copy of the Software Foundations repository on your computer; to import the project again, you should use this local copy directly by choosing the Existing local repository option instead of Clone URI.
To fetch updates from the Software Foundations repository and incorporate them into your local copy, open the Git Repositories view (Window → Show View → Other... → Git → Git Repositories), right-click the Software-Foundations entry, and click Pull.
Coqoon's source code is hosted on GitHub, and can be checked out anonymously using the command
git clone git://github.com/coqoon/coqoon.git
Report bugs, issues and problems using the Coqoon issue tracker.
Coqoon is managed by Jesper Bengtson and developed by Alexander Faithfull (who also maintains this webpage), based on work by Hannes Mehnert.