Welcome
iCoq is a tool for regression proof selection in largescale Coq verification projects, suitable for use with continuous integration services, e.g., Travis CI. It can also be used locally, as a replacement for coq_makefile.
Overview
Proof assistants such as Coq are used to construct and check formal proofs in many largescale verification projects. As proofs grow in number and size, the need for tool support to quickly find failing proofs after revising a project increases. We present a technique for largescale regression proof selection, suitable for use in continuous integration services, e.g., Travis CI. We instantiate the technique in a tool dubbed iCoq. iCoq tracks finegrained dependencies between Coq definitions, propositions, and proofs, and only checks those proofs affected by changes between two revisions. iCoq additionally saves time by ignoring changes with no impact on semantics. We applied iCoq to track dependencies across many revisions in several large Coq projects and measured the time savings compared to proof checking from scratch and when using Coq's timestampbased toolchain for incremental checking. Our results show that proof checking with iCoq is up to 10 times faster than the former and up to 3 times faster than the latter.
Installation
 Install Java 8 and make sure the Java executable is in the PATH.
 Install OPAM 1.2.2.

Install OCaml 4.05 via OPAM:
$ opam switch 4.05.0
$ eval `opam config env` 
Add the iCoq OPAM package repository:
$ opam repo add proofengineeringdev http://opamdev.proofengineering.org 
Install iCoq and its dependencies:
$ opam install icoq
Components
Component  Language  Description 

coqast  OCaml  compute digests of Coq term ASTs 
coqdepends  OCaml  extract dependencies from Coq term ASTs 
coqdigest  OCaml  compute digests of Coq proof scripts 
coqc  OCaml  Coq proofchecking dependency extraction 
graph builder  Java  construct/maintain dependency graphs 
proof runner  bash  execute proofs 
Contact
Please send comments or questions to Ahmet Celik.