Experimental automation for Coq

We are developing new, experimental proof automation using Machine Learning for Coq, and we would like you to help us test it. Participation is completely voluntary.

What do you get? You get to use our newest automation, which should help you prove the theorems you need for your project more quickly. In particular, there are two new commands. Suggest will recommend some tactics that might be appropriate to use in the current proof state. search will automatically try to finish the current proof for you.
What do we get? The version of Coq you can install from this page will collect and upload anonymous usage statistics regarding the new automation (such as how often you use it, and under which circumstances). The data we collect will not be traceable to you, and your participation in this experiment will have no bearing on your final grade for the course. We will also ask you to fill in a short survey at the end of the course.

Installation

See the instructions below. If you run into trouble, please send an email to l.blaauwbroek@cs.ru.nl or ask during the lecture.

Windows

For Windows, we provide a custom Coq installer, that installs Coq together with our automation. The installer can be obtained here. Make sure that you first deinstall all existing versions of Coq before running the installer. Note that this installer is unsigned, so Windows will be reluctant to run the installer. In some warning popups you have to click on "more info" before a button that will run the installer appears.

After the installation is complete, create the file C:\Users\<username>\.coqrc (without an additional .txt extension!) with the following text:

From Tactician Require Import Ltac1.

You can now start CoqIDE from the Start menu.

Linux and MacOS

To use our automation, you will have to install Coq through the Opam package manager. First, install Opam 2.x through the package manager of your linux distribution (in case of MacOS, Homebrew and MacPorts are known to work). You can check that the installed version is newer than 2.0 by running opam --version. Some distributions do not yet include Opam 2.0. For Ubuntu 18.04 and higher a custom ppa is available. On other systems, you can use a binary installation script. After Opam is installend, run the following commands to properly configure it and install Coq with our automation.

opam init --bare # answer yes to any questions the initialization script may ask
opam switch create coq-switch --empty
eval $(opam env)
opam repo add ttc git+https://github.com/LasseBlaauwbroek/ttc-automation.git
opam install --yes coq-tactician-stdlib coqide
tactician enable # answer yes

If the opam install command gives you any trouble, complaining about missing system packages, you can try to run opam depext --install --yes coq-tactician-stdlib coqide instead (it should automatically prompt you to install the system packages).

The installation can take up to an hour. After installation, you can run CoqIde with the command

 eval $(opam env) && coqide &

(for convenience, you might consider putting this snippet in a file to execute)

Usage

After installation using the instructions above, there are two new commands available to you in addition to Coq's normal commands. You can use Suggest while proving a lemma to obtain recommendations for tactics. The tactic search will try to automatically find a proof. You can leave it to run for some time, and if it finds a proof, it prints a witness script that will cache the proof it found. This makes that you don't have to wait very long everytime you reprove a lemma. If the tactic takes too long, you can stop it using the big red button in CoqIde. You can download an example file here.