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.

Sign up for GitHub

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

Jump to bottom

Compilation error with Coq 8.16.0 #1

Open
RyanGlScott opened this issue Nov 17, 2022 · 4 comments
Open

Compilation error with Coq 8.16.0 #1

RyanGlScott opened this issue Nov 17, 2022 · 4 comments

Comments

@RyanGlScott
Copy link
Collaborator

entree-specs (as of commit bfdeb73) builds with Coq 8.15.2 and earlier, but fails to build with Coq 8.16.0:

$ make
<elided>
COQC theories/Core/EnTreeDefinition.v
COQC theories/Eq/Eqit.v
COQC theories/Core/SubEvent.v
COQC theories/Ref/Padded.v
COQC theories/Ref/EnTreeSpecDefinition.v
COQC theories/Ref/MRecSpec.v
COQC theories/Ref/EnTreeSpecFacts.v
File "./theories/Ref/EnTreeSpecFacts.v", line 735, characters 31-49:
Error: Cannot find an homogeneous relation to rewrite.

make[1]: *** [Makefile.coq:793: theories/Ref/EnTreeSpecFacts.vo] Error 1
make: *** [Makefile.coq:409: all] Error 2

The failing line is here:

entree-specs/theories/Ref/EnTreeSpecFacts.v

Line 735 in bfdeb73

specialize (REL b). setoid_rewrite REL. rewrite tau_eutt. reflexivity.

RyanGlScott added a commit to GaloisInc/saw-script that referenced this issue Dec 9, 2022
@RyanGlScott
Install entree-specs as a Coq dependency
d2d9f01 
This updates the CI to build a particular `entree-specs` commit before building
the Coq support libraries. This also updates the instructions in the
`saw-core-coq` `README` accordingly.

Note that this requires limiting the Coq support window to 8.15 for now, as
`entree-specs` requires 8.15 as the minimum. In particular, `entree-specs`
does not yet support 8.16 (see GaloisInc/entree-specs#1), so we now require
Coq 8.15 exactly.
@RyanGlScott RyanGlScott mentioned this issue Oct 16, 2024
Merged
RyanGlScott added a commit that referenced this issue Oct 16, 2024
@RyanGlScott
opam: Require coq < 8.16
6ded0be 
`entree-specs` is not currently buildable with Coq 8.16 or later. See #1. As
such, we prevent these versions of Coq from being included in build plans by
excluding them at the `opam` file level.
RyanGlScott added a commit that referenced this issue Oct 16, 2024
@RyanGlScott
opam: Require coq < 8.16
ead10bf 
`entree-specs` is not currently buildable with Coq 8.16 or later. See #1. As
such, we prevent these versions of Coq from being included in build plans by
excluding them at the `opam` file level.
@pennyannn
Copy link

pennyannn commented Nov 11, 2024 •
edited
Loading

Run into a similar issue in AWS-LC-verification CI. The error output:

entree-specs is now pinned to git+https://github.com/GaloisInc/entree-specs.git#52c4868f1f65c7ce74e90000214de27e23ba98fb (version dev)
2024-11-11T22:49:31.4310095Z #12 380.5 
2024-11-11T22:49:35.9661115Z #12 385.2 The following actions will be performed:
2024-11-11T22:49:35.9662177Z #12 385.2   - install entree-specs dev*
2024-11-11T22:49:36.1169597Z #12 385.2 
2024-11-11T22:49:36.1170177Z #12 385.2 <><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><><><>
2024-11-11T22:49:44.3943045Z #12 393.6 [ERROR] The compilation of entree-specs failed at "/usr/bin/make".
2024-11-11T22:49:44.3943796Z #12 393.6 
2024-11-11T22:49:44.3944371Z #12 393.6 #=== ERROR while compiling entree-specs.dev ===================================#
2024-11-11T22:49:44.3945939Z #12 393.6 # context              2.0.5 | linux/x86_64 | ocaml-system.4.08.1 | pinned(git+https://github.com/GaloisInc/entree-specs.git#52c4868f1f65c7ce74e90000214de27e23ba98fb#52c4868f)
2024-11-11T22:49:44.3947324Z #12 393.6 # path                 ~/.opam/default/.opam-switch/build/entree-specs.dev
2024-11-11T22:49:44.3947886Z #12 393.6 # command              /usr/bin/make
2024-11-11T22:49:44.3948289Z #12 393.6 # exit-code            2
2024-11-11T22:49:44.3948783Z #12 393.6 # env-file             ~/.opam/log/entree-specs-27116-2dea01.env
2024-11-11T22:49:44.3949437Z #12 393.6 # output-file          ~/.opam/log/entree-specs-27116-2dea01.out
2024-11-11T22:49:44.3949944Z #12 393.6 ### output ###
2024-11-11T22:49:44.3950229Z #12 393.6 # [...]
2024-11-11T22:49:44.3950545Z #12 393.6 # COQC theories/Core/EnTreeDefinition.v
2024-11-11T22:49:44.3950955Z #12 393.6 # COQC theories/Eq/Eqit.v
2024-11-11T22:49:44.3951331Z #12 393.6 # COQC theories/Core/SubEvent.v
2024-11-11T22:49:44.3951717Z #12 393.6 # COQC theories/Ref/Padded.v
2024-11-11T22:49:44.3952140Z #12 393.6 # COQC theories/Ref/EnTreeSpecDefinition.v
2024-11-11T22:49:44.3952582Z #12 393.6 # COQC theories/Ref/MRecSpec.v
2024-11-11T22:49:44.3953001Z #12 393.6 # COQC theories/Ref/EnTreeSpecFacts.v
2024-11-11T22:49:44.3953585Z #12 393.6 # File "./theories/Ref/EnTreeSpecFacts.v", line 432, characters 60-101:
2024-11-11T22:49:44.3954281Z #12 393.6 # Error: No such goal. The current bullet * is unfinished.
2024-11-11T22:49:44.3954937Z #12 393.6 # 
2024-11-11T22:49:44.3956225Z #12 393.6 # make[1]: *** [Makefile.coq:764: theories/Ref/EnTreeSpecFacts.vo] Error 1
2024-11-11T22:49:44.3957080Z #12 393.6 # make: *** [Makefile.coq:387: all] Error 2

But this is with coq.8.15.1, so I'm not sure what is going on. The CI used to be passing with this version of Coq and entree-specs is pinned to be #52c4868f.

@sauclovian-g
Copy link
Contributor

That is entree-specs #7, so you should be able to fix it by updating.

@sauclovian-g
Copy link
Contributor

(alternatively you could restrict coq-paco to 4.2.0, but updating's probably preferable in the long run)

@pennyannn
Copy link

Thanks for the pointers! I will try updating entree-specs.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@RyanGlScott @pennyannn @sauclovian-g