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.
Suggestwill recommend some tactics that might be appropriate to use in the current proof state.
searchwill automatically try to finish the current proof for you.
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:
You can now start CoqIDE from the Start menu.
From Tactician Require Import Ltac1.
To use our automation, you will have to install Coq through the Opam package manager.
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
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
(for convenience, you might consider putting this snippet in a file to execute)
eval $(opam env) && coqide &
Suggestwhile proving a lemma to obtain recommendations for tactics. The tactic
searchwill 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.