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

fix: allow dot idents to resolve to local names #6602

Merged
merged 2 commits into from
Jan 12, 2025
Merged

fix: allow dot idents to resolve to local names #6602

merged 2 commits into from
Jan 12, 2025

Conversation

cppio
Copy link
Contributor

@cppio cppio commented Jan 10, 2025 •
edited
Loading

This PR allows the dot ident notation to resolve to the current definition, or to any of the other definitions in the same mutual block. Existing code that uses dot ident notation may need to have nonrec added if the ident has the same name as the definition.

Closes #6601

@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 Jan 10, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 10, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6602
f3c70f2
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 10, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#6602
49a0896
@cppio cppio closed this Jan 10, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jan 10, 2025 •
edited
Loading

Mathlib CI status (docs):

@leanprover-community-bot leanprover-community-bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Jan 10, 2025
nomeata
nomeata previously approved these changes Jan 10, 2025
View reviewed changes
Copy link
Collaborator

@nomeata nomeata left a comment •
edited
Loading

Choose a reason for hiding this comment

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

(nevermind, looks like there is more work to be done)

@nomeata nomeata self-requested a review January 10, 2025 21:08
@cppio
Copy link
Contributor Author

cppio commented Jan 10, 2025

This causes breakage in Batteries and Mathlib due to code such as https://github.com/leanprover-community/batteries/blob/66225aab4f6bd1687053b03916105f7cab140507/Batteries/Data/UnionFind/Lemmas.lean#L100-L101 which rely on the dot ident not resolving to the current definition. This can easily be fixed by using nonrec, which the linked code already does for rfl.

@cppio cppio reopened this Jan 10, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 10, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6602
0b8bfa6
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 10, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6602
f45d805
@nomeata
Copy link
Collaborator

nomeata commented Jan 10, 2025

Thanks for the investigation. Can you add this analysis to #6601, ideally with a self-contained example of the idiom that this fix would be breaking (so that we can use it for the test suite)? Under which circumstaces can .foo refer to both an existing constant and the current definitions?

Also, if possible, contrast the behavior with the a.foo notation for A.foo (a : A); ideally .foo and a.foo resolution behave the same with regard to recursive definitions.

@nomeata nomeata dismissed their stale review January 10, 2025 22:03

(invalidated by breakage)

@nomeata nomeata removed their request for review January 10, 2025 22:04
@cppio cppio mentioned this pull request Jan 11, 2025
Closed
3 tasks
cppio added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 11, 2025
@cppio
fix breakage caused by leanprover/lean4#6602
ea80df0
@nomeata nomeata added the awaiting-mathlib We should not merge this until we have a successful Mathlib build label Jan 11, 2025
@cppio
Copy link
Contributor Author

cppio commented Jan 11, 2025

changelog-language

@github-actions github-actions bot added the changelog-language Language features, tactics, and metaprograms label Jan 11, 2025
@cppio cppio marked this pull request as ready for review January 11, 2025 12:39
cppio added a commit to cppio/batteries that referenced this pull request Jan 11, 2025
@cppio
fix build for leanprover/lean4#6602
4eb7304
@nomeata
Copy link
Collaborator

nomeata commented Jan 11, 2025

Please ping me here once mathlib is green (this likely requires pinning the mathlib adaption branch to the fixed batteries branch that you created, but should be possible)

@kim-em
Copy link
Collaborator

kim-em commented Jan 12, 2025

If you are fixing Mathlib, would you please avoid introducing more nonrec in any situation where it is possible instead to disambiguate a name?

cppio added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 12, 2025
@cppio
avoid nonrec for leanprover/lean4#6602
89f6ddc
@leanprover-community-bot leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed awaiting-mathlib We should not merge this until we have a successful Mathlib build breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Jan 12, 2025
@cppio
Copy link
Contributor Author

cppio commented Jan 12, 2025

@nomeata I made lake-manifest.json point to the commit in my fork of batteries, so mathlib builds now.

cppio added a commit to cppio/batteries that referenced this pull request Jan 12, 2025
@cppio
chore: adaptation for leanprover/lean4#6602
bf631d4
github-merge-queue bot pushed a commit to leanprover-community/batteries that referenced this pull request Jan 12, 2025
@cppio
chore: adaptation for leanprover/lean4#6602 (#1092)
8690c0b
@nomeata nomeata added this pull request to the merge queue Jan 12, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Jan 12, 2025
@cppio cppio requested review from TwoFX and mhuisi as code owners January 12, 2025 16:24
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jan 12, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6602
c3ad461
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 12, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#6602
3b982b7
@nomeata nomeata added this pull request to the merge queue Jan 12, 2025
@leanprover-community-bot leanprover-community-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels Jan 12, 2025
Merged via the queue into leanprover:master with commit 0da3624 Jan 12, 2025
19 checks passed
@cppio cppio deleted the dot-ident-mutual branch January 12, 2025 18:13
jcommelin added a commit to leanprover-community/mathlib4 that referenced this pull request Jan 17, 2025
@kim-em @leanprover-community-mathlib4-bot
@jcommelin @digama0 @alreadydone @Ruben-VandeVelde @trivial1711 @joelriou @chrisflav @artie2000 @eric-wieser @kmill @cppio
chore: adaptations for nightly-2025-01-16 (#20804)
d8ed55c 
* chore: bump to nightly-2024-12-23

* chore: adaptations for nightly-2024-12-23 (#20196)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Mario Carneiro <[email protected]>
Co-authored-by: Junyan Xu <[email protected]>
Co-authored-by: Ruben Van de Velde <[email protected]>
Co-authored-by: Mitchell Lee <[email protected]>
Co-authored-by: Joël Riou <[email protected]>
Co-authored-by: Christian Merten <[email protected]>
Co-authored-by: Artie Khovanov <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>

* fix

* chore: bump to nightly-2024-12-24

* Merge master into nightly-testing

* chore: bump to nightly-2024-12-25

* Merge master into nightly-testing

* chore: bump to nightly-2024-12-26

* chore: bump to nightly-2024-12-27

* Merge master into nightly-testing

* chore: bump to nightly-2024-12-28

* Merge master into nightly-testing

* fix

* fix

* fix

* chore: bump to nightly-2024-12-29

* Merge master into nightly-testing

* deprecations

* revert

* revert

* revert

* Update lean-toolchain for testing leanprover/lean4#6473

* remove DeriveToExpr

* Trigger CI for leanprover/lean4#6473

* fix

* chore: bump to nightly-2024-12-30

* Merge master into nightly-testing

* Trigger CI for leanprover/lean4#6473

* chore: bump to nightly-2024-12-31

* Merge master into nightly-testing

* chore: bump to nightly-2025-01-01

* Merge master into nightly-testing

* chore: bump to nightly-2025-01-02

* fix

* partial fix

* fix hopefully

* chore: adaptations for nightly-2025-01-02

* chore: bump to nightly-2025-01-03

* chore: adaptations for nightly-2025-01-03

* chore: bump to nightly-2025-01-04

* fixes

* shake --update

* chore: bump to nightly-2025-01-05

* Merge master into nightly-testing

* chore: bump to nightly-2025-01-06

* bump batteries

* chore: bump to nightly-2025-01-07

* chore: bump to nightly-2025-01-08

* chore: bump to nightly-2025-01-09

* bump batteries

* bump deps

* fix

* chore: adaptations for nightly-2025-01-09

* chore: bump to nightly-2025-01-10

* remove upstreamed

* Update lean-toolchain for testing leanprover/lean4#6602

* Trigger CI for leanprover/lean4#6602

* fix breakage caused by leanprover/lean4#6602

* chore: adaptations for nightly-2025-01-10

* fix merge

* avoid nonrec for leanprover/lean4#6602

* Trigger CI for leanprover/lean4#6602

* chore: bump to nightly-2025-01-14

* bump

* fixes

* fixes

* fixes

* chore: bump to nightly-2025-01-15

* fix

* empty commit to bump CI

* Update lean-toolchain for testing leanprover/lean4#6660

* fixes for leanprover/lean4#6660

* chore: bump to nightly-2025-01-16

* fix

* move batteries back to nightly-testing

* move batteries back to nightly-testing

---------

Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Johan Commelin <[email protected]>
Co-authored-by: Mario Carneiro <[email protected]>
Co-authored-by: Junyan Xu <[email protected]>
Co-authored-by: Ruben Van de Velde <[email protected]>
Co-authored-by: Mitchell Lee <[email protected]>
Co-authored-by: Joël Riou <[email protected]>
Co-authored-by: Christian Merten <[email protected]>
Co-authored-by: Artie Khovanov <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Kyle Miller <[email protected]>
Co-authored-by: Parth Shastri <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@nomeata nomeata nomeata left review comments

@TwoFX TwoFX Awaiting requested review from TwoFX TwoFX is a code owner

@mhuisi mhuisi Awaiting requested review from mhuisi mhuisi is a code owner

Assignees
No one assigned
Labels
breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-language Language features, tactics, and metaprograms 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.

dot ident notation cannot refer to recursive call
4 participants
@cppio @leanprover-community-bot @nomeata @kim-em