Coq bench

We bench the Coq opam packages, not Coq itself. The compilation times are only informative. To discuss, there is a live thread on Gitter.


OS Machine OCaml Opam Released Development
Linux x86_64 4.02.3 2.0.1
Linux x86_64 4.05.0 2.0.1
Linux x86_64 4.07.1 2.0.1
Linux x86_64 4.08.1 2.0.5
Linux x86_64 4.09.0 2.0.5


The main aim of Coq bench is to check that all stable Coq packages are working. We check all packages in all versions. We target the current Coq projects and the reproducibility of older ones. We install each package from a fresh Coq install. This is more a checker than a bench. For precise timings, look at If you find a bug in an opam package, please report it on

This website has been running continuously almost since the beginning of the use of opam as a package mananger for Coq. The first commit dates back to February 2015. We host everything on GitHub, both the source code and the website. We run the tests on separated servers, and commit results in GitHub. One needs to be part of the coq-bench organization to have control of everything. A similar project in the OCaml community is


October 5, 2019

  • truncating the logs (maximum 100.000 characters)

August 24, 2019

  • testing coq-intuitionistic-nuprl, again

August 10, 2019

  • add a black-list system for recurring and hard to solve errors (see black_list.rb)

July 23, 2019

June 25, 2019

  • stop testing coq-intuitionistic-nuprl (too slow)

June 20, 2019

  • use the OCaml setup from the opam switch

April 30, 2019

  • test incompatibility with the current OCaml version
  • give the worst test case instead of the best for the summary column

April 7, 2019

  • add Coq 8.9

June 5, 2018

  • add Coq 8.8

November 1, 2017

  • add Coq 8.7

December 29, 2016

  • add Coq 8.6

October 28, 2016

  • add Coq 8.5.3

July 17, 2016

  • add Coq

July 13, 2016

  • upgrade to Coq 8.5.2

May 28, 2016

  • run the opam lint check
  • single-threaded compilation for better reproducibility of builds
  • shorter installation timeout (30 minutes) to anticipate the release of the contribs
  • a timeout is not an error anymore


Send an email to coqbench [at] clarus [dot] me.