Skip to content

chore: rename Substring to Substring.Raw#11154

Merged
TwoFX merged 6 commits intoleanprover:masterfrom
TwoFX:markus/substring-raw
Nov 16, 2025
Merged

chore: rename Substring to Substring.Raw#11154
TwoFX merged 6 commits intoleanprover:masterfrom
TwoFX:markus/substring-raw

Conversation

@TwoFX
Copy link
Copy Markdown
Member

@TwoFX TwoFX commented Nov 12, 2025 •
edited
Loading

This PR renames Substring to Substring.Raw.

This is to signify its status as a second-class citizen (not deprecated, but no real plans for verification, like String.Pos.Raw) and to free up the name Substring for a possible future type String.Substring : String -> Type so that s.Substring is the type of substrings of s.

The functions String.toSubstring and String.toSubstring' will remain for now for bootstrapping reasons.

@TwoFX TwoFX added the changelog-library Library label Nov 12, 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 Nov 13, 2025
@ghost
Copy link
Copy Markdown

ghost commented Nov 13, 2025 •
edited by ghost
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 7f7a4d3eafc3b65249f354b650dd3fb15ed1a1a3 --onto d464b13569ffd6a2a8cb7e00bbba56e5ab344ac7. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-13 10:41:53)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase eb01aaeee4c5f4fad3f19c7f52f15ea84e9f0a9a --onto 2b85e29cc9828a164f63bcc7ef47581767542460. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-14 09:50:52)
  • 💥 Mathlib branch lean-pr-testing-11154 build failed against this PR. (2025-11-16 09:20:11) View Log
  • 💥 Mathlib branch lean-pr-testing-11154 build failed against this PR. (2025-11-16 10:18:38) View Log

@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented Nov 13, 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 7f7a4d3eafc3b65249f354b650dd3fb15ed1a1a3 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-13 10:41:55)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase eb01aaeee4c5f4fad3f19c7f52f15ea84e9f0a9a --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-14 09:50:53)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-15 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. (2025-11-16 09:16:40)

@TwoFX TwoFX force-pushed the markus/substring-raw branch 2 times, most recently from e5156da to 62f831f Compare November 15, 2025 07:42
@TwoFX TwoFX force-pushed the markus/substring-raw branch from 62f831f to b224077 Compare November 16, 2025 07:25
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Nov 16, 2025
Update lean-toolchain for testing leanprover/lean4#11154
c98445f
ghost pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Nov 16, 2025
Update lean-toolchain for testing leanprover/lean4#11154
c88b18c
@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Nov 16, 2025
@TwoFX TwoFX marked this pull request as ready for review November 16, 2025 09:29
@TwoFX TwoFX enabled auto-merge November 16, 2025 09:29
@TwoFX TwoFX added this pull request to the merge queue Nov 16, 2025
Merged via the queue into leanprover:master with commit bf60550 Nov 16, 2025
28 checks passed
@TwoFX TwoFX mentioned this pull request Nov 18, 2025
Merged
github-merge-queue bot pushed a commit that referenced this pull request Nov 18, 2025
@TwoFX
chore: deprecate String.toSubstring (#11232)
03eb2f7 
This PR deprecates `String.toSubstring` in favor of
`String.toRawSubstring` (cf. #11154).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sgraf812 sgraf812 Awaiting requested review from sgraf812 sgraf812 is a code owner

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

@mhuisi mhuisi Awaiting requested review from mhuisi mhuisi is a code owner

@kmill kmill Awaiting requested review from kmill kmill is a code owner

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

@hargoniX hargoniX Awaiting requested review from hargoniX hargoniX is a code owner

@tydeu tydeu Awaiting requested review from tydeu tydeu is a code owner

Assignees

No one assigned

Labels

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-library Library force-mathlib-ci 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.

2 participants

@TwoFX @leanprover-bot