Planning for dune support (draft)
Supporting dune would let users benefit from the dune cache, composable builds, etc. OTOH, its Coq support still has rough edges; in particular,
make vos and
make validate have no analogue yet.
Ralf was open to supporting dune as long as somebody else volunteered to maintain suport for it: https://mattermost.mpi-sws.org/iris/pl/bjqieom1tjrqmck6ahh9zp5ipc. I volunteer to help; I'd like somebody else to do that as well.
Various increments are possible:
- enable building stdpp without tests
- enable building iris, without tests; here we must choose whether to assume stdpp is installed, or assume it is part of the dune workspace and use compositional builds;
- enable using dune in CI
- document how to take advantage of dune — adding pointers on external docs where possible
- either document work arounds to use with Proof General (add
_CoqProject), or get the issue fixed properly upstream
- migrate tests to dune cram tests (and potentially migrate Makefile.coq.local to support the new syntax)
I have some ideas of the maintenance costs.
- Coq warning flags need be synchronized between coq_makefile and dune
- Tests need be formatted as cram tests