Coq non-reproducible builds of https://github.com/bedrocksystems/BRiCk/blob/b668f6d062d49deff9d0de27bbdb1df70dd9f0b8/theories/prelude/avl.v

71d94098174fd126280ab786a9d3fbef

build-log.txt

bhv$ (rm -rf _build/default/fmdeps/cpp2v-core/theories/prelude/; DUNE_CACHE_CHECK_PROBABILITY=1 dune b _build/default/fmdeps/cpp2v-core/theories/prelude/)
Warning: cache store error [d3707be2b264ff7d08d25f6f8ec1abd3]: ((in_cache
((avl.glob dc8b0f93f56de739ea8a2bb529819948) (avl.vo
71d94098174fd126280ab786a9d3fbef))) (computed ((avl.glob
dc8b0f93f56de739ea8a2bb529819948) (avl.vo
e406feea41ff15dcd85e9ca21de53beb)))) after executing
(mkdir -p _build/default;cd _build/default;
/Users/pgiarrusso1/.opam/coq-8.16.01-ocaml-4.14.0+flambda/bin/coqc -q -w
  -notation-overridden -w -custom-entry-overridden -w
  -redundant-canonical-projection -w -ambiguous-paths -w
  +deprecated-hint-without-locality -w +deprecated-instance-without-locality
  -w +unknown-option -w -deprecated-native-compiler-option -w
  -native-compiler-disabled -native-compiler ondemand -R
  fmdeps/cpp2v-core/theories/prelude bedrock.prelude
  fmdeps/cpp2v-core/theories/prelude/avl.v)
bhv$ mkdir -p non-repro/avl; cd non-repro/avl
bhv/non-repro/avl$ cp ~/.cache/dune/db/files/v4/71/71d94098174fd126280ab786a9d3fbef .
bhv/non-repro/avl$ cp ~/.cache/dune/db/files/v4/e4/e406feea41ff15dcd85e9ca21de53beb .

e406feea41ff15dcd85e9ca21de53beb

Reproduced using:

• Coq 8.16.0 + 4 commits — 3 backports and a small patch from @Janno, not used here
  https://github.com/Blaisorblade/coq/tree/v8.16-backports
• OCaml 4.14.0 flambda (ocaml-option-flambda.1,ocaml-variants.4.14.0+options)
• Relevant deps:

coq-stdpp            dev.2022-09-29.0.c1e2742a An extended "Standard Library" for Coq
coq-ext-lib          0.11.6                    A library of Coq definitions, theorems, and tactics