Skip to content

perf: remove obsolete old codegen workaround #9311

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
Kha merged 4 commits into from
Dec 12, 2025
Merged

perf: remove obsolete old codegen workaround #9311

Kha merged 4 commits into from
Dec 12, 2025
+2 −4

Conversation

@Kha
Copy link
Member

@Kha Kha commented Jul 11, 2025

No description provided.

@Kha Kha added the awaiting-mathlib We should not merge this until we have a successful Mathlib build label Jul 11, 2025
@Kha
Copy link
Member Author

Kha commented Jul 11, 2025

!bench

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Jul 11, 2025

Here are the benchmark results for commit 9a91298.
The entire run failed.
Found no significant differences.

@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 Jul 11, 2025
@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Jul 11, 2025 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-07-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. (2025-07-11 15:47:26)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 5778a3c0f2dbe17fdac88902478362d66c43fd61 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-07-14 13:50:27)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 9e4f9d317bd5b27bd43b76ba811fdf8a9f6d279e --onto 646df6ba16b3f68de539a085456c323e160e206d. You can force reference manual CI using the force-manual-ci label. (2025-12-12 15:55:58)

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jul 11, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#9311
c0bf938
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Jul 11, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#9311
39a4e8d
@leanprover-community-bot leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR and removed awaiting-mathlib We should not merge this until we have a successful Mathlib build labels Jul 11, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jul 11, 2025 •
edited
Loading

  • ✅ Mathlib branch lean-pr-testing-9311 has successfully built against this PR. (2025-07-11 16:47:59) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5778a3c0f2dbe17fdac88902478362d66c43fd61 --onto 18a82c04fc59d3dba392308e09d65ee431240d89. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-14 13:50:26)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9e4f9d317bd5b27bd43b76ba811fdf8a9f6d279e --onto 19e1fe55f33a8aadc4243da32828b70a4b4677cc. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-12 15:55:56)

@zwarich
Copy link
Contributor

zwarich commented Jul 11, 2025

!bench

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Jul 11, 2025

Here are the benchmark results for commit 9a91298.
The entire run failed.
Found no significant differences.

@Kha Kha force-pushed the push-rquwqnkrswpu branch from 9a91298 to 62a615f Compare July 14, 2025 13:27
@Kha Kha added the merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. label Dec 11, 2025
@Kha
Copy link
Member Author

Kha commented Dec 12, 2025

!bench

@leanprover-radar
Copy link

leanprover-radar commented Dec 12, 2025 •
edited
Loading

Benchmark results for 41bc534 against 9e4f9d3 are in! @Kha

Runs (2)
  • 🟥 build exited with code 2
  • 🟥 other exited with code 2

@Kha
Copy link
Member Author

Kha commented Dec 12, 2025

!bench

@leanprover-radar
Copy link

leanprover-radar commented Dec 12, 2025 •
edited
Loading

Benchmark results for bc76286 against 9e4f9d3 are in! @Kha

No significant changes detected.

@Kha Kha added this pull request to the merge queue Dec 12, 2025
Merged via the queue into leanprover:master with commit 5fff9fb Dec 12, 2025
17 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR merge-ci Enable merge queue CI checks for PR. In particular, produce artifacts for all major platforms. 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.

5 participants

@Kha @leanprover-bot @leanprover-community-bot @zwarich @leanprover-radar