--cache-check-probability gives "false" positives on Coq builds #6004
Description
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.