The Coq mailing list

[Emilio Jesús Gallego Arias <e AT x80.org>]

Abhishek Anand <abhishek.anand.iitg AT gmail.com> writes:

> I hear the word dune thrown around at every build problem. Is there some
> place where this Dune's Coq support is explained, especially what it
> guarantees?

Some pointers are:

- 
https://coq.discourse.group/t/a-guide-to-building-your-coq-libraries-and-plugins-with-dune/20
- 
https://coq.github.io/doc/master/refman/practical-tools/utilities.html?highlight=dune#building-a-coq-project-with-dune
- https://github.com/ejgallego/coq-plugin-template

and of course Dune's own manual. Documentation needs quite a bit of work
yet, as the support is still evolving. A good place to ask is in this
Zulip stream

https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs.20.26.20users

Not sure what you mean by "guarantees", in terms of how dune works there
are some papers and docs, but no complete specification of the internals
[as it is mostly a declarative build language, so the language is
documented]

In terms of Dune's support for Coq, the implementation is quite
straightforward, basically using Dune's internal API to define the right
build rules, the rest is taken care of by Dune itself.

Among other things, Dune does provide sound incremental builds, a global
cache, etc...

Regarding guarantees w.r.t. Coq support, there is still quite a bit of
work to do before we consider Dune's Coq language "stable", but we are
hoping to push upstream some important remaining bits soon.

E.