Skip to content

Allow compiling the packages with dune.

Rodolphe Lepigre requested to merge rodolphe/dune into master

This MR adds support for the dune build system (documentation available here), so it is basically an updated version of !387 (closed) (CC @Blaisorblade).

Dune still has many rough edges for projects involving Coq (mostly, it lacks features), but it is still very useful. The main goal of this MR is to allow including stdpp in dune workspaces, which basically allow one to compile (parts of) all involved projects with a single dune build invocation, which is convenient to make changes to several packages at once without having to install the packages at the start of the dependency chain (which does not scale). Another large advantage of compiling with dune is caching, but that is more relevant if you have large projects.

What is included in this MR is:

  • Compilation of the packages only (no tests).
  • Compilation with dune (via make dune) as part of a new CI job.

What is not included in this MR, but could be worked on in subsequent MRs if there is interest:

  • Generate the _CoqProject file depending on how the repo is being used (normal build: use current _CoqProject, dune build: use slightly different _CoqProject, dune workspace build: no _CoqProject since it can get in the way). Note that dune technically does not need a _CoqProject since editors could invoke dune coq top instead of coqtop, but they currently don't by default.
  • Letting dune generate and manage (also install) the opam packages, which would require making dune a hard dependency, but would simplify the infrastructure significantly (no need for patching up _CoqProject with a script).
  • Port the tests to dune cram tests, which could also simplify the infrastructure, but currently requires a slightly more verbose setup.

Merge request reports