[draft] Preliminary support for building with Dune

[ejgallego]

Dear CompCert developers, this is a proof-of-concept highlighting a full build of x86 using the Dune build system.

The PR is not meant to be merged yet, but as a demonstration and to gather feedback. In particular, it has a few quirks that should be solved soon Dune upstream:

• no proper configuration
• mixed Coq/ML dirs require a hack
• only works with Dune master

IMHO, I think it would make sense to eventually finish and merge this PR, either as the main build system, or as secondary one, to be used in Coq's Continous Integration system.

Dune support is very interesting for Coq developers as it allows for composed, incremental builds with Coq itself; this means a large speed-up in practice.

[bschommer]

Thanks for the work, I already played around a little bit with using dune only for the OCaml part of CompCert, but did not try to port the Coq part. I think switching to dune would be an option, given that Coq and menhir now require dune and we would introduce an additional dependency and it works nicely under windows, but I don't think that we want to maintain a secondary build system.

[ejgallego]

I could take care of the maintenance at least for the time we consider Coq dune support experimental, so still you folks consider the official build system the make-based one.

[bschommer]

One thing I noticed is that the warning flags change which is probably due to fact that the coq code triggers some warnings that we don't want in the other parts. It seems to me that from dune side there was no real interest in allowing different flags for different files but the suggestion was rather to produce suppress directives in the code generator.

[ejgallego]

Thanks for the observation @bschommer ; having different flags for different files should be OK I think [IIUC] , I will investigate.

We are reworking a bit the directory mode of Dune so I will update this PR to a much cleaner [IMO] version.