WIP: refactoring towards verified String.split

[TwoFX]

TBD

[TwoFX]

!radar

[leanprover-radar]

Benchmark results for bb338a9 against 9e18eea are in! @TwoFX

• 🟥 build//instructions: +68.1G (+0.5%)

Large changes (4🟥)

• 🟥 charactersIn//instructions: +1.5G (+3.7%)
• 🟥 identifier auto-completion//instructions: +2.2G (+3.0%)
• 🟥 parser//instructions: +185.9M (+0.5%)
• 🟥 workspaceSymbols//instructions: +1.5G (+5.6%)

Medium changes (1✅, 8🟥)

• 🟥 big_do//instructions: +30.9M (+0.1%)
• 🟥 build/module/Init.Data.Format.Instances//bytes .olean.private: +38kiB (+42.5%)
• 🟥 build/module/Lake.Toml.Data.DateTime//bytes .olean.private: +136kiB (+29.4%)
• 🟥 build/module/Lake.Util.Casing//bytes .olean.private: +38kiB (+33.6%)
• 🟥 build/module/Lake.Util.Date//bytes .olean.private: +38kiB (+23.9%)
• ✅ build/module/Lean.Elab.AutoBound//bytes .olean.private: -31kiB (-21.7%)
• 🟥 iterators (elab)//instructions: +27.8M (+0.9%)
• 🟥 iterators (interpreted)//instructions: +27.9M (+0.1%)
• 🟥 lake startup//instructions: +7.0M (+2.9%)

Small changes (26✅, 973🟥)

Too many entries to display here. View the full report on radar instead.

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-01-28 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-01-29 11:26:01)

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-12228 has successfully built against this PR. (2026-01-29 12:27:41) View Log
• ✅ Mathlib branch lean-pr-testing-12228 has successfully built against this PR. (2026-01-29 14:21:47) View Log

[TwoFX]

!radar

[leanprover-radar]

Benchmark results for 2fb399c against 9e18eea are in! @TwoFX

• 🟥 build//instructions: +60.4G (+0.5%)

Large changes (4🟥)

• 🟥 charactersIn//instructions: +1.5G (+3.7%)
• 🟥 identifier auto-completion//instructions: +2.1G (+2.9%)
• 🟥 parser//instructions: +182.8M (+0.4%)
• 🟥 workspaceSymbols//instructions: +1.5G (+5.6%)

Medium changes (1✅, 6🟥)

• 🟥 build/module/Init.Data.Format.Instances//bytes .olean.private: +29kiB (+32.5%)
• 🟥 build/module/Lake.Toml.Data.DateTime//bytes .olean.private: +116kiB (+25.0%)
• 🟥 build/module/Lake.Util.Casing//bytes .olean.private: +28kiB (+25.2%)
• ✅ build/module/Lean.Elab.AutoBound//bytes .olean.private: -31kiB (-21.7%)
• 🟥 build/module/Std.Data.DTreeMap.Internal.Lemmas//instructions: +1.0G (+0.5%)
• 🟥 iterators (elab)//instructions: +24.6M (+0.8%)
• 🟥 iterators (interpreted)//instructions: +24.4M (+0.1%)

Small changes (28✅, 635🟥)

Too many entries to display here. View the full report on radar instead.