Stream: Dune devs & users

Topic: `--cache-check-probability` reports `.aux` files, which a...


view this post on Zulip Paolo Giarrusso (Jul 20 2022 at 11:01):

@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

view this post on Zulip Janno (Jul 20 2022 at 11:02):

What do .aux files depend on, actually?

view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Jul 20 2022 at 11:03):

I assume what changed is the timing below 0.778

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"

view this post on Zulip Paolo Giarrusso (Jul 20 2022 at 11:04):

@Janno no: deps (universe) is for sound builds and means "always rebuild".

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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 ).

view this post on Zulip Rudi Grinberg (Jul 25 2022 at 21:17):

do we depend on .aux files to build anything inside dune?

view this post on Zulip 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.

view this post on Zulip Rudi Grinberg (Jul 25 2022 at 21:20):

dune's cache will of course not restore them then

view this post on Zulip Paolo Giarrusso (Jul 26 2022 at 00:43):

Dune _mostly_ worked when not listing them as target — you changed that in https://github.com/ocaml/dune/pull/3721.

view this post on Zulip 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.


Last updated: Feb 04 2023 at 02:03 UTC