Expected Behavior

Assume we use dune (with or without caching enabled). When coqdep outputs

*** Warning: in file foo/bar.v, library baz.quux is required and has not been found in the loadpath!

and we add the missing library, coqdep is rerun and the build works again.

Actual Behavior

The _build folder and (if enabled) the cache are functionally corrupted via the following 3 steps:

1. Thecoqdep invocation returns exit code 0, but it produced the wrong output: foo/bar.v.d does not report the dependency on baz/quux.v (arguably because of coqdep -modules #5100, but we can fix this bug without coqdep -modules #5100). This is harmless with coq_makefile, but terrible in dune's usage (with per-file invocation, and caching). I believe this is a bug.
2. dune doesn't notice the issue in step 1, and considers the invocation successful.
3. Even when adding baz/quux.v, coqdep isn't reinvoked. Since I'm using dune 3.1.1, this is with [coq] Ignore contents in coqdep rule #5547 already included.

I and @Janno found a fix for step 1: we wrap coqdep, and the wrapper fails if coqdep prints anything on stderr.

Reproduction

Specifications

• Version of dune (output of dune --version): 3.1.1

Additional information

• Link to gist with verbose output (run dune with the --verbose flag):