bedrock2
bedrock2 copied to clipboard
Build fails on master, blocking Coq bench
Coq has not been benching fiat crypto for a while because bedrock 2 is failing with
# [...]
# The term "impl1_refl" has type "impl1 (seps Frame) (seps Frame)"
# while it is expected to have type "impl1 (seps Frame) (seps Rs)"
# (cannot unify "seps Frame x" and "seps Rs x").
#
# Command exited with non-zero status 1
# /home/gitlab-runner/builds/v6HyzL39Q/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-bedrock2.dev/bedrock2/src/bedrock2/SepCalls.vo (real: 0.34, user: 0.27, sys: 0.07, mem: 442136 ko)
# make[3]: *** [Makefile.coq.noex:813: /home/gitlab-runner/builds/v6HyzL39Q/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-bedrock2.dev/bedrock2/src/bedrock2/SepCalls.vo] Error 1
# make[3]: *** [/home/gitlab-runner/builds/v6HyzL39Q/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-bedrock2.dev/bedrock2/src/bedrock2/SepCalls.vo] Deleting file '/home/gitlab-runner/builds/v6HyzL39Q/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-bedrock2.dev/bedrock2/src/bedrock2/SepCalls.glob'
This is on make bedrock2_ex https://github.com/rocq-prover/opam/blob/581a115813d9205dde521e1a3d34f0689fb5128d/extra-dev/packages/coq-bedrock2/coq-bedrock2.dev/opam#L12 / https://github.com/rocq-prover/opam/blob/581a115813d9205dde521e1a3d34f0689fb5128d/extra-dev/packages/coq-fiat-crypto-with-bedrock/coq-fiat-crypto-with-bedrock.dev/opam#L14
cc @andres-erbsen