Skip to content

Add warning for non closed level 0 notations #21107

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
Open
wants to merge 4 commits into
base: master
Choose a base branch
from
Open

Add warning for non closed level 0 notations #21107

wants to merge 4 commits into from

Conversation

proux01
Copy link
Contributor

@proux01 proux01 commented Sep 23, 2025 •
edited
Loading

As suggested in #20953

  • Added / updated test-suite.
  • Added changelog.
  • Added / updated documentation.
    • Documented any new / changed user messages.
    • Updated documented syntax by running make doc_gram_rsts.
  • Opened overlay pull requests.

Overlay (to be merged in sync with the current PR)

@proux01 proux01 added this to the 9.2+rc1 milestone Sep 23, 2025
@proux01 proux01 requested review from a team as code owners September 23, 2025 09:26
@proux01 proux01 added kind: user messages Error messages, warnings, etc. part: notations The notation system. request: full CI Use this label when you want your next push to trigger a full CI. labels Sep 23, 2025
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 23, 2025
@SkySkimmer
Copy link
Contributor

Is this working properly? I don't see the warning for uint "phi" notations (cf rocq-prover/stdlib#209) in the stdlib log

@proux01 proux01 force-pushed the test-strict-right-assoc branch from c812b67 to c4cae01 Compare September 24, 2025 13:34
@proux01 proux01 requested review from a team as code owners September 24, 2025 13:34
@coqbot-app coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Sep 24, 2025
SkySkimmer
SkySkimmer reviewed Sep 24, 2025
View reviewed changes
Copy link
Contributor

@SkySkimmer SkySkimmer left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

probably worth a changelog for the corelib changes too

@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 24, 2025
@proux01 proux01 force-pushed the test-strict-right-assoc branch from c4cae01 to 39fea68 Compare September 24, 2025 13:43
@coqbot-app coqbot-app bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Sep 24, 2025
proux01 added a commit to proux01/stdlib that referenced this pull request Sep 24, 2025
@proux01
Adapt to rocq-prover/rocq#21107
006c5e2
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 25, 2025
@proux01 proux01 force-pushed the test-strict-right-assoc branch from 39fea68 to 66e394f Compare September 25, 2025 09:00
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 25, 2025
@github-actions github-actions bot added the needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. label Sep 25, 2025
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 25, 2025
@proux01 proux01 force-pushed the test-strict-right-assoc branch from 66e394f to 4ea66fa Compare September 25, 2025 09:15
@coqbot-app coqbot-app bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels Sep 25, 2025
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 25, 2025
@proux01 proux01 force-pushed the test-strict-right-assoc branch from 4ea66fa to 9f37440 Compare September 25, 2025 09:34
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 25, 2025
@proux01 proux01 added the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 25, 2025
@proux01 proux01 force-pushed the test-strict-right-assoc branch from 9f37440 to 25e2967 Compare September 25, 2025 10:59
@coqbot-app coqbot-app bot removed the request: full CI Use this label when you want your next push to trigger a full CI. label Sep 25, 2025
@proux01 proux01 mentioned this pull request Sep 25, 2025
Open
@proux01
Copy link
Contributor Author

proux01 commented Sep 25, 2025 •
edited
Loading

Is this working properly? I don't see the warning for uint "phi" notations (cf rocq-prover/stdlib#209) in the stdlib log

Good catch, it was working properly with Reserved Notation but apparently doing the reservation through the Notation command simply dropped all warnings, fixed.

BTW, yet another indication we should deprecate reserving notation through Notation rather than Reserved Notation, but definitely outside the scope of the current PR.

probably worth a changelog for the corelib changes too

I gave up on changing the level of the prim array notation and documented the other change (although it's a relatively internal notation, let's be careful)

CI is "green" (rewriter failure is an unmerged overlay: mit-plv/rewriter#178), I consider this ready.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@SkySkimmer SkySkimmer SkySkimmer left review comments

At least 1 approving review is required to merge this pull request.

Assignees
No one assigned
Labels
kind: user messages Error messages, warnings, etc. part: notations The notation system.
Projects
None yet
Milestone
9.2+rc1
Development

Successfully merging this pull request may close these issues.
2 participants
@proux01 @SkySkimmer