Skip to Main content Skip to Navigation
New interface
Documents associated with scientific events

A Nix toolbox for reproducible Coq environments, Continuous Integration and artifact reuse

Cyril Cohen 1 Théo Zimmermann 2, 3 
1 STAMP - Sûreté du logiciel et Preuves Mathématiques Formalisées
CRISAM - Inria Sophia Antipolis - Méditerranée
3 PI.R2 - Design, study and implementation of languages for proofs and programs
CNRS - Centre National de la Recherche Scientifique, Inria de Paris, UPCité - Université Paris Cité, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale
Abstract : When using or contributing to a Coq project (especially one with third party dependencies), it can be difficult and annoying to install the exact set of dependencies at the versions the maintainers recommend. It is more convenient when projects provide an easy way to set everything up to be ready to code, even more so if the dependencies can be quickly fetched in pre-compiled form. Nonetheless, it is also important to preserve the flexibility for project maintainers to test their projects against alternative versions (releases and development) of the dependencies, both while developing locally and in a distant Continuous Integration service (CI). Finally, being able to test that candidate changes do not break reverse dependencies (i.e., packages that depend on the project) is essential to bring confidence to project maintainers. We have designed the Coq Nix toolbox which relies on Nix [3] to allow for better sharing of configurations and pre-compiled packages across several projects. This toolbox makes it easy to setup a project and generates CI configurations to test multiple versions of the dependencies and compatibility with reverse dependencies. It enables the use of a single command nix-shell to get the same working environment for every developer. This also saves compilation time since developers and users may download packages that have already been compiled in CI.
Complete list of metadata

https://hal.inria.fr/hal-03366644
Contributor : Théo Zimmermann Connect in order to contact the contributor
Submitted on : Tuesday, October 5, 2021 - 5:30:06 PM
Last modification on : Tuesday, September 6, 2022 - 1:26:59 PM
Long-term archiving on: : Thursday, January 6, 2022 - 8:16:45 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03366644, version 1

Citation

Cyril Cohen, Théo Zimmermann. A Nix toolbox for reproducible Coq environments, Continuous Integration and artifact reuse. The Coq Workshop, Jul 2021, Virtual, France. ⟨hal-03366644⟩

Share

Metrics

Record views

49

Files downloads

72