chore: introduce and immediately deprecate String.Slice.length (#11286)

This PR adds a function `String.Slice.length`, with the following
deprecation string: There is no constant-time length function on slices.
Use `s.positions.count` instead, or `isEmpty` if you only need to know
whether the slice is empty.

Author: TwoFX

src/Init/Data/String/Slice.lean

@@ -930,6 +930,10 @@ Examples:
 def chars (s : Slice) :=
   Std.Iterators.Iter.map (fun ⟨pos, h⟩ => pos.get h) (positions s)
 
+@[deprecated "There is no constant-time length function on slices. Use `s.positions.count` instead, or `isEmpty` if you only need to know whether the slice is empty." (since := "2025-11-20")]
+def length (s : Slice) : Nat :=
+  s.positions.count
+
 structure RevPosIterator (s : Slice) where
   currPos : s.Pos
 deriving Inhabited

src/Lean/ErrorExplanation.lean

@@ -277,7 +277,7 @@ where
   fence (ticksToClose : Option Nat := none) := attempt do
     let line ← any
     if line.startsWith "```" then
-      let numTicks := line.takeWhile (· == '`') |>.copy |>.length
+      let numTicks := line.takeWhile (· == '`') |>.utf8ByteSize -- this makes sense because we know the slice consists only of ticks
       match ticksToClose with
       | none => return (numTicks, line.drop numTicks)
       | some n =>

src/Lean/Server/FileWorker/ExampleHover.lean

@@ -88,11 +88,11 @@ def rewriteExamples (docstring : String) : String := Id.run do
   -- The current state, which tracks the context of the line being processed
   let mut inOutput : RWState := .normal
   for l in lines do
-    let indent := l.takeWhile (· == ' ') |>.copy |>.length
+    let indent := l.takeWhile (· == ' ') |>.utf8ByteSize -- this makes sense because we know the slice consists only of spaces
     let mut l' := l.trimAsciiStart
     -- Is this a code block fence?
     if l'.startsWith "```" then
-      let count := l'.takeWhile (· == '`') |>.copy |>.length
+      let count := l'.takeWhile (· == '`') |>.utf8ByteSize -- this makes sense because we know the slice consists only of ticks
       l' := l'.dropWhile (· == '`')
       l' := l'.dropWhile (· == ' ')
       match inOutput with

src/lake/Lake/Toml/Data/DateTime.lean

@@ -69,7 +69,7 @@ public def ofString? (t : String) : Option Time := do
     match s.split '.' |>.toList with
     | [s,f] =>
       let time ← ofValid? (← h.toNat?) (← m.toNat?) (← s.toNat?)
-      return {time with fracExponent := f.copy.length-1, fracMantissa := ← f.toNat?}
+      return {time with fracExponent := f.positions.count-1, fracMantissa := ← f.toNat?}
     | [s] =>
       ofValid? (← h.toNat?) (← m.toNat?) (← s.toNat?)
     | _ => none