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

Ltac2 typed notations #18432

Merged
merged 6 commits into from Feb 9, 2024
Merged

Ltac2 typed notations #18432

merged 6 commits into from Feb 9, 2024

Conversation

SkySkimmer
Copy link
Contributor

@SkySkimmer SkySkimmer commented Dec 21, 2023 •
edited

Fix #17477

We preserve the ability to define untyped notations with a flag (DONE unset the flag in the compat files), however it is not clear that this is at all useful.

To handle globalize on a typed notation (called when declaring an untyped notation which uses the typed notation, and when using Ltac2 Globalize) we add a constructor to raw_tacexpr which contains a glb_tacexpr with its expected type information. The types will be checked when the untyped notation is typechecked (eg at use in a regular definition or in a typed notation).

Aliases are currently never eagerly typed (so eg Ltac2 Notation foo := Int.add (). is still accepted), this could probably be easily changed.

@SkySkimmer SkySkimmer added kind: feature New user-facing feature request or implementation. kind: documentation Additions or improvement to documentation. needs: changelog entry This should be documented in doc/changelog. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge. request: full CI Use this label when you want your next push to trigger a full CI. labels Dec 21, 2023
@SkySkimmer SkySkimmer added this to the 8.20+rc1 milestone Dec 21, 2023
@SkySkimmer SkySkimmer requested a review from a team as a code owner December 21, 2023 14:49
@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 Dec 21, 2023
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Dec 21, 2023
@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 Dec 21, 2023
@ppedrot ppedrot self-assigned this Dec 22, 2023
@SkySkimmer SkySkimmer added needs: documentation Documentation was not added or updated. and removed kind: documentation Additions or improvement to documentation. labels Dec 22, 2023
@SkySkimmer SkySkimmer added request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: documentation Documentation was not added or updated. needs: changelog entry This should be documented in doc/changelog. labels Jan 23, 2024
@SkySkimmer SkySkimmer requested a review from a team as a code owner January 23, 2024 12: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 Jan 23, 2024
@SkySkimmer
Copy link
Contributor Author

doc/changelog added

@SkySkimmer
Copy link
Contributor Author

@coqbot run full ci

@ppedrot
Copy link
Member

ppedrot commented Feb 7, 2024

TODO unset the flag in the compat files

@SkySkimmer do you plan to do it before merging?

@SkySkimmer SkySkimmer added the needs: progress Work in progress: awaiting action from the author. label Feb 7, 2024
@SkySkimmer SkySkimmer requested a review from a team as a code owner February 7, 2024 12:40
@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 Feb 7, 2024
@SkySkimmer SkySkimmer removed the needs: progress Work in progress: awaiting action from the author. label Feb 7, 2024
@SkySkimmer
Copy link
Contributor Author

TODO unset the flag in the compat files

done

@SkySkimmer SkySkimmer requested a review from a team as a code owner February 7, 2024 16:01
@ppedrot
Copy link
Member

ppedrot commented Feb 8, 2024

@coqbot run full ci

@coqbot-app coqbot-app bot removed 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 Feb 8, 2024
@ppedrot
Copy link
Member

ppedrot commented Feb 9, 2024

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 0c1a6d0 into coq:master Feb 9, 2024
4 of 7 checks passed
@SkySkimmer SkySkimmer deleted the ltac2-typed-notation branch February 9, 2024 16:07
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Mar 7, 2024
@coqbot-app @ppedrot @rlepigre
Merge PR coq#18432: Ltac2 typed notations
b7eb09c 
Reviewed-by: ppedrot
Ack-by: rlepigre
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Mar 7, 2024
@coqbot-app @ppedrot @rlepigre
Merge PR coq#18432: Ltac2 typed notations
e98d4a8 
Reviewed-by: ppedrot
Ack-by: rlepigre
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Mar 7, 2024
@coqbot-app @ppedrot @rlepigre
Merge PR coq#18432: Ltac2 typed notations
9609d35 
Reviewed-by: ppedrot
Ack-by: rlepigre
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Mar 7, 2024
@coqbot-app @ppedrot @rlepigre
Merge PR coq#18432: Ltac2 typed notations
85f5b75 
Reviewed-by: ppedrot
Ack-by: rlepigre
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Mar 12, 2024
@coqbot-app @ppedrot @rlepigre
Merge PR coq#18432: Ltac2 typed notations
ff9a18a 
Reviewed-by: ppedrot
Ack-by: rlepigre
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Mar 13, 2024
@coqbot-app @ppedrot @rlepigre
Merge PR coq#18432: Ltac2 typed notations
1d4a61f 
Reviewed-by: ppedrot
Ack-by: rlepigre
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Mar 13, 2024
@coqbot-app @ppedrot @rlepigre
Merge PR coq#18432: Ltac2 typed notations
8fc5b01 
Reviewed-by: ppedrot
Ack-by: rlepigre
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Mar 14, 2024
@coqbot-app @ppedrot @rlepigre
Merge PR coq#18432: Ltac2 typed notations
ac4d57c 
Reviewed-by: ppedrot
Ack-by: rlepigre
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Mar 15, 2024
@coqbot-app @ppedrot @rlepigre
Merge PR coq#18432: Ltac2 typed notations
4bb3d98 
Reviewed-by: ppedrot
Ack-by: rlepigre
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Mar 15, 2024
@coqbot-app @ppedrot @rlepigre
Merge PR coq#18432: Ltac2 typed notations
561fb97 
Reviewed-by: ppedrot
Ack-by: rlepigre
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
rlepigre pushed a commit to rlepigre/coq that referenced this pull request Mar 15, 2024
@coqbot-app @ppedrot @rlepigre
Merge PR coq#18432: Ltac2 typed notations
980ae70 
Reviewed-by: ppedrot
Ack-by: rlepigre
Co-authored-by: ppedrot <ppedrot@users.noreply.github.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@rlepigre rlepigre rlepigre left review comments

@ppedrot ppedrot ppedrot approved these changes

Assignees

@ppedrot ppedrot

Labels
kind: feature New user-facing feature request or implementation. part: ltac2 Issues and PRs related to the (in development) Ltac2 tactic langauge.
Projects
None yet
Milestone
8.20+rc1
Development

Successfully merging this pull request may close these issues.

Imprecise typing error location if discriminee of Ltac2 match!/lazy_match! is not a constr
3 participants
@SkySkimmer @ppedrot @rlepigre