Automatic Test-Case Reduction in Proof Assistants: A Case Study in Coq

TL;DR

This work addresses the challenge of debugging reverse-CI failures in Coq by introducing the Coq Bug Minimizer, which automatically produces minimal, standalone test cases that reproduce buggy behavior. The tool leverages Coq-specific simplification techniques, inlining strategies, and proof-admission to aggressively shrink both code and dependencies while preserving the underlying bug signal, and integrates with coqbot for automatic triggering. Empirical evaluation over 150+ CI failures shows substantial gains: roughly 75% of failures are reduced to smaller test cases, 89% yield standalone reproductions, and the minimized tests are about one-third the size of the originals, with rapid compilation times. The approach includes sophisticated handling of shadowing, global state, and module resolution to enable standalone file generation and practical integration into Coq's internal test suite, offering a scalable path for maintaining compatibility as proof assistants evolve.

Abstract

As the adoption of proof assistants increases, there is a need for efficiency in identifying, documenting, and fixing compatibility issues that arise from proof assistant evolution. We present the Coq Bug Minimizer, a tool for reproducing buggy behavior with minimal and standalone files, integrated with coqbot to trigger automatically on Coq reverse CI failures. Our tool eliminates the overhead of having to download, set up, compile, and then explore and understand large developments: enabling Coq developers to easily obtain modular test-case files for fast experimentation. In this paper, we describe insights about how test-case reduction is different in Coq than in traditional compilers. We expect that our insights will generalize to other proof assistants. We evaluate the Coq Bug Minimizer on over 150 CI failures. Our tool succeeds in reducing failures to smaller test cases in roughly 75% of the time. The minimizer produces a fully standalone test case 89% of the time, and it is on average about one-third the size of the original test. The average reduced test case compiles in 1.25 seconds, with 75% taking under half a second.