Dune build system

[rgrinberg]

Experimental port to use dune to build library + tests. The port isn't yet complete, but it's interesting enough for the maintainers to experiment with. If there's interest, I can finish up the port.

Requires dune 2.6+.

• To build $ dune build
• To build & run tests $ dune runtest

cc @ejgallego

[Lysxia]

Thanks @rgrinberg using dune seems especially nice now that you've added support for extraction.

One question: for proof-general/coqide to find the .vo files, is the right way to point _CoqProject to the _build directory?

I can merge this when this is finished.

[Lysxia]

I rebased.

TODO:

• [x] Dunify tutorial/
• [x] Dunify examples/
• [x] Dunify tests/src/Tests.v
• [x] Add script to set up the various _CoqProject so editors can find .vo files; at the same time I think the default should still be for things to work as before for non-dune users for now.
• [x] CI
• [x] doc

[Lysxia]

Thanks again @rgrinberg for initiating this! dune is indeed pretty nice and I'm looking forward to see its Coq support improve further.

• It seems dune doesn't support Coq 8.9, so I just dropped that version too (the make build still works with it, but not for long)
• For extraction I switched to monolithic extraction only. Modular extraction required me to list all modules, which was very brittle because all it takes is one dependency adding one import to break the build.
• I don't know whether or how dune supports building documentation for Coq projects, that's the main reason for still maintaining the make build for now.

[ejgallego]

Glad to hear you found dune coq support useful @Lysxia

• It seems dune doesn't support Coq 8.9, so I just dropped that version too (the make build still works with it, but not for long)

This was a bug, fixed in master, hopefully it will make it to a 2.8.3 or 2.9 release soon. Sorry for that.

• For extraction I switched to monolithic extraction only. Modular extraction required me to list all modules, which was very brittle because all it takes is one dependency adding one import to break the build.

I'm sure we can improve that, and other work on tooling seems to finally be progressing in Coq so we can actually have some hope for a better integration. Please feel free to submit a feature request to Dune's bug tracker.

• I don't know whether or how dune supports building documentation for Coq projects, that's the main reason for still maintaining the make build for now.

Not yet but it is a top priority; Coq upstream needs it for the standard library so we can remove another bit of make stuff there.

[Lysxia]

Heh, 2.8.3 came out an hour ago. Thanks for the info @ejgallego !

[ejgallego]

Thanks a lot @rgrinberg for the release! @clarus , I'm pinging you here and hopefully dune 2.8.3 should fix all the problems you had in coq.io with 8.9, let me know in Zulip if that is not the case.

[clarus]

@ejgallego OK thanks!