!radar

Benchmark results for 14d2adb against 7b3d778 are in! @datokrat

• 🟥 build//instructions: +885.0M (+0.01%)

Large changes (2✅)

• ✅ iterators (compiled)//instructions: -155.9M (-24.19%)
• ✅ iterators (interpreted)//instructions: -1.7G (-4.73%)

Medium changes (1🟥)

• 🟥 iterators (elab)//instructions: +45.2M (+1.55%)

Small changes (6✅, 11🟥)

• 🟥 binarytrees.st//instructions: +5.4M (+0.01%)
• ✅ build/module/Init.Data.Iterators.Lemmas.Combinators.Monadic.Take//instructions: -26.8M (-1.04%)
• 🟥 build/module/Init.Data.Slice.List.Iterator//bytes .olean: +12kiB (+10.41%)
• 🟥 build/module/Lake.Build.Actions//instructions: +23.7M (+0.80%)
• 🟥 build/module/Lake.CLI.Build//instructions: +20.3M (+0.65%)
• 🟥 build/module/Lake.Toml.Data.DateTime//instructions: +36.8M (+1.56%)
• 🟥 build/module/Lake.Toml.Elab.Value//instructions: +44.1M (+0.99%)
• 🟥 build/module/Lean.Compiler.FFI//instructions: +15.4M (+1.76%)
• ✅ build/module/Lean.DocString.Formatter//instructions: -29.9M (-0.49%)
• 🟥 build/module/Lean.Elab.GuardMsgs//instructions: +40.2M (+0.58%)
• 🟥 build/module/Lean.Elab.Parallel//instructions: +47.3M (+0.53%)
• 🟥 build/module/Lean.Server.Completion.CompletionItemCompression//instructions: +56.3M (+0.63%)
• 🟥 build/module/Std.Data.Iterators.Lemmas.Combinators.Drop//instructions: +17.2M (+0.82%)
• ✅ build/module/Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop//instructions: -14.0M (-1.20%)
• ✅ build/module/Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile//instructions: -31.8M (-0.50%)
• ✅ build/module/Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile//instructions: -23.0M (-0.76%)
• ✅ build/module/Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip//instructions: -19.6M (-0.73%)

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7b3d778ab047a176130d38931794714f997a1f7b --onto 2e7fe7e79d151ee91039f086b8036252cdf9b725. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-23 10:40:40)

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 7b3d778ab047a176130d38931794714f997a1f7b --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-23 10:40:42)

!radar

Benchmark results for 0333db3 against 7b3d778 are in! @datokrat

• ✅ build//instructions: -922.7M (-0.01%)

Small changes (6✅, 1🟥)

• ✅ build/module/Init.Data.Iterators.Lemmas.Combinators.Monadic.Take//instructions: -26.9M (-1.05%)
• ✅ build/module/Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift//instructions: -18.4M (-0.66%)
• 🟥 build/module/Std.Data.Iterators.Lemmas.Combinators.Drop//instructions: +19.0M (+0.91%)
• ✅ build/module/Std.Data.Iterators.Lemmas.Combinators.Monadic.Drop//instructions: -14.9M (-1.28%)
• ✅ build/module/Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile//instructions: -35.4M (-0.56%)
• ✅ build/module/Std.Data.Iterators.Lemmas.Combinators.Monadic.TakeWhile//instructions: -25.2M (-0.84%)
• ✅ build/module/Std.Data.Iterators.Lemmas.Combinators.Monadic.Zip//instructions: -20.5M (-0.77%)