chore: fmt bench

[mhuisi]

[mhuisi]

!radar

[leanprover-radar]

Benchmark results for 6aeb7c546948c0300c0f77224ffce662df738d52 against c41cb64ca7cd86a0519d009532bad87bc87e9d2a 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]

!radar

[leanprover-radar]

Benchmark results for 6e4ffe18a2b75e5f29bdb167f73d74b25c2ed636 against c41cb64ca7cd86a0519d009532bad87bc87e9d2a 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]

!radar

[leanprover-radar]

Benchmark results for 330002fe7a484c7cdae50f930877548e53d799f7 against c41cb64ca7cd86a0519d009532bad87bc87e9d2a 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% (🟥).

[leanprover-community-bot]

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]

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]

!radar

[leanprover-radar]

Benchmark results for bce235c78de51516aaec1e96546f464977439bdb against c41cb64ca7cd86a0519d009532bad87bc87e9d2a 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]

!radar

[leanprover-radar]

Benchmark results for 0053745c82988946a53993104fa05d37f80dfa90 against c41cb64ca7cd86a0519d009532bad87bc87e9d2a 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]

!radar

[leanprover-radar]

Benchmark results for 02a9b022c987863c1dc14a3e97b3eef11706e4ee against c41cb64ca7cd86a0519d009532bad87bc87e9d2a 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]

!radar

[leanprover-radar]

Benchmark results for b19bbcb19a3a602982621e54ef1ad38ba303c025 against c41cb64ca7cd86a0519d009532bad87bc87e9d2a 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]

!radar

[leanprover-radar]

Benchmark results for 0abc2fdbc358fb332b63c79532026c3e96474102 against c41cb64ca7cd86a0519d009532bad87bc87e9d2a 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% (🟥).