chore: bump toolchain to v4.27.0-rc1

doc/UsersGuide/Markup.lean

@@ -34,11 +34,11 @@ def log10 (n : Nat) : Nat :=
   else 0
 
 def asCode (s : String) : String :=
-  let lines := s.dropRightWhile (· == '\n') |>.splitToList (· == '\n')
+  let lines := s.dropEndWhile (· == '\n') |>.split (· == '\n') |>.toList
   let lw := log10 lines.length + 1
   let pad (s : String) : String :=
     (lw - s.length).fold (init := s) fun _ _ => (" " ++ ·)
-  (lines.mapIdx fun i l => (s!"{toString (i + 1) |> pad}|{l}⏎\n")) |> String.join |>.trimRight
+  (lines.mapIdx fun i l => (s!"{toString (i + 1) |> pad}|{l}⏎\n")) |> String.join |>.trimAsciiEnd |>.copy
 
 partial def preview (stx : Syntax) : m Std.Format :=
   match stx with
@@ -291,7 +291,7 @@ def markupPreview : DirectiveExpanderOf MarkupPreviewConfig
     let `(block|``` | $expected ```) := blk2
       | throwErrorAt blk1 "Expected anonymous code block"
 
-    let stx ← blocks {} |>.parseString contents.getString.trimRight
+    let stx ← blocks {} |>.parseString contents.getString.trimAsciiEnd.copy
     let p ← preview stx
     let p := p.pretty (width := 35)
 
@@ -310,8 +310,8 @@ def markupPreview : DirectiveExpanderOf MarkupPreviewConfig
     ])
 where
   eq (s1 s2 : String) : Bool :=
-    let lines1 := s1.trim.splitToList (· == '\n') |>.map (·.trimRight)
-    let lines2 := s2.trim.splitToList (· == '\n') |>.map (·.trimRight)
+    let lines1 := s1.trimAscii.split (· == '\n') |>.map (·.trimAsciiEnd) |>.toArray
+    let lines2 := s2.trimAscii.split (· == '\n') |>.map (·.trimAsciiEnd) |>.toArray
     lines1 == lines2
 
   nonemptyI : TSyntax `inline → Bool

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "74835c84b38e4070b8240a063c6417c767e551ae",
+   "rev": "160af9e8e7d4ae448f3c92edcc5b6a8522453f11",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.26.0
+leanprover/lean4:v4.27.0-rc1

src/multi-verso/MultiVerso.lean

@@ -351,7 +351,7 @@ public def fromXrefJson (root : String) (json : Json) : Except String (NameMap R
         | throw s!"Expected JSON array, got {v.compress}"
       let v ← v.mapM fun x => do
         let address ← x.getObjValAs? String "address"
-        let address := address.stripPrefix "/" |>.stripSuffix "/" |>.splitOn "/" |>.toArray
+        let address := address.dropPrefix "/" |>.dropSuffix "/" |>.split "/" |>.toArray |>.map (·.copy)
         let htmlId ← x.getObjValAs? String "id"
         let data ← x.getObjVal? "data"
         pure {link := {root, path := address, htmlId := htmlId.sluggify}, data : RefObject}

src/multi-verso/MultiVerso/Link.lean

@@ -48,4 +48,4 @@ deriving ToJson, FromJson, BEq, Ord, Repr
 
 @[inherit_doc Link.link]
 public def RemoteLink.link (link : RemoteLink) : String :=
-  link.root.stripSuffix "/" ++ link.toLink.link
+  (link.root.dropSuffix "/").copy ++ link.toLink.link

src/multi-verso/MultiVerso/NameMap.lean

@@ -218,10 +218,10 @@ public instance : GetElem? (NameMap α) Name α fun xs n => n ∈ xs where
   getElem? xs x := xs.get? x
 
 
-public instance : ForIn m (NameMap α) (PublicName × α) where
+public instance [Monad m] : ForIn m (NameMap α) (PublicName × α) where
   forIn xs init f := (xs : Std.TreeMap _ _ _).forIn (fun a b acc => f (a, b) acc) init
 
-instance : ForIn m (NameMap α) (Name × α) where
+instance [Monad m] : ForIn m (NameMap α) (Name × α) where
   forIn xs init f := (xs : Std.TreeMap _ _ _).forIn (fun a b acc => f (a.toName, b) acc) init
 
 /--

src/multi-verso/MultiVerso/Path.lean

@@ -58,10 +58,10 @@ This relies on the assumption that the path has only directory-like entries. In
 public def relativize (path : Path) (url : String) : String := Id.run do
   if "/".isPrefixOf url then
     let mut path := path.toSubarray
-    let mut url := url.toSubstring.drop 1
+    let mut url := url.toSlice.drop 1
     while h : path.size > 0 do
       -- Get rid of the common prefix of the paths, to avoid unnecessary "../"s
-      if let some url' := url.dropPrefix? (path[0] ++ "/").toSubstring then
+      if let some url' := url.dropPrefix? (path[0] ++ "/") then
         path := path.drop 1
         url := url'
       else break

src/tests/Tests/Arbitrary.lean

@@ -190,9 +190,9 @@ instance : Arbitrary LetterString where
 
 instance : Shrinkable LetterString where
   shrink s :=
-    if let some first := s.startValidPos.get? then
+    if let some first := s.startPos.get? then
       let rest := s.drop 1
-      [String.singleton first] ++ [rest] ++
+      [String.singleton first] ++ [rest.copy] ++
       (instShrinkableLetter.shrink first |>.map (String.singleton · ++ rest))
     else []
 

src/tests/Tests/VersoManual.lean

@@ -5,4 +5,3 @@ Author: David Thrane Christiansen
 -/
 import Tests.VersoManual.Html
 import Tests.VersoManual.Html.SoftHyphenate
-import Tests.VersoManual.Markdown

src/tests/Tests/VersoManual/Html.lean

@@ -96,7 +96,7 @@ Expected #[D], seeing #[D]
 Done
 -/
 #guard_msgs in
-#eval do
+#eval show IO Unit from do
   let mut here : Zipper := ⟨[], testToc⟩
   let spec := testToc.preorder
 

src/verso-blog/VersoBlog.lean

@@ -765,7 +765,7 @@ def leanOutput : CodeBlockExpanderOf LeanOutputConfig
         pure messages
 
     for m in messages do
-      Verso.Doc.Suggestion.saveSuggestion str (m.take 30 ++ "…") m
+      Verso.Doc.Suggestion.saveSuggestion str ((m.take 30).copy ++ "…") m
     throwErrorAt str "Didn't match - expected one of: {indentD (toMessageData messages)}\nbut got:{indentD (toMessageData str.getString)}"
 where
   withNewline (str : String) := if str == "" || str.back != '\n' then str ++ "\n" else str
@@ -780,7 +780,7 @@ where
     pure <| withNewline <| head ++ (← message.data.toString)
 
   mostlyEqual (ws : WhitespaceMode) (s1 s2 : String) : Bool :=
-    messagesMatch (ws.apply s1.trim) (ws.apply s2.trim)
+    messagesMatch (ws.apply s1.trimAscii.copy) (ws.apply s2.trimAscii.copy)
 
 open Lean Elab Command in
 elab "define_lexed_text" blockName:ident " ← " lexerName:ident : command => do

src/verso-blog/VersoBlog/Basic.lean

@@ -419,24 +419,23 @@ defmethod BlogPost.summary (post : BlogPost) : Array (Block Post) := Id.run do
   out
 
 partial def TraverseState.freshId (state : Blog.TraverseState) (path : Path) (hint : Slug) : Slug := Id.run do
-  let hint := if hint.toString.isEmpty then "x".sluggify else hint
   let mut idStr := mangle (toString hint)
   match state.usedIds[path]? with
   | none => return idStr
   | some used =>
     while used.contains idStr do
-      idStr := next idStr
+      idStr := next idStr.toString
     return idStr
 where
-  next (idStr : Slug) : Slug :=
-    match idStr.toString.takeRightWhile (·.isDigit) with
-    | "" => idStr.toString ++ "1" |>.sluggify
+  next (idStr : String) : Slug :=
+    match idStr.takeEndWhile Char.isDigit |>.copy with
+    | "" => idStr ++ "1" |>.sluggify
     | more =>
       if let some n := more.toNat? then
-        idStr.toString.dropRight (more.length) ++ toString (n + 1) |>.sluggify
+        (idStr.dropEnd more.length).copy ++ toString (n + 1) |>.sluggify
       else
-        idStr.toString.dropRight (more.length) ++ "1" |>.sluggify
-  mangle (idStr : String) : Multi.Slug := Id.run do
+        (idStr.dropEnd more.length).copy ++ "1" |>.sluggify
+  mangle (idStr : String) : Slug := Id.run do
     let mut state := false -- found valid leading char?
     let mut out := ""
     for c in idStr.toList do

src/verso-blog/VersoBlog/LiterateLeanPage.lean

@@ -40,7 +40,7 @@ def loadModuleContent
       let toolchainfile := projectDir / "lean-toolchain"
       if !(← toolchainfile.pathExists) then
         throw <| .userError s!"File {toolchainfile} doesn't exist, couldn't load project"
-      pure (← IO.FS.readFile toolchainfile).trim
+      pure (← IO.FS.readFile toolchainfile).trimAscii.copy
     | some override => pure override
 
   -- Kludge: remove variables introduced by Lake. Clearing out DYLD_LIBRARY_PATH and
@@ -110,7 +110,7 @@ def Helper.fromModule
       let toolchainfile := projectDir / "lean-toolchain"
       if !(← toolchainfile.pathExists) then
         throw <| .userError s!"File {toolchainfile} doesn't exist, couldn't load project"
-      pure (← IO.FS.readFile toolchainfile).trim
+      pure (← IO.FS.readFile toolchainfile).trimAscii.copy
     | some override => pure override
 
   -- Kludge: remove variables introduced by Lake. Clearing out DYLD_LIBRARY_PATH and
@@ -204,40 +204,40 @@ deriving BEq, Hashable, Repr, Inhabited
 
 -- TODO rewrite with dynamic programming
 partial def Pat.match (p : List Pat) (str : String) : Option (Lean.NameMap String) :=
-  go str.startValidPos p
+  go str.startPos p
 where
   go iter
-    | [] => if iter = str.endValidPos then pure {} else failure
+    | [] => if iter = str.endPos then pure {} else failure
     | .char c :: p' =>
-      if h : iter ≠ str.endValidPos then
+      if h : iter ≠ str.endPos then
         if iter.get h == c then
           go (iter.next h) p'
         else failure
       else failure
     | .str s :: p' =>
       go iter (s.toList.map .char ++ p')
     | .var x :: p' => do
-      let mut iter' := str.endValidPos
+      let mut iter' := str.endPos
       while iter' ≥ iter do
         try
           let rest ← go iter' p'
-          return rest.insert x (iter.extract iter')
+          return rest.insert x (str.extract iter iter')
         catch
           | () =>
-            if h : iter' = str.startValidPos then
+            if h : iter' = str.startPos then
               break
             else
               iter' := iter'.prev h
               continue
       failure
     | .any :: p' => do
-      let mut iter' := str.endValidPos
+      let mut iter' := str.endPos
       while iter' ≥ iter do
         try
           return (← go iter' p')
         catch
           | () =>
-            if h : iter' = str.startValidPos then
+            if h : iter' = str.startPos then
               break
             else
               iter' := iter'.prev h
@@ -306,8 +306,8 @@ variable [Monad m] [MonadError m] [MonadQuotation m]
 
 
 partial def getModuleDocString (hl : Highlighted) : m String := do
-  let str := (← getString hl).trim
-  let str := str.stripPrefix "/-!" |>.stripSuffix "-/" |>.trim
+  let str := (← getString hl).trimAscii
+  let str := str.dropPrefix "/-!" |>.dropSuffix "-/" |>.trimAscii |>.copy
   pure str
 where getString : Highlighted → m String
   | .text txt | .unparsed txt => pure txt

src/verso-blog/VersoBlog/LiterateLeanPage/Options.lean

@@ -9,7 +9,6 @@ open Lean MonadOptions
 
 register_option verso.literateMarkdown.logInlines : Bool := {
   defValue := false
-  group := "doc"
   descr := "Whether to log failures to elaborate inline code items in Markdown comments."
 }
 

src/verso-literate/Main.lean

@@ -56,7 +56,7 @@ where
   | .missing => none
 
   wholeFileInfo : SourceInfo → SourceInfo
-    | .original l l' t _ => .original l l' t contents.endPos
+    | .original l l' t _ => .original l l' t contents.rawEndPos
     | i => i
 
 instance : ToJson ElabInline where
@@ -246,16 +246,16 @@ where
           if let some doc := doc? then
             return #[.modDoc (← toModLit doc)]
         else if stx[1].isAtom then
-          if let some doc := MD4Lean.parse (stx[1].getAtomVal.stripSuffix "-/") then
+          if let some doc := MD4Lean.parse (stx[1].getAtomVal.dropSuffix "-/").copy then
             return #[.markdownModDoc doc]
 
     highlight' (Option.map (#[·]) res.info[0]? |>.getD #[]) stx true
     let hl ← modifyGet fun (st : HighlightState) => (Highlighted.fromOutput st.output, {st with output := []})
     let hl ← hl.substM (m := HighlightM) fun str => do
       if str.endsWith "▲" then
-        let str := str.dropWhile (· ≠ '▼') |>.drop 1 |>.dropRight 1
-        let indentStr := str.takeWhile (· ≠ '◄')
-        let str := str.drop (indentStr.length + 1)
+        let str := str.dropWhile (· ≠ '▼' : Char → Bool) |>.drop 1 |>.dropEnd 1
+        let indentStr := str.takeWhile (· ≠ '◄' : Char → Bool)
+        let str := str.drop (indentStr.chars.count + 1)
         let declName := str.toName
         let i := indentStr.toNat!
         if let some v ← findInternalDocString? (← getEnv) declName then

src/verso-literate/VersoLiterate/Exported.lean

@@ -56,7 +56,7 @@ instance : FromJson Char where
   fromJson? v := do
     let v ← v.getStr?
     if h : v.length = 1 then
-      return v.startValidPos.get <| by simp_all; intro hv; subst_eqs
+      return v.startPos.get <| by simp_all; intro hv; subst_eqs
     else throw s!"Expected singleton string for `Char`, but got {v.quote}"
 
 deriving instance ToJson, FromJson for MD4Lean.AttrText, MD4Lean.Text, MD4Lean.Li, MD4Lean.Block, MD4Lean.Document

src/verso-literate/VersoLiterate/Module.lean

@@ -52,7 +52,7 @@ def loadModuleJson
       let toolchainfile := projectDir / "lean-toolchain"
       if !(← toolchainfile.pathExists) then
         throw <| .userError s!"File {toolchainfile} doesn't exist, couldn't load project"
-      pure (← IO.FS.readFile toolchainfile).trim
+      pure (← IO.FS.readFile toolchainfile).trimAscii.copy
     | some override => pure override
 
   -- Kludge: remove variables introduced by Lake. Clearing out DYLD_LIBRARY_PATH and

src/verso-manual/VersoManual.lean

@@ -731,7 +731,7 @@ where
     | [] => pure cfg
 
   fixBase (base : String) : String :=
-    if base.takeRight 1 != "/" then base ++ "/" else base
+    if base.endsWith "/" then base else base ++ "/"
 
   go : ReaderT ExtensionImpls IO UInt32 := do
     let hasError ← IO.mkRef false

src/verso-manual/VersoManual/Basic.lean

@@ -189,9 +189,9 @@ instance : FromJson Numbering where
       else throw s!"Expected exponent 0 for {v.compress}"
     | v@(.str s) =>
       if h : s.length = 1 then
-        return .letter <| s.startValidPos.get <| by
+        return .letter <| s.startPos.get <| by
           have : "".length = 0 := by rfl
-          grind [String.startValidPos_eq_endValidPos_iff]
+          grind => instantiate only [String.startPos_eq_endPos_iff]
       else throw s!"Expected one-character string for {v.compress}"
     | other => throw s!"Expected number or string, got {other.compress}"
 
@@ -252,7 +252,7 @@ instance : GetElem? Domains Name Domain (fun ds d => ds.contents.contains d) whe
 
 instance : EmptyCollection Domains := ⟨({} : NameMap Domain)⟩
 
-instance : ForIn m Domains (Name × Domain) where
+instance [Monad m] : ForIn m Domains (Name × Domain) where
   forIn doms init f := inferInstanceAs (ForIn m (NameMap Domain) (NameMap.PublicName × Domain)) |>.forIn doms init fun (n, dom) v =>
     -- Eta expansion uses a coercion
     f (n, dom) v
@@ -1075,7 +1075,7 @@ def TraverseState.definitionIds (state : TraverseState) (ctxt : TraverseContext)
   if let some examples := state.domains.get? exampleDomain then
     let mut idMap := {}
     for (x, _) in examples.objects do
-      let afterSpace := x.dropWhile (· != ' ')
+      let afterSpace := x.dropWhile (· != ' ') |>.copy
       if exampleDeco.isEqSome afterSpace then
         if let .ok { htmlId := slug, .. } := state.resolveDomainObject exampleDomain x then
           idMap := idMap.insert (x.takeWhile (· != ' ') |>.toName) slug.toString