Coqoon

Coqoon is an Eclipse plugin providing a feature-complete development environment for Coq projects.

Features

Requirements

Coq

Coq 8.7 and later

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.

Coq 8.5 and Coq 8.6

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.

Java

Coqoon should work with any recent version of the Java virtual machine. See Oracle's Java downloads page.

Eclipse

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.

Operating systems

Coqoon is tested regularly on Windows, Mac OS X and Linux.

Installation

  1. Start Eclipse.
  2. Select the Help → Install New Software... menu option.
  3. Paste the line
    Coqoon - https://www.itu.dk/research/tomeso/coqoon/e42
    into the Work with: text box, and press Enter.
  4. Select the Coqoon → Coqoon feature, and click Next.
  5. Agree to the Coqoon licence agreement, and click Next.

Compliance

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.

Updating

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.

Configuration

Finding the Coq program

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.)

Enabling the Coq perspective

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.

Sample projects

The Odd Order Theorem

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:

  1. Select the File → Import... menu option.
  2. Choose the General → Existing Projects into Workspace option.
  3. Click the Select archive file: radio button, then click the Browse... button.
  4. Select the ZIP archive containing the project.
  5. Click Finish.

Compliance

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.

Software Foundations

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:

  1. Right-click in the Project Explorer and choose Import.
  2. Choose the Git → Project from Git option.
  3. Choose the Clone URI option.
  4. Paste https://github.com/coqoon/Software-Foundations.git into the URI text box, and press Finish.

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.

Development

Source repository

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

Issue tracker

Report bugs, issues and problems using the Coqoon issue tracker.

Contact

Coqoon is managed by Jesper Bengtson and developed by Alexander Faithfull (who also maintains this webpage), based on work by Hannes Mehnert.