Allow compiling the packages with dune.
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 thatdune
technically does not need a_CoqProject
since editors could invokedune coq top
instead ofcoqtop
, 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.