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

Issue a warning when a notation declares different levels for the same term #17985

Closed
RalfJung opened this issue Aug 29, 2023 · 1 comment · Fixed by #17988
Closed

Issue a warning when a notation declares different levels for the same term #17985

RalfJung opened this issue Aug 29, 2023 · 1 comment · Fixed by #17988
Milestone
8.19+rc1

Comments

@RalfJung
Copy link
Contributor

Description of the problem

I accidentally wrote something like that:

Reserved Notation "'<<<' A '>>>' e '<<<' B '>>>'" (A, B at level 200, e, B at level 55).

(The actual notation was a lot bigger.)
It took me a while to realize that I have B at two different levels; Coq seems to then prefer the first level given. Ideally it should warn (or error) though and tell the user that they are declaring different levels for the same term.

Coq Version

8.17.0
herbelin added a commit to herbelin/github-coq that referenced this issue Aug 29, 2023
@herbelin
Fixes coq#17985: Error on level of notation variable set more than once.
4a798af 
In practice, it is enough to simplify the code for setting levels
thanks to the pre-parsing of the main entry in 359cac9.

Also, we reset the syntax modifiers in the natural order after having
parsed the non-syntax modifiers.
herbelin added a commit to herbelin/github-coq that referenced this issue Aug 29, 2023
@herbelin
Fixes coq#17985: Error on level of notation variable set more than once.
d9683e1 
In practice, it is enough to simplify the code for setting levels
thanks to the pre-parsing of the main entry in 359cac9.

Also, we reset the syntax modifiers in the natural order after having
parsed the non-syntax modifiers.
@herbelin herbelin mentioned this issue Aug 29, 2023
Merged
2 tasks
@herbelin
Copy link
Member

Good point. I tried to raise an error in PR #17988. If it fails too often, we can still make a warning.

herbelin added a commit to herbelin/github-coq that referenced this issue Aug 29, 2023
@herbelin
Fixes coq#17985: Error on level of notation variable set more than once.
537ca34 
In practice, it is enough to simplify the code for setting levels
thanks to the pre-parsing of the main entry in 359cac9.

Also, we reset the syntax modifiers in the natural order after having
parsed the non-syntax modifiers.
@coqbot-app coqbot-app bot added this to the 8.19+rc1 milestone Aug 30, 2023
coqbot-app bot added a commit that referenced this issue Aug 30, 2023
@coqbot-app @ppedrot
Merge PR #17988: Addresses #17985: error on duplicate notation variab…
e0d96f9 
…le levels

Reviewed-by: ppedrot
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
Villetaneuse pushed a commit to Villetaneuse/coq that referenced this issue Sep 9, 2023
@herbelin @Villetaneuse
Fixes coq#17985: Error on level of notation variable set more than once.
57371e2 
In practice, it is enough to simplify the code for setting levels
thanks to the pre-parsing of the main entry in 359cac9.

Also, we reset the syntax modifiers in the natural order after having
parsed the non-syntax modifiers.
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
8.19+rc1
Development

Successfully merging a pull request may close this issue.

Addresses #17985: error on duplicate notation variable levels herbelin/github-coq
2 participants
@RalfJung @herbelin