Welcome

iCoq is a tool for regression proof selection in large-scale 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 large-scale 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 large-scale 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 fine-grained 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 timestamp-based 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

  1. Install Java 8 and make sure the Java executable is in the PATH.
  2. Install OPAM 1.2.2.
  3. Install OCaml 4.05 via OPAM:
      $ opam switch 4.05.0
      $ eval `opam config env`
  4. Add the iCoq OPAM package repository:
      $ opam repo add proofengineering-dev http://opam-dev.proofengineering.org
  5. Install iCoq and its dependencies:
      $ opam install icoq

Components

Component Language Description
coq-ast OCaml compute digests of Coq term ASTs
coq-depends OCaml extract dependencies from Coq term ASTs
coq-digest OCaml compute digests of Coq proof scripts
coqc OCaml Coq proof-checking dependency extraction
graph builder Java construct/maintain dependency graphs
proof runner bash execute proofs

Contact

Please send comments or questions to Ahmet Celik.