Skip to content

Instantly share code, notes, and snippets.

@Blaisorblade

Blaisorblade/71d94098174fd126280ab786a9d3fbef

Last active January 13, 2023 11:34
Show Gist options
  • Save Blaisorblade/cd953398a241c17002b1d903806c2bea to your computer and use it in GitHub Desktop.
Save Blaisorblade/cd953398a241c17002b1d903806c2bea to your computer and use it in GitHub Desktop.
Download ZIP
Raw
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 .
Raw
e406feea41ff15dcd85e9ca21de53beb
This file has been truncated, but you can view the full file.
View raw
@Blaisorblade
Copy link
Author

Reproduced using:

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment