dune caches "failing" coqdep invocations even when adding missing files

[Blaisorblade]

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):

[ejgallego]

Thanks for the report @Blaisorblade , that's a bit strange, as in principle dune should reinvoke coqdep if the filesystem layout changes. Let's add a test case to dune test suite to see what is going on.

[ejgallego]

It'd be a good idea to make coqdep fail on missing deps, but that'd break quite a few stuff I understand.

I'm not sure where the Coq discussion about this is, but for OCaml it was discussed in ocaml/ocaml#8625

[Alizter]

@ejgallego I think we called it "strict" for coqdep?

[Blaisorblade]

as in principle dune should reinvoke coqdep if the filesystem layout changes

That does not appear to work either, and I filed #6149 for that since I've just gotten a different unsoundness in dune CI with it. It might be the case that fixing that would fix this bug as well

that'd break quite a few stuff I understand.

I was only suggesting that coqdep to fail if there is a Require that cannot be resolved — because coqc is guaranteed to fail as well on such problems, especially now that coqc and coqdep resolve Requires the same way. When the resolution code differed, the warning was more reasonable.

ocaml/ocaml#8625 shows a problem with wildcards without matches, e.g. *.mli when there's no such file); failing on those errors would be nice but isn't relevant to this issue. (Makefiles might need to be adjusted, tho it would be enough to use e.g. $(wildcard *.mli) instead of *.mli if that's not done already).

[ejgallego]

@Blaisorblade , I think that indeed it is reasonable that coqdep fails more, I fully support that. The trick is to fix all the developments that rely on that broken behavior, there are many!