bedrock2 icon indicating copy to clipboard operation
bedrock2 copied to clipboard

Build fails on master, blocking Coq bench

Open JasonGross opened this issue 1 month ago • 1 comments

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

JasonGross avatar Nov 03 '25 15:11 JasonGross

cc @andres-erbsen

JasonGross avatar Nov 03 '25 15:11 JasonGross