`--cache-check-probability` reports `.aux` files, which a... · Dune devs & users

@Janno just suggested we use --cache-check-probability=0.01 to double-check our Coq builds are reproducible, but it doesn't seem usable — .aux files contain timing info and aren't meant to be reproducible. Below an example. AFAICT, the hashes imply that .glob and .vo have the same hash, but .aux files don't; a few other instances seem to match, but I haven't implemented a log parser to check that _all_ warnings are this kind of false positive.

BTW, should "Warning: cache store error" read "Warning: non-reproducible build results detected", and possibly tell which hash changed?

dune build --cache-check-probability=0.01 fmdeps/cpp2v-core/

real    0m1.078s
user    0m0.015s
sys 0m0.693s
 llvm-config fmdeps/cpp2v-core/build/llvm-lib-path.txt
         sed fmdeps/cpp2v-core/build/llvm-lib-path.txt
        coqc fmdeps/cpp2v-core/theories/lang/cpp/semantics/.val_wrap.aux,fmdeps/cpp2v-core/theories/lang/cpp/semantics/val_wrap.{glob,vo}
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)

real    0m2.005s
user    0m1.260s
sys 0m0.446s

Janno (Jul 20 2022 at 11:02):

Janno (Jul 20 2022 at 11:03):

The docs for dune reproducibility checks mention: To prevent Dune from caching such rules, mark them as non-reproducible by using (deps (universe)). Is that something we can implement?

Paolo Giarrusso (Jul 20 2022 at 11:03):

COQAUX1 c08c45ba8defa4c5d7d4526791afc78b /Users/pgiarrusso1/git-bedrock/bhv-notation/_build/default/fmdeps/cpp2v-core/theories/lang/cpp/semantics/val_wrap.v
0 0 vo_compile_time "0.778"

Paolo Giarrusso (Jul 20 2022 at 11:04):

Janno (Jul 20 2022 at 11:06):

And I suspect (given the contents) there is no way to build .aux files separately from the associated .vo files, right?

Paolo Giarrusso (Jul 20 2022 at 11:08):

Yep. I'm sure that Dune devs will have objections to the very concept of .aux files; but today they're only used for IDE heuristics, so Coq builds don't have actual soundness problem with it. And AFAICT it's also fine to use reuse .aux files from the cache.

Paolo Giarrusso (Jul 20 2022 at 11:11):

Either way, I'd like to _not_ get this discussion sidetracked by redesigning .aux files. It'd be good to use this option to detect if _important_ outputs are non-reproducible — I'd definitely want to know. And I imagine Coq devs should enable this as well in their CI (cc @Ali Caglayan @Emilio Jesús Gallego Arias ).

Rudi Grinberg (Jul 25 2022 at 21:17):

Rudi Grinberg (Jul 25 2022 at 21:19):

If we don't, perhaps we just remove them from the list of targets of coqc rules.

Rudi Grinberg (Jul 25 2022 at 21:20):

Paolo Giarrusso (Jul 26 2022 at 00:43):

Emilio Jesús Gallego Arias (Jul 26 2022 at 15:43):

I think the best for now is to live with non-reproducible .aux files, and have a PR that disables them in Dune.