Skip to content

chore: test PR for !bench mathlib #11552

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
Closed
Garmelon wants to merge 1 commit into from
Closed

chore: test PR for !bench mathlib #11552

Garmelon wants to merge 1 commit into from
+2 −0

Conversation

@Garmelon
Copy link
Contributor

@Garmelon Garmelon commented Dec 8, 2025 •
edited
Loading

Don't merge

@Garmelon Garmelon changed the title Test PR for !bench mathlib chore: test PR for !bench mathlib Dec 8, 2025
@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 Dec 8, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Dec 8, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#11552
b4408cd
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Dec 8, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#11552
6734ad9
@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 Dec 8, 2025
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request Dec 8, 2025
@leanprover-bot
Update lean-toolchain for testing leanprover/lean4#11552
8a1ab3e
@Garmelon
Copy link
Contributor Author

Garmelon commented Dec 8, 2025 •
edited
Loading

!bench mathlib
try 8

@leanprover-radar
Copy link

leanprover-radar commented Dec 8, 2025 •
edited
Loading

Benchmark results for leanprover-community/mathlib4-nightly-testing@6734ad9 against leanprover-community/mathlib4-nightly-testing@64d8fd3 are in! @Garmelon

@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label Dec 8, 2025
@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Dec 8, 2025 •
edited
Loading

Reference manual CI status:

@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label Dec 8, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Dec 8, 2025

Mathlib CI status (docs):

@Garmelon Garmelon removed the mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN label Dec 8, 2025
@Garmelon
Copy link
Contributor Author

Garmelon commented Dec 8, 2025

!bench mathlib

@leanprover-radar
Copy link

leanprover-radar commented Dec 8, 2025 •
edited
Loading

Benchmark results for leanprover-community/mathlib4-nightly-testing@6734ad9 against leanprover-community/mathlib4-nightly-testing@64d8fd3 are in! @Garmelon

@Garmelon Garmelon added 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 and removed toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN labels Dec 8, 2025
@Garmelon Garmelon closed this Dec 8, 2025
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-manual CI has verified that the Lean Language Reference builds against this PR builds-mathlib CI has verified that Mathlib builds against this PR 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.

5 participants

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