Skip to content

fix: allow generalization in let#3060

Merged
Kha merged 5 commits intoleanprover:masterfrom
eric-wieser:let-generalization
Jan 23, 2024
Merged

fix: allow generalization in let#3060
Kha merged 5 commits intoleanprover:masterfrom
eric-wieser:let-generalization

Conversation

@eric-wieser
Copy link
Copy Markdown
Contributor

@eric-wieser eric-wieser commented Dec 13, 2023 •
edited
Loading

As suggested by @kmill, removing an unnecessary let (possibly only there in the first place for copy/paste reasons) seems to fix the included test.

This makes ~q() matching in quote4 noticeably more useful in things like norm_num (as it fixes leanprover-community/quote4#29)

It also makes a quote4 bug slightly more visible (leanprover-community/quote4#30), but the bug there already existed anyway, and isn't caused by this patch.

Fixes #3065

@eric-wieser eric-wieser marked this pull request as ready for review December 13, 2023 15:43
@eric-wieser
Copy link
Copy Markdown
Contributor Author

eric-wieser commented Dec 13, 2023

awaiting-review

@github-actions github-actions bot added the awaiting-review Waiting for someone to review the PR label Dec 13, 2023
@eric-wieser eric-wieser mentioned this pull request Dec 14, 2023
Closed
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Dec 15, 2023
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Dec 15, 2023
Update lean-toolchain for testing leanprover/lean4#3060
2e83636
@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Dec 15, 2023
@ghost
Copy link
Copy Markdown

ghost commented Dec 15, 2023 •
edited by ghost
Loading

ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Dec 15, 2023
Trigger CI for leanprover/lean4#3060
3865811
@eric-wieser eric-wieser mentioned this pull request Dec 15, 2023
Open
@ghost ghost added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Dec 15, 2023
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Dec 16, 2023
Trigger CI for leanprover/lean4#3060
8e2151c
@eric-wieser
Copy link
Copy Markdown
Contributor Author

eric-wieser commented Dec 21, 2023

@semorrison, is there any hope of this landing in the 4.5.0 release?

@kim-em
Copy link
Copy Markdown
Collaborator

kim-em commented Dec 21, 2023

@semorrison, is there any hope of this landing in the 4.5.0 release?

I'm sorry, this didn't make it.

@eric-wieser
Copy link
Copy Markdown
Contributor Author

eric-wieser commented Dec 21, 2023

And just to check I understand the rc process, the fact this missed 4.5.0rc1 means it certainly will miss any future rcs?

ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jan 4, 2024
Trigger CI for leanprover/lean4#3060
dacc372
@eric-wieser eric-wieser mentioned this pull request Jan 4, 2024
Closed
1 task
@kim-em
Copy link
Copy Markdown
Collaborator

kim-em commented Jan 5, 2024

And just to check I understand the rc process, the fact this missed 4.5.0rc1 means it certainly will miss any future rcs?

Well, hopefully it can make v4.6.0-rc1!

The status of rc2 is still a bit up in the air. If there is really substantial demand (like 10 maintainers have +1'd a post saying that Mathlib wants something asap), I think we're open to cutting a rc2 solely for the sake a new features. But the preference is that we only make rc2 when there is a bad problem that needs fixing.

@eric-wieser
Copy link
Copy Markdown
Contributor Author

eric-wieser commented Jan 5, 2024

If rc2 happens it would be great if this could land in it, but certainly this PR isn't important enough to justify rc2 existing!

@eric-wieser eric-wieser mentioned this pull request Jan 8, 2024
Closed
@kim-em
Copy link
Copy Markdown
Collaborator

kim-em commented Jan 10, 2024

@Kha, I know @eric-wieser is keen to get this in, as it will enable new uses of Qq in writing tactic (positivity) extensions in Mathlib. As it touches do notation I think it needs review from you.

@Kha
Copy link
Copy Markdown
Member

Kha commented Jan 10, 2024

It looks like a strict improvement to me but I'll give @leodemoura a chance to look at it as well since he wrote the code. In general we haven't gone back to the do code in a long time so it's not a good time for any larger changes (which this one isn't).

@eric-wieser
Copy link
Copy Markdown
Contributor Author

eric-wieser commented Jan 22, 2024

@Kha, if Leo doesn't have the time, are you comfortable merging this without his approval?

@Kha
Copy link
Copy Markdown
Member

Kha commented Jan 23, 2024

Ok, I still don't see any possible downsides

@Kha Kha added this pull request to the merge queue Jan 23, 2024
Merged via the queue into leanprover:master with commit ec39de8 Jan 23, 2024
@eric-wieser eric-wieser mentioned this pull request Jan 23, 2024
Closed
@nomeata nomeata mentioned this pull request Jan 25, 2024
Closed
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jan 25, 2024
@eric-wieser
fix: adaptations for nightly-2024-01-24 (leanprover/lean4#3060) (#9943)
a8d7ec5 
leanprover/lean4#3060 exposed the latent leanprover-community/quote4#30 (by propagating it from `if let` and `match` to `let`). The workaround is thankfully trivial.
@eric-wieser eric-wieser mentioned this pull request Feb 2, 2024
Closed
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request Feb 3, 2024
@eric-wieser
chore: cleanup TODOs around leanprover/lean4#3060 (#10198)
bbb2893 
Mathlib is now using v4.6.0-rc1, which includes the fix in leanprover/lean4#3060
atarnoam pushed a commit to leanprover-community/mathlib4 that referenced this pull request Feb 9, 2024
@eric-wieser @atarnoam
chore: cleanup TODOs around leanprover/lean4#3060 (#10198)
dfbd298 
Mathlib is now using v4.6.0-rc1, which includes the fix in leanprover/lean4#3060
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em kim-em approved these changes

@digama0 digama0 digama0 approved these changes

@leodemoura leodemoura Awaiting requested review from leodemoura

@Kha Kha Awaiting requested review from Kha

Assignees

No one assigned

Labels

awaiting-review Waiting for someone to review the PR builds-mathlib CI has verified that Mathlib builds against this PR toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

let/ else pattern matching does not substitute in expected type generalizing does not work in match

4 participants

@eric-wieser @kim-em @Kha @digama0