Skip to content

test PR for !bench (don't merge) #12049

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
Draft
Garmelon wants to merge 1 commit into
base: master
Choose a base branch
from
Draft

test PR for !bench (don't merge) #12049

Garmelon wants to merge 1 commit into from

Conversation

@Garmelon
Copy link
Contributor

@Garmelon Garmelon commented Jan 19, 2026

For some reason, I couldn't re-open the old PR #11552.

@Garmelon
Copy link
Contributor Author

Garmelon commented Jan 19, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Jan 19, 2026 •
edited
Loading

Benchmark results for 2541bfc against 36eaa68 are in! @Garmelon

  • 🟥 build//instructions: +535.8M (+0.0%)

No significant changes detected.

@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 Jan 19, 2026
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Jan 19, 2026

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 36eaa6874463080426903a00727c04e39fa64732 --onto 3dfd125337305c9de6ddcc7c0330c50f0e39fb8e. You can force Mathlib CI using the force-mathlib-ci label. (2026-01-19 19:26:04)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Jan 19, 2026

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 36eaa6874463080426903a00727c04e39fa64732 --onto 4af9cc05924d81e1d5dd35105fdce007c5bbc2e8. You can force reference manual CI using the force-manual-ci label. (2026-01-19 19:26:05)

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

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

@Garmelon @leanprover-radar @leanprover-community-bot @leanprover-bot