Skip to content

feat: realizeConst for match equations#7247

Merged
Kha merged 2 commits intoleanprover:masterfrom
Kha:push-qwppsywztwvl
Mar 3, 2025
Merged

feat: realizeConst for match equations#7247
Kha merged 2 commits intoleanprover:masterfrom
Kha:push-qwppsywztwvl

Conversation

@Kha
Copy link
Copy Markdown
Member

@Kha Kha commented Feb 26, 2025

This PR makes generation of match equations and splitters compatible with parallelism.

@Kha Kha added the changelog-language Language features and metaprograms label Feb 26, 2025
@Kha Kha force-pushed the push-qwppsywztwvl branch from e9c0ae2 to 0f1ae17 Compare February 26, 2025 20:22
@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 Feb 26, 2025
@ghost
Copy link
Copy Markdown

ghost commented Feb 26, 2025 •
edited by ghost
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2e66341f69a0db9ef8b8e5255d0f0cfa73cdadc1 --onto c3402b85ab96b7ceec32e0b119837913da0051d0. (2025-02-26 20:43:24)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 2e66341f69a0db9ef8b8e5255d0f0cfa73cdadc1 --onto 727c696d9f132bc2701b9755f8819bd36335cd26. (2025-02-28 15:26:41)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ad5a746cdd6c29a47952fc38d6e256ad4071f57e --onto 727c696d9f132bc2701b9755f8819bd36335cd26. (2025-02-28 16:28:58)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a244b0688244a0b9036fc2f14e63c1368bbdd94c --onto e3c6909ad593e5a966a449df5e92abb1f0dbc317. (2025-03-03 16:27:23)

Kha
Kha commented Feb 27, 2025
View reviewed changes
src/Lean/Attributes.lean
Comment on lines +255 to +261
-- We assume (and check below) that, if used asynchronously, enum attributes are set only in the
-- same context in which the tagged declaration was created
asyncMode := .async
replay? := some fun _ newState consts st => consts.foldl (init := st) fun st c =>
match newState.find? c with
| some v => st.insert c v
| _ => st
Copy link
Copy Markdown
Member Author

@Kha Kha Feb 27, 2025

Choose a reason for hiding this comment

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

Needed for @[inline] being applied to the splitter def

tests/lean/run/matchEqsBug.lean Outdated
test% f.match_1
#check f.match_1.splitter

def g.match_1.splitter := 4
Copy link
Copy Markdown
Member Author

@Kha Kha Feb 27, 2025

Choose a reason for hiding this comment

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

The async code (must) assume that the same name isn't used by a private and a non-private declaration so this broke. I think that is an acceptable regression.

@Kha Kha mentioned this pull request Feb 27, 2025
Merged
@Kha Kha force-pushed the push-qwppsywztwvl branch 2 times, most recently from a27576d to 1a7b356 Compare February 28, 2025 15:57
@Kha Kha added the merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. label Mar 2, 2025
@Kha Kha force-pushed the push-qwppsywztwvl branch 2 times, most recently from 0e4db6d to 4c68db2 Compare March 3, 2025 10:08
@Kha Kha requested a review from leodemoura as a code owner March 3, 2025 10:08
@Kha Kha mentioned this pull request Mar 3, 2025
Merged
@Kha Kha force-pushed the push-qwppsywztwvl branch from 4c68db2 to e2e35f9 Compare March 3, 2025 12:15
github-merge-queue bot pushed a commit that referenced this pull request Mar 3, 2025
@Kha
fix: more realizeConst fixes (#7300)
0a55f4b 
Found and debugged while working on stage 2 of #7247
@Kha Kha force-pushed the push-qwppsywztwvl branch 2 times, most recently from a0bfb55 to e1d3692 Compare March 3, 2025 13:18
@Kha Kha force-pushed the push-qwppsywztwvl branch from e1d3692 to 09f3d1a Compare March 3, 2025 15:53
@Kha Kha removed the merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. label Mar 3, 2025
@Kha Kha enabled auto-merge March 3, 2025 16:35
@Kha Kha force-pushed the push-qwppsywztwvl branch from 4585021 to 09f3d1a Compare March 3, 2025 17:02
@Kha Kha added this pull request to the merge queue Mar 3, 2025
Merged via the queue into leanprover:master with commit dab6a16 Mar 3, 2025
28 checks passed
@Kha Kha mentioned this pull request Mar 4, 2025
Merged
github-merge-queue bot pushed a commit that referenced this pull request Mar 6, 2025
@Kha
feat: use realizeConst for all equation, unfold, induction, and par…
24db5b5 
…tial fixpoint theorems (#7261)

This PR ensures all equation, unfold, induction, and partial fixpoint
theorem generators in core are compatible with parallelism.

Stacked on #7247
github-merge-queue bot pushed a commit that referenced this pull request Apr 1, 2025
@Kha
fix: make new codegen async realization-compatible (#7316)
8b1caa3 
Follow-up to #7247
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

Assignees

No one assigned

Labels

changelog-language Language features 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.

1 participant

@Kha