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:

1. enable building stdpp without tests
2. 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;
3. enable using dune in CI
4. document how to take advantage of dune — adding pointers on external docs where possible

• either document work arounds to use with Proof General (add _build/default to _CoqProject), or get the issue fixed properly upstream

5. 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