fix: make sure app elaborator eta feature does not result in capturable variables#10377
Merged
kmill merged 4 commits intoleanprover:masterfrom Sep 14, 2025
Merged
fix: make sure app elaborator eta feature does not result in capturable variables#10377kmill merged 4 commits intoleanprover:masterfrom
kmill merged 4 commits intoleanprover:masterfrom
Conversation
…le variables This PR fixes an issue where the "eta feature" in the app elaborator, which is invoked when positional arguments are skipped due to named arguments, result in variables that can be captured by those named arguments. Now the temporary local variables that implement this feature get fresh names. The names used for the closed lambda expression still use the original parameter names. Closes leanprover#6373
Collaborator
|
Reference manual CI status:
|
ghost
pushed a commit
to leanprover-community/batteries
that referenced
this pull request
Sep 14, 2025
ghost
pushed a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Sep 14, 2025
|
Mathlib CI status (docs):
|
kim-em
added a commit
to leanprover-community/mathlib4-nightly-testing
that referenced
this pull request
Sep 15, 2025
* fix deprecations * remove upstreamed defs * two fixes * fix merge * fix merge * revert sqrt changes * ugh * fix from nightly-testing * fix merge * remove test deleted on master * fix test * note about test * . * Update lean-toolchain for leanprover/lean4#10194 * chore: bump to nightly-2025-09-02 * adjust to upstream changes * fix * fix * long line * Use Mathlib's nightly toolchain to run docgen in the nightly test * simpNF linter * whitespace * Update lean-toolchain for testing leanprover/lean4#10217 * Correct the working directory: should be 'docbuild' * Rework the grind regression report as a nightly-testing regression report It should still report the same things, but now as one message for all regression kinds * feat(Cache): download speeds & more info on errors * fix(Cache): add base download failure message * fixes * turn off linter * adaptation note * turn off linter.nightlyRegressionSet * chore: adaptations for nightly-2025-09-02 * Update lean-toolchain for testing leanprover/lean4#10059 * Update lean-toolchain for leanprover/lean4#10217 * chore: bump to nightly-2025-09-03 * Remove the erroring nightly regression report, we'll develop this on another branch. * fixes * update LibraryRewrite test * Update lean-toolchain for leanprover/lean4#10059 * chore: bump to nightly-2025-09-04 * fix * chore: bump to nightly-2025-09-05 * chore: adaptations for nightly-2025-09-05 * chore: bump to nightly-2025-09-06 * Update lean-toolchain for testing leanprover/lean4#10271 * Adapt to leanprover/lean4#10271 * Bump batteries * Update lean-toolchain for leanprover/lean4#10271 * chore: bump to nightly-2025-09-07 * nolint unusedArguments * Merge master into nightly-testing * chore: bump to nightly-2025-09-08 * fixes * chore: bump to nightly-2025-09-09 * fix thing * Update lean-toolchain for testing leanprover/lean4#10306 * temporarily remove test * adaptation note * master version of Cache/Requests.lean * chore: bump to nightly-2025-09-10 * adaptation note * chore: adaptations for nightly-2025-09-10 * merge lean-pr-testing-10059 * bump toolchain manually?? * restore test * chore: bump to nightly-2025-09-11 * lake update * fix * adaptations for leanprover/lean4#10307 * remove validateDocComment in ToAdditive * remove upstreamed Function.Injective * update assert_not_exists * oops * comment out DeriveTraversable * chore: replace some grind attibutes with grind_pattern, to be robust for future heuristic changes * suggestions from Rob23oba * lshake --fix * fix bad shake * shake --update * . * chore: adaptations for nightly-2025-09-11 * chore: bump to nightly-2025-09-12 * Revert "oops" This reverts commit 517b832. * Revert "comment out DeriveTraversable" This reverts commit 0460eb8. * fix DeriveTraversable * add `binders` fields * fix * fixes * update manifest * fixes * fixes * fixes * chore: bump to nightly-2025-09-13 * fixes * fixes * fixes * fixes * fixes * fixes * fixes * remove adaptation note * Update lean-toolchain for testing leanprover/lean4#10373 * fixes * chore: bump to nightly-2025-09-14 * Update lean-toolchain for testing leanprover/lean4#10377 * fix * fix * fix * fix emrge * update batteries * chore: adaptations for nightly-2025-09-14 * Merge master into nightly-testing * Update Mathlib/Data/List/Basic.lean * Merge master into nightly-testing * chore: adaptations for nightly-2025-09-14 * chore: bump to nightly-2025-09-15 --------- Co-authored-by: Rob23oba <robin.arnez@web.de> Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com> Co-authored-by: Kim Morrison <kim@tqft.net> Co-authored-by: github-actions <github-actions@github.com> Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com> Co-authored-by: Mac Malone <mac@lean-fro.org> Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com> Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com> Co-authored-by: Joachim Breitner <mail@joachim-breitner.de> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR fixes an issue where the "eta feature" in the app elaborator, which is invoked when positional arguments are skipped due to named arguments, results in variables that can be captured by those named arguments. Now the temporary local variables that implement this feature get fresh names. The names used for the closed lambda expression still use the original parameter names.
Closes #6373