Coqdoc flags --with-header and --with-footer should imply a dependency on the argument files

[rlepigre]

The --with-header and --with-footer arguments of coqdoc (specified via a (coqdoc_flags ...) thingy) have file argument that should be dependencies of all the generated documentation files. It appears that they are currently not considered dependencies, which means that the documentation is not recompiled when the header / footer files change. (And the situation is worse when using the cache.)

To work around this, I typically put these files in /tmp/some_folder/ using a wrapper makefile, and disable the cache. However, this leads to very long building times that could otherwise mostly hit the cache.

[ejgallego]

That should be really easy to fix, I wonder tho if dune can support having (coqdoc_flags (--with-header=%{dep:foo.html})) directly?

Fix can be either by:

• analizing the flags and injecting the deps
• adding / refining a new field for the header options

[Alizter]

I would suggest adding a new field for these kinds of options. The general coqdoc_flags field can be thought of as a last-resort tweak for features unsupported. Having a dedicated fields will allow you to unambiguously expand passed arguments by using all the stanza magic we have in dune.