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 preterm antiquotation $preterm:x #17359

Merged
merged 1 commit into from Jun 8, 2023
Merged

Ltac2 preterm antiquotation $preterm:x #17359

merged 1 commit into from Jun 8, 2023

Conversation

SkySkimmer
Copy link
Contributor

@SkySkimmer SkySkimmer commented Mar 8, 2023 •
edited

@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 Mar 8, 2023
@ppedrot
Copy link
Member

ppedrot commented Mar 9, 2023

I don't like the proliferation of built-in syntax for terms in Ltac2. We should be able to derive it from ltac2 quotations + proper functions to pretype a term. IIUC that's already possible today after #16740?

@SkySkimmer
Copy link
Contributor Author

SkySkimmer commented Mar 9, 2023 •
edited

ltac2:() has a significant cost because it needs to turn the env and expected type into a fresh evar
and if there's no expected type that's one more evar

@ppedrot
Copy link
Member

ppedrot commented Mar 9, 2023

But then it calls for a more principled approach where we have to provide this kind of expressive antiquotation that prevents the pretyper to redo the work. Just that it's general and needs not be either a constr or a uconstr.

@SkySkimmer SkySkimmer added needs: changelog entry This should be documented in doc/changelog. request: full CI Use this label when you want your next push to trigger a full CI. and removed needs: changelog entry This should be documented in doc/changelog. labels Mar 10, 2023
@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 Mar 15, 2023
@SkySkimmer SkySkimmer marked this pull request as ready for review March 15, 2023 15:01
@SkySkimmer SkySkimmer requested review from a team as code owners March 15, 2023 15:01
@SkySkimmer SkySkimmer added this to the 8.18+rc1 milestone Mar 15, 2023
@SkySkimmer SkySkimmer added the kind: enhancement Enhancement to an existing user-facing feature, tactic, etc. label Mar 15, 2023
@ppedrot ppedrot self-assigned this Apr 3, 2023
@SkySkimmer SkySkimmer changed the title Ltac2 preterm antiquotation Ltac2 preterm antiquotation $$x May 10, 2023
@SkySkimmer SkySkimmer mentioned this pull request May 17, 2023
Open
@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 Jun 1, 2023
@coqbot-app coqbot-app bot added needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. and removed needs: rebase Should be rebased on the latest master to solve conflicts or have a newer CI run. labels Jun 2, 2023
@SkySkimmer SkySkimmer changed the title Ltac2 preterm antiquotation $$x Ltac2 preterm antiquotation $preterm:x Jun 5, 2023
@SkySkimmer
Copy link
Contributor Author

@ppedrot

I changed the syntax to $preterm:x and added $constr:x alias of $x

ppedrot
ppedrot reviewed Jun 6, 2023
View reviewed changes
plugins/ltac2/g_ltac2.mlg
let test_dollar_ident_colon_ident =
let open Pcoq.Lookahead in
to_entry "test_dollar_ident_colon_ident" begin
lk_kw "$" >> lk_ident >> lk_kw ":" >> lk_ident >> check_no_space
Copy link
Member

Choose a reason for hiding this comment

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

TODO: check this is the correct no-space lookahead.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

Looks fine, I added some tests

@SkySkimmer
Copy link
Contributor Author

@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 Jun 7, 2023
SkySkimmer added a commit to SkySkimmer/coq-serapi that referenced this pull request Jun 8, 2023
@SkySkimmer
Adapt to coq/coq#17359 (ltac2_var_quotation)
a5701a0
@SkySkimmer SkySkimmer added the request: full CI Use this label when you want your next push to trigger a full CI. label Jun 8, 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 Jun 8, 2023
@ppedrot
Copy link
Member

ppedrot commented Jun 8, 2023

@coqbot merge now

@coqbot-app coqbot-app bot merged commit 362de29 into coq:master Jun 8, 2023
6 checks passed
@coqbot-app
Copy link
Contributor

coqbot-app bot commented Jun 8, 2023

@ppedrot: Please take care of the following overlays:

  • 17359-SkySkimmer-tac2-preterm-antiquot.sh

ppedrot added a commit to ejgallego/coq-serapi that referenced this pull request Jun 8, 2023
@ppedrot
Merge pull request #337 from SkySkimmer/tac2-preterm-antiquot
e29eadc 
Adapt to coq/coq#17359 (ltac2_var_quotation)
@SkySkimmer SkySkimmer deleted the tac2-preterm-antiquot branch June 8, 2023 14:25
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jfehrle jfehrle jfehrle left review comments

@ppedrot ppedrot ppedrot approved these changes

Assignees

@ppedrot ppedrot

Labels
kind: enhancement Enhancement to an existing user-facing feature, tactic, etc.
Projects
None yet
Milestone
8.18+rc1
Development

Successfully merging this pull request may close these issues.

uconstr: for Ltac2?
3 participants
@SkySkimmer @ppedrot @jfehrle