Welcome

Welcome to iCoq home page. iCoq is a tool for regression proof selection for large-scale Coq verification projects, suitable for use with continuous integration services, e.g., Travis CI (or locally).

Abstract

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.

Components

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

Download

iCoq is currently distributed as an archive file. You can download the archive here. We provide a README file in the archive. Run this file to try the tool on Verdi Raft.

Installation

    1. Install Ocaml (>= 4.05.0) and Opam (https://opam.ocaml.org/doc/Install.html). After the installation is done, setup opam by executing the following commands:
      $ opam switch 4.05.0 # opam switch create 4.05.0
      $ eval `opam config env`
    2. Add the iCoq repo:
      $ opam repo add proofengineering-dev http://opam-dev.proofengineering.org
    3. Install Coq 8.5.3:
      $ opam pin add coq 8.5.3~depends
    4. Install coq-ast and coq-depends:
      $ opam install coq-ast coq-depends
    5. Install mathcomp:
      $ opam install coq-mathcomp-ssreflect
Additionally, Java 8 has to be installed and Java executable needs to be on the PATH enviroment variable.

Contact

Please send comments or questions to Ahmet Celik.