Skip to content

feat: exprDependsOn follows delayed assignments - #2484

Open
kim-em wants to merge 2 commits into
leanprover:masterfrom
kim-em:exprDependsOn
Open

feat: exprDependsOn follows delayed assignments#2484
kim-em wants to merge 2 commits into
leanprover:masterfrom
kim-em:exprDependsOn

Conversation

@kim-em

@kim-em kim-em commented Aug 30, 2023 •
edited
Loading

Copy link
Copy Markdown
Collaborator

This PR fixes Lean.dependsOn.visitMain to follow delayed metavariable assignments when checking expression dependencies. Previously, when a metavariable had a delayed assignment, exprDependsOn' would only inspect the local context of the original metavariable declaration, missing the dependency through the pending metavariable. Now it recursively visits the pending metavariable from the delayed assignment before falling back to the local context check.

Fixes #2483

@kim-em
kim-em force-pushed the exprDependsOn branch 4 times, most recently from 0a5e1c3 to a97449d Compare September 1, 2023 00:42
@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 Sep 1, 2023
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Sep 1, 2023
leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#2484
81a04d1
@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Sep 1, 2023
@ghost

ghost commented Sep 1, 2023 •
edited by ghost
Loading

Copy link
Copy Markdown

@kim-em
kim-em force-pushed the exprDependsOn branch 2 times, most recently from 5228e51 to bcc0c41 Compare September 1, 2023 06:49
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Sep 1, 2023
leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#2484
40371a1
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Sep 1, 2023
leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#2484
b792571
@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 Sep 1, 2023
@ghost

ghost commented Sep 1, 2023 •
edited by ghost
Loading

Copy link
Copy Markdown

@kim-em kim-em added the awaiting-review Waiting for someone to review the PR label Sep 4, 2023
@kim-em
kim-em marked this pull request as ready for review September 4, 2023 00:21
@Kha
Kha requested review from Kha and leodemoura as code owners November 20, 2023 08:15
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Dec 12, 2023
leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#2484
37726f0
@leanprover-bot leanprover-bot added the P-low We are not planning to work on this issue label Jan 28, 2025
@leanprover-bot

leanprover-bot commented Feb 12, 2026

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-02-10 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-02-12 06:39:03)

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request Feb 12, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#2484
01c8e95
@github-actions github-actions Bot added the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Feb 12, 2026
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Feb 12, 2026
leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#2484
8927a7f
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Feb 12, 2026

Copy link
Copy Markdown

Mathlib CI status (docs):

@kim-em kim-em added the changelog-language Language features and metaprograms label Jun 10, 2026
Kim Morrison @claude
chore: retrigger CI
0e28e55 
The only red on this PR is a `check-pr-body` run from February that GitHub will
no longer let us re-run; the same workflow has since passed on this SHA.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WGQ4cXuC9bBbZQ3psYLZUA
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@leodemoura leodemoura Awaiting requested review from leodemoura
@Kha Kha Awaiting requested review from Kha

Assignees

@leodemoura leodemoura

Labels

awaiting-review Waiting for someone to review the PR builds-mathlib CI has verified that Mathlib builds against this PR changelog-language Language features and metaprograms low priority mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN P-low We are not planning to work on this issue 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.

Lean.exprDependsOn' does not take into account delayed assignments.

4 participants

@kim-em @leanprover-bot @Kha @leodemoura