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

Adapt w.r.t. coq/coq#16004. #606

Merged
merged 2 commits into from
Jul 19, 2022

Conversation

ppedrot
Copy link
Contributor

@ppedrot ppedrot commented Jul 18, 2022

We probably also need to bump the submodule commits, but I'll do that in another PR.

@ppedrot ppedrot force-pushed the hint-locality-error branch from eeb934a to def10e4 Compare July 18, 2022 19:29
@QinshiWang
Copy link
Contributor

What is

(** Ignore Hint Rewrite global attribute for Coq 8.13 *)
Set Warnings "-unsupported-attributes".

Should I add or remove some attributes?

@ppedrot
Copy link
Contributor Author

ppedrot commented Jul 19, 2022

@QinshiWang VST seems to support Coq 8.13 as per the opam file, I had to keep backwards compatibility with this version. Since the Hint Rewrite locality attributes were only introduced in 8.14, unsetting the warning allows ignoring the error that Coq 8.13 raises when given global flags for Hint Rewrite commands. Once support for Coq 8.13 is dropped you can remove the Set Warning line.

@QinshiWang
Copy link
Contributor

@ppedrot Thanks. I believe VST has dropped support for Coq 8.13 according to the Makefile. The OPAM files in this repo are not frequent maintained (see #597). But on the other hand, the Zlist library is separately installable. It is worth supporting more Coq versions than the main body of VST.

@andrew-appel andrew-appel merged commit 0e364d0 into PrincetonUniversity:master Jul 19, 2022
@ppedrot ppedrot deleted the hint-locality-error branch July 19, 2022 18:15
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

Successfully merging this pull request may close these issues.

3 participants