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

Compilation of ssete9 failed (on coq dev) #13

Closed
Casteran opened this issue Aug 9, 2022 · 0 comments · Fixed by #14
Closed

Compilation of ssete9 failed (on coq dev) #13

Casteran opened this issue Aug 9, 2022 · 0 comments · Fixed by #14

Comments

@Casteran
Copy link
Member

Casteran commented Aug 9, 2022

The compilation of hydra-battles fails (on Zulip CI, coq dev) when trying to build gaia (Schutte), apparently because of a lexical error.

# File "./theories/schutte/ssete9.v", line 2207, characters 15-20:
  # Error: The reference Pzero was not found in the current environment.

I looked at ssete9.v code on coq-community. Line 2207 is the only place where =P and zero are sticked together, leading to consider Pzero as an undeclared identifier.

It could be related to a recent change in lexical analysis rules coq/coq#16322
Perhaps it would be enough to add a apace between =P and zero.

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 a pull request may close this issue.

1 participant