Skip to content

perf: enable separate codegen#13103

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

perf: enable separate codegen#13103
Kha wants to merge 14 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-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.

@Kha Kha force-pushed the push-upslpnuoopnm branch from 0ef668c to 96a3d98 Compare March 25, 2026 12:47
@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 96a3d98 against e6df474 are in. Significant changes detected! @Kha

  • 🟥 build//instructions: +3.6T (+29.36%)
  • 🟥 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 (1016✅, 284🟥)

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 25, 2026
Update lean-toolchain for leanprover/lean4#13103
12afad3
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
d77cfa5
@mathlib-lean-pr-testing
Copy link

mathlib-lean-pr-testing bot commented Mar 25, 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 b03ed40 against e6df474 are in. Significant changes detected! @Kha

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

Large changes (119✅, 7🟥)

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

Medium changes (394✅, 3🟥)

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

Small changes (1218✅, 25🟥)

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 25, 2026
Update lean-toolchain for leanprover/lean4#13103
4943a21
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
3b81c73
@mathlib-lean-pr-testing
Copy link

mathlib-lean-pr-testing bot commented Mar 25, 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 2e95453 against e6df474 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 2e95453 to 4cd4726 Compare March 25, 2026 18:24
@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 4cd4726 against e6df474 are in. Significant changes detected! @Kha

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

Large changes (119✅, 7🟥)

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

Medium changes (395✅)

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

Small changes (1237✅, 12🟥)

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 25, 2026
Update lean-toolchain for leanprover/lean4#13103
5cd9874
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
f28bcbc
@mathlib-lean-pr-testing
Copy link

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

Mathlib CI status (docs):

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