Skip to content

perf: enable separate codegen#13103

Draft
Kha wants to merge 13 commits intoleanprover:masterfrom
Kha:push-upslpnuoopnm
Draft

perf: enable separate codegen#13103
Kha wants to merge 13 commits intoleanprover:masterfrom
Kha:push-upslpnuoopnm

Conversation

@Kha
Copy link
Member

@Kha Kha commented Mar 24, 2026

No description provided.

@Kha
Copy link
Member Author

Kha commented Mar 24, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Mar 24, 2026 •
edited
Loading

Benchmark results for aeb3292 against 6f98a76 are in. Significant changes detected! @Kha

  • 🟥 build exited with code 2
  • 🟥 other exited with code 2

No significant changes detected.

@Kha Kha force-pushed the push-upslpnuoopnm branch from aeb3292 to e764fe8 Compare March 24, 2026 13:24
@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 Mar 24, 2026
@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Mar 24, 2026

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-24 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-03-24 14:09:00)

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 24, 2026
Update lean-toolchain for testing leanprover/lean4#13103
ad7e37a
@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 Mar 24, 2026
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 24, 2026
Update lean-toolchain for testing leanprover/lean4#13103
d2bd50e
@mathlib-lean-pr-testing mathlib-lean-pr-testing bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Mar 24, 2026
@mathlib-lean-pr-testing
Copy link

mathlib-lean-pr-testing bot commented Mar 24, 2026

Mathlib CI status (docs):

@Kha Kha force-pushed the push-upslpnuoopnm branch from e764fe8 to a9e95bc Compare March 24, 2026 14:14
mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 24, 2026
Update lean-toolchain for leanprover/lean4#13103
072bf11
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 24, 2026
Update lean-toolchain for leanprover/lean4#13103
13bff91
@mathlib-lean-pr-testing
Copy link

mathlib-lean-pr-testing bot commented Mar 24, 2026

Mathlib CI status (docs):

@Kha
Copy link
Member Author

Kha commented Mar 24, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Mar 24, 2026 •
edited
Loading

Benchmark results for 2f226e3 against e6df474 are in. Significant changes detected! @Kha

  • 🟥 build exited with code 2
  • 🟥 other exited with code 2

No significant changes detected.

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 24, 2026
Update lean-toolchain for leanprover/lean4#13103
b9e0ec6
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 24, 2026
Update lean-toolchain for leanprover/lean4#13103
ae5acfb
@mathlib-lean-pr-testing
Copy link

mathlib-lean-pr-testing bot commented Mar 24, 2026

Mathlib CI status (docs):

@Kha
Copy link
Member Author

Kha commented Mar 24, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Mar 24, 2026 •
edited
Loading

Benchmark results for 1f3882e against e6df474 are in. Significant changes detected! @Kha

  • 🟥 build//instructions: +3.6T (+29.37%)
  • 🟥 other exited with code 2

Large changes (116✅, 11🟥)

Too many entries to display here. View the full report on radar instead.

Medium changes (382✅, 18🟥)

Too many entries to display here. View the full report on radar instead.

Small changes (1006✅, 288🟥)

Too many entries to display here. View the full report on radar instead.

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 24, 2026
Update lean-toolchain for leanprover/lean4#13103
f99d98a
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 24, 2026
Update lean-toolchain for leanprover/lean4#13103
c2e0337
@mathlib-lean-pr-testing
Copy link

mathlib-lean-pr-testing bot commented Mar 24, 2026

Mathlib CI status (docs):

@Kha
Copy link
Member Author

Kha commented Mar 25, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Mar 25, 2026 •
edited
Loading

Benchmark results for a408558 against e6df474 are in. Significant changes detected! @Kha

  • 🟥 build//instructions: +3.6T (+29.37%)
  • 🟥 other exited with code 2

Large changes (116✅, 11🟥)

Too many entries to display here. View the full report on radar instead.

Medium changes (382✅, 17🟥)

Too many entries to display here. View the full report on radar instead.

Small changes (1004✅, 290🟥)

Too many entries to display here. View the full report on radar instead.

@Kha
Copy link
Member Author

Kha commented Mar 25, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Mar 25, 2026 •
edited
Loading

Benchmark results for 4f0ce2d against e6df474 are in. Significant changes detected! @Kha

  • 🟥 build exited with code 2
  • 🟥 other exited with code 2

No significant changes detected.

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 25, 2026
Update lean-toolchain for leanprover/lean4#13103
8b24db2
mathlib-nightly-testing bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Mar 25, 2026
Update lean-toolchain for leanprover/lean4#13103
af9f106
@mathlib-lean-pr-testing
Copy link

mathlib-lean-pr-testing bot commented Mar 25, 2026

Mathlib CI status (docs):

@Kha Kha force-pushed the push-upslpnuoopnm branch from 4f0ce2d to eabd6f2 Compare March 25, 2026 10:52
@Kha
Copy link
Member Author

Kha commented Mar 25, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Mar 25, 2026 •
edited
Loading

Benchmark results for eabd6f2 against e6df474 are in. Significant changes detected! @Kha

  • 🟥 build exited with code 2
  • 🟥 other exited with code 2

No significant changes detected.

mathlib-nightly-testing bot pushed a commit to leanprover-community/batteries that referenced this pull request Mar 25, 2026
Update lean-toolchain for leanprover/lean4#13103
12bac2e
@Kha Kha force-pushed the push-upslpnuoopnm branch from eabd6f2 to 0ef668c Compare March 25, 2026 12:22
@Kha
Copy link
Member Author

Kha commented Mar 25, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Mar 25, 2026 •
edited
Loading

Benchmark results for 0ef668c against e6df474 are in. Significant changes detected! @Kha

  • 🟥 build//instructions: +3.4T (+28.03%)
  • 🟥 other exited with code 2

Large changes (116✅, 11🟥)

Too many entries to display here. View the full report on radar instead.

Medium changes (382✅, 18🟥)

Too many entries to display here. View the full report on radar instead.

Small changes (1021✅, 284🟥)

Too many entries to display here. View the full report on radar instead.

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 leodemoura will be requested when the pull request is marked ready for review leodemoura is a code owner

@hargoniX hargoniX Awaiting requested review from hargoniX hargoniX will be requested when the pull request is marked ready for review hargoniX 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 mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN 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.

3 participants

@Kha @leanprover-radar @leanprover-bot