Docker-based CI/CD for Rocq/OCaml projects
Érik Martin-Dorel
TL;DR
The paper addresses enabling reproducible, Docker-based CI/CD workflows for Rocq/OCaml projects, with a focus on proof-oriented code bases. It presents three closely related tools—docker-coq, docker-coq-action, and docker-keeper—together with a high-level feature overview, underlying requirements, and design decisions to guide future maintainers, followed by a qualitative evaluation against state-of-the-art approaches. The work traces its origins to presentations at the Coq Workshop and discusses the Rocq rename, underscoring its practical lineage. Overall, the contributions offer a concrete DevOps toolkit to improve build reliability, reproducibility, and collaboration in formal verification projects within the Rocq/OCaml ecosystem.
Abstract
This paper presents three closely-related software projects, namely: docker-coq, docker-coq-action, and docker-keeper. It aims at two objectives: provide a high-level description of the available features -- to foster the use of a Docker-based CI/CD for Rocq (formerly known as Coq) or OCaml projects -- and document the underlying requirements and the main design choices of these three DevOps tools -- to help their future maintainers.