Skip to content

chore: fmt bench #11144

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
mhuisi wants to merge 36 commits into
base: master
Choose a base branch
from
Draft

chore: fmt bench #11144

mhuisi wants to merge 36 commits into from

Conversation

@mhuisi
Copy link
Contributor

@mhuisi mhuisi commented Nov 11, 2025

No description provided.

@mhuisi mhuisi added the changelog-no Do not include this PR in the release changelog label Nov 11, 2025
@mhuisi
Copy link
Contributor Author

mhuisi commented Nov 11, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Nov 11, 2025 •
edited
Loading

Benchmark results for 6aeb7c5 against c41cb64 are in! @mhuisi

Runs (1)
  • other exited with code 1 (🟥)
Minor changes (3)
  • stdlib size//bytes .olean changed by +0.3% (🟥).
  • stdlib size//lines changed by +669.0 (🟥).
  • stdlib//instructions changed by +0.2% (🟥).

@mhuisi
Copy link
Contributor Author

mhuisi commented Nov 11, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Nov 11, 2025 •
edited
Loading

Benchmark results for 6e4ffe1 against c41cb64 are in! @mhuisi

Runs (1)
  • other exited with code 1 (🟥)
Minor changes (2)
  • stdlib size//bytes .olean changed by +0.3% (🟥).
  • stdlib//instructions changed by +0.2% (🟥).

@mhuisi
Copy link
Contributor Author

mhuisi commented Nov 11, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Nov 11, 2025 •
edited
Loading

Benchmark results for 330002f against c41cb64 are in! @mhuisi

Major changes (1)
  • import Lean//instructions changed by +1.8% (🟥).
Minor changes (2)
  • stdlib size//bytes .olean changed by +0.3% (🟥).
  • stdlib//instructions changed by +0.2% (🟥).

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

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

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c41cb64ca7cd86a0519d009532bad87bc87e9d2a --onto 838be605acfeeb39186a9af2f56376f2a7fe2246. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-11 21:36:01)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c41cb64ca7cd86a0519d009532bad87bc87e9d2a --onto d464b13569ffd6a2a8cb7e00bbba56e5ab344ac7. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-12 16:45:04)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c41cb64ca7cd86a0519d009532bad87bc87e9d2a --onto 2b85e29cc9828a164f63bcc7ef47581767542460. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-14 14:37:34)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c41cb64ca7cd86a0519d009532bad87bc87e9d2a --onto 5306a3469d20caa5f9d80384a5c1effdb14e9c67. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-21 12:03:18)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c41cb64ca7cd86a0519d009532bad87bc87e9d2a --onto f2e191d0afbb5adcc6f12e1779c8b141fc9af996. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-24 18:43:02)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c41cb64ca7cd86a0519d009532bad87bc87e9d2a --onto b0e6db322421ce368999f08870fd747e45242f86. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-25 13:32:38)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1ae680c5e2f3922ba0c6c257a105426fdab20999 --onto 5bd331e85d9d110a29fb3367dbb21854010ffcbd. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-01 19:00:34)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1ae680c5e2f3922ba0c6c257a105426fdab20999 --onto 455fd0b4488e2adc85f825a52e2ee7d944a5740a. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-05 17:27:28)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1ae680c5e2f3922ba0c6c257a105426fdab20999 --onto 62f2f9229356039356c0469a46d8ecd77be88e2a. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-08 16:07:25)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Nov 11, 2025 •
edited
Loading

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase c41cb64ca7cd86a0519d009532bad87bc87e9d2a --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-11 21:36:03)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 1ae680c5e2f3922ba0c6c257a105426fdab20999 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-01 19:00:35)

@mhuisi
Copy link
Contributor Author

mhuisi commented Nov 12, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Nov 12, 2025 •
edited
Loading

Benchmark results for bce235c against c41cb64 are in! @mhuisi

Major changes (1)
  • import Lean//instructions changed by +1.8% (🟥).
Minor changes (5)
  • lake config import//instructions changed by +0.7% (🟥).
  • lake config tree//instructions changed by +0.8% (🟥).
  • lake env//instructions changed by +0.5% (🟥).
  • stdlib size//bytes .olean changed by +0.3% (🟥).
  • stdlib//instructions changed by +0.2% (🟥).

@mhuisi
Copy link
Contributor Author

mhuisi commented Nov 12, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Nov 12, 2025 •
edited
Loading

Benchmark results for 0053745 against c41cb64 are in! @mhuisi

Major changes (1)
  • import Lean//instructions changed by +1.8% (🟥).
Minor changes (5)
  • lake config import//instructions changed by +0.5% (🟥).
  • lake config tree//instructions changed by +1.0% (🟥).
  • lake env//instructions changed by +0.8% (🟥).
  • stdlib size//bytes .olean changed by +0.3% (🟥).
  • stdlib//instructions changed by +0.2% (🟥).

@mhuisi
Copy link
Contributor Author

mhuisi commented Nov 14, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Nov 14, 2025 •
edited
Loading

Benchmark results for 02a9b02 against c41cb64 are in! @mhuisi

Major changes (1)
  • import Lean//instructions changed by +1.8% (🟥).
Minor changes (5)
  • lake config tree//instructions changed by +0.6% (🟥).
  • lake env//instructions changed by +0.7% (🟥).
  • stdlib size//bytes .olean changed by +0.3% (🟥).
  • stdlib size//bytes .olean.private changed by +0.2% (🟥).
  • stdlib//instructions changed by +0.2% (🟥).

@mhuisi
Copy link
Contributor Author

mhuisi commented Nov 14, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Nov 14, 2025 •
edited
Loading

Benchmark results for b19bbcb against c41cb64 are in! @mhuisi

Major changes (1)
  • import Lean//instructions changed by +1.8% (🟥).
Minor changes (4)
  • lake env//instructions changed by +0.5% (🟥).
  • stdlib size//bytes .olean changed by +0.3% (🟥).
  • stdlib size//bytes .olean.private changed by +0.2% (🟥).
  • stdlib//instructions changed by +0.2% (🟥).

@mhuisi
Copy link
Contributor Author

mhuisi commented Nov 14, 2025

!radar

@leanprover-radar
Copy link

leanprover-radar commented Nov 14, 2025 •
edited
Loading

Benchmark results for 0abc2fd against c41cb64 are in! @mhuisi

Major changes (1)
  • import Lean//instructions changed by +1.8% (🟥).
Minor changes (3)
  • lake config tree//instructions changed by +0.6% (🟥).
  • stdlib size//bytes .olean changed by +0.3% (🟥).
  • stdlib//instructions changed by +0.2% (🟥).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em Awaiting requested review from kim-em kim-em will be requested when the pull request is marked ready for review kim-em is a code owner

Assignees

No one assigned

Labels

changelog-no Do not include this PR in the release changelog 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.

4 participants

@mhuisi @leanprover-radar @leanprover-community-bot @leanprover-bot