Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

coq-bedrock2 failing in Coq bench #451

Closed
SkySkimmer opened this issue Mar 11, 2025 · 4 comments
Closed

coq-bedrock2 failing in Coq bench #451

SkySkimmer opened this issue Mar 11, 2025 · 4 comments

Comments

@SkySkimmer
Copy link
Contributor

eg https://coq.gitlabpages.inria.fr/-/coq/-/jobs/5442253/artifacts/_bench/logs/coq-bedrock2.NEW.opam_install.1.stdout.log

- File "/home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-bedrock2.dev/bedrock2/src/bedrock2Examples/LAN9250.v", line 207, characters 21-31:
- Error: The reference string_dec was not found in the current environment.
- 
- Command exited with non-zero status 1
- /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-bedrock2.dev/bedrock2/src/bedrock2Examples/LAN9250.vo (real: 0.34, user: 0.27, sys: 0.07, mem: 438856 ko)
- make[3]: *** [Makefile.coq.ex:814: /home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-bedrock2.dev/bedrock2/src/bedrock2Examples/LAN9250.vo] Error 1
- make[3]: *** [/home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-bedrock2.dev/bedrock2/src/bedrock2Examples/LAN9250.vo] Deleting file '/home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-bedrock2.dev/bedrock2/src/bedrock2Examples/LAN9250.glob'
- make[2]: *** [Makefile.coq.ex:412: all] Error 2
- make[1]: *** [Makefile:71: ex] Error 2
- make[1]: Leaving directory '/home/gitlab-runner/builds/v6HyzL39/0/coq/coq/_bench/opam.NEW/ocaml-NEW/.opam-switch/build/coq-bedrock2.dev/bedrock2'
- make: *** [Makefile:90: bedrock2_ex] Error 2


<><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
┌─ The following actions failed
│ λ build coq-bedrock2 dev
@samuelgruetter
Copy link
Contributor

After bumping coqutil, I also get this error using Coq 8.18.0.
@DIJamner do you remember if, before merging mit-plv/coqutil#127, you tested whether that still builds with bedrock2?

@DIJamner
Copy link
Contributor

I didn't test this, I'll figure out and fix whatever the problem is.

@DIJamner
Copy link
Contributor

I put the fix in PR #452 to make sure it successfully builds before merging. It seems like somehow the order of transitive imports changed, which affected the resolution of a relative module path, so I qualified the import.

@SkySkimmer
Copy link
Contributor Author

Seems to work indeed

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants