--cache-check-probability gives "false" positives on Coq builds

[Blaisorblade]

Expected Behavior

--cache-check-probability reports no errors on Coq builds.

Actual Behavior

--cache-check-probability reports uninteresting mismatches on .aux files; those should be blacklisted, as they contain Coq's internal timing data.

Details

All of those are noise, and filtering out from dune's log is hard because of how they're reported. This would be easier to deal with if I could just use grep -v for filtering out .foo.aux files. For instance, in the error below discusses multiple files, but comparing hashes (by hand!) reveals only the .aux files differ.

Warning: cache store error [2a6b64b24364e80991d0a8750bc6f6f1]: ((in_cache
((.val_wrap.aux 7edf50c72edb078e83c1b3dc199b16e7) (val_wrap.glob
ddbe510c6e3d743dc1b8c330920555bf) (val_wrap.vo
e7ecba91dd595e37c05d3cc0fb04a720))) (computed ((.val_wrap.aux
d0a4a5a888606817381d68446555e4de) (val_wrap.glob
ddbe510c6e3d743dc1b8c330920555bf) (val_wrap.vo
e7ecba91dd595e37c05d3cc0fb04a720)))) after executing
(mkdir -p _build/default;cd _build/default;
.bin/coqc -q -w -notation-overridden -w -redundant-canonical-projection -w
  -convert_concl_no_check -w -ambiguous-paths -w -custom-entry-overridden -w
  -ssr-search-moved -w +deprecated-hint-without-locality -w
  +deprecated-instance-without-locality -w +unknown-option -w
  -notation-overridden -w -custom-entry-overridden -w
  -redundant-canonical-projection -w -ambiguous-paths -w -ssr-search-moved -w
  +deprecated-hint-without-locality -w +unknown-option -w
  -deprecated-native-compiler-option -w -native-compiler-disabled
  -native-compiler ondemand -Q fmdeps/cpp2v-core/theories/prelude
  bedrock.prelude -R fmdeps/cpp2v-core/theories/lang bedrock.lang
  fmdeps/cpp2v-core/theories/lang/cpp/semantics/val_wrap.v)

There's some discussion/analysis on
https://coq.zulipchat.com/#narrow/stream/240550-Dune-devs-.26-users/topic/.60--cache-check-probability.60.20reports.20.60.2Eaux.60.20files.2C.20which.20a.2E.2E.2E.

[Blaisorblade]

Just run into this "in the wild" without --cache-check-probability.

Warning: cache store error [96783d5ff8ae6414702d0ecb6116c922]: ((in_cache
((.lock_hpp_proof.aux e31f1eea173bb5c9c2bf98de353efc62) (lock_hpp_proof.glob
bf47aa422792d5f827a9c8d968bd1746) (lock_hpp_proof.vo
75f5d7e512ec62130a914cd9224790e1))) (computed ((.lock_hpp_proof.aux
a055b4346356c8fe061db9364ad964c2) (lock_hpp_proof.glob
bf47aa422792d5f827a9c8d968bd1746) (lock_hpp_proof.vo
75f5d7e512ec62130a914cd9224790e1)))) after executing

[ejgallego]

I need to catch up with the discussion, but likely we should just ignore .aux files at all, they are a (wrong) workaround to an upstream design problem.