chore: bump toolchain to v4.27.0-rc1 (#338)

Author: kim-em

DocGen4/Output/Base.lean

@@ -251,12 +251,12 @@ corresponds to which identifier it will thus say that `" + "` corresponds to
 only `+` should be linked, taking care of this is what this function is
 responsible for.
 -/
-def splitWhitespaces (s : String) : (String × String × String) := Id.run do
-  let mut length := s.length
-  let mut s := s.trimLeft
-  let front := "".pushn ' ' (length - s.length)
-  length := s.length
-  s := s.trimRight
+def splitWhitespaces (s : String) : String × String × String :=
+  let length := s.length
+  let s := s.trimAsciiStart
+  let front := "".pushn ' ' (length - s.positions.count)
+  let length := s.positions.count
+  let s := s.trimAsciiEnd.copy
   let back := "".pushn ' ' (length - s.length)
   (front, s, back)
 

DocGen4/Output/Bibtex.lean

@@ -19,7 +19,7 @@ namespace DocGen4.Bibtex
 
 /-- Process the contents of bib file. -/
 def process' (contents : String) : Except String (Array BibItem) := do
-  match BibtexQuery.Parser.bibtexFile ⟨contents, contents.startValidPos⟩ with
+  match BibtexQuery.Parser.bibtexFile ⟨contents, contents.startPos⟩ with
   | .success _ arr =>
     let arr ← arr.toArray.filterMapM ProcessedEntry.ofEntry
     return arr |> sortEntry |> deduplicateTag |>.map fun x =>

DocGen4/Output/DocString.lean

@@ -70,7 +70,7 @@ partial def xmlGetHeadingId (el : Xml.Element) : String :=
 def nameToLink? (s : String) : HtmlM (Option String) := do
   let res ← getResult
   if s.endsWith ".lean" && s.contains '/' then
-    return (← getRoot) ++ s.dropRight 5 ++ ".html"
+    return (← getRoot) ++ s.dropEnd 5 ++ ".html"
   else if let some name := Lean.Syntax.decodeNameLit ("`" ++ s) then
     -- with exactly the same name
     if res.name2ModIdx.contains name then
@@ -106,7 +106,7 @@ def nameToLink? (s : String) : HtmlM (Option String) := do
 def extendLink (s : String)  : HtmlM String := do
   -- for intra doc links
   if s.startsWith "##" then
-    if let some link ← nameToLink? (s.drop 2) then
+    if let some link ← nameToLink? (s.drop 2).copy then
       return link
     else
       return s!"{← getRoot}find/?pattern={s.drop 2}#doc"
@@ -158,7 +158,7 @@ def addHeadingAttributes (el : Element) (funName : String)
 /-- Find a bibitem if `href` starts with `thePrefix`. -/
 def findBibitem? (href : String) (thePrefix : String := "") : HtmlM (Option BibItem) := do
   if href.startsWith thePrefix then
-    pure <| (← read).refsMap[href.drop thePrefix.length]?
+    pure <| (← read).refsMap[href.drop thePrefix.length |>.copy]?
   else
     pure .none
 
@@ -206,8 +206,8 @@ def autoLink (el : Element) : HtmlM Element := do
         let attributes := Std.TreeMap.empty.insert "href" link
         return [Content.Element <| Element.Element "a" attributes #[Content.Character s]]
       | none =>
-        let sHead := s.dropRightWhile (· != '.')
-        let sTail := s.takeRightWhile (· != '.')
+        let sHead := s.dropEndWhile (· != '.') |>.copy
+        let sTail := s.takeEndWhile (· != '.') |>.copy
         let link'? ← nameToLink? sTail
         match link'? with
         | some link' =>
@@ -242,13 +242,13 @@ partial def modifyElement (element : Element) (funName : String) : HtmlM Element
       return ⟨ name, attrs, ← modifyContents contents funName modifyElement ⟩
 
 /-- Find all references in a markdown text. -/
-partial def findAllReferences (refsMap : Std.HashMap String BibItem) (s : String) (i : String.Pos.Raw := 0)
+partial def findAllReferences (refsMap : Std.HashMap String BibItem) (s : String) (i : s.Pos := s.startPos)
     (ret : Std.HashSet String := ∅) : Std.HashSet String :=
-  let lps := s.posOfAux '[' s.rawEndPos i
-  if lps < s.rawEndPos then
-    let lpe := s.posOfAux ']' s.rawEndPos lps
-    if lpe < s.rawEndPos then
-      let citekey := Substring.Raw.toString ⟨s, ⟨lps.1 + 1⟩, lpe⟩
+  let lps := i.find '['
+  if hs : lps ≠ s.endPos then
+    let lpe := lps.find ']'
+    if lpe ≠ s.endPos then
+      let citekey := s.extract (lps.next hs) lpe
       match refsMap[citekey]? with
       | .some _ => findAllReferences refsMap s lpe (ret.insert citekey)
       | .none => findAllReferences refsMap s lpe ret
@@ -264,7 +264,7 @@ def docStringToHtml (docString : String) (funName : String) : HtmlM (Array Html)
       s!"[{s}]: references.html#ref_{s}\n")
   match MD4Lean.renderHtml (docString ++ refsMarkdown) with
   | .some rendered =>
-    match manyDocument ⟨rendered, rendered.startValidPos⟩ with
+    match manyDocument ⟨rendered, rendered.startPos⟩ with
     | .success _ res =>
       let newRes ← modifyElements res funName modifyElement
       -- TODO: use `toString` instead of `eToStringEscaped`

DocGen4/Output/References.lean

@@ -33,7 +33,7 @@ def preprocessBibFile (buildDir : System.FilePath) (contents : String) (process
   IO.FS.writeFile (basePath buildDir / "references.bib") contents
   IO.FS.writeFile (declarationsBasePath buildDir / "references.json") "[]"
   -- if contents is empty, just do nothing
-  if contents.trim.isEmpty then
+  if contents.trimAscii.isEmpty then
     return
   -- run the user provided process function
   let items ← process contents

DocGen4/Output/ToHtmlFormat.lean

@@ -87,7 +87,7 @@ partial def toStringAux : Html → String
 | raw s => s
 
 def toString (html : Html) : String :=
-  html.toStringAux.trimRight
+  html.toStringAux.trimAsciiEnd.copy
 
 partial def textLength : Html → Nat
 | raw s => s.length  -- measures lengths of escape sequences too!
@@ -109,7 +109,7 @@ def jsxText : Parser :=
   withAntiquot (mkAntiquot "jsxText" `jsxText) {
     fn := fun c s =>
       let startPos := s.pos
-      let s := takeWhile1Fn (not ∘ "[{<>}]$".contains) "expected JSX text" c s
+      let s := takeWhile1Fn (!"[{<>}]$".contains ·) "expected JSX text" c s
       mkNodeToken `jsxText startPos true c s }
 
 @[combinator_formatter DocGen4.Jsx.jsxText] def jsxText.formatter : Formatter := pure ()

DocGen4/Process/Attributes.lean

@@ -113,7 +113,7 @@ instance : ToString Linter.DeprecationEntry where
     if let some since := entry.since? then
       string := string ++ s!"(since := \"{since}\")"
 
-    string := string.trimRight
+    string := string.trimAsciiEnd.copy
     return string
 
 /--

DocGen4/Process/Hierarchy.lean

@@ -32,7 +32,7 @@ def toArray : HierarchyMap → Array (Name × Hierarchy)
 def hForIn [Monad m] (t : HierarchyMap) (init : σ) (f : (Name × Hierarchy) → σ → m (ForInStep σ)) : m σ :=
   t.forIn init (fun a b acc => f (a, b) acc)
 
-instance : ForIn m HierarchyMap (Name × Hierarchy) where
+instance [Monad m] : ForIn m HierarchyMap (Name × Hierarchy) where
   forIn := HierarchyMap.hForIn
 
 end HierarchyMap
@@ -105,7 +105,7 @@ partial def fromDirectoryAux (dir : System.FilePath) (previous : Name) : IO (Arr
     if ← entry.path.isDir then
       children := children ++ (← fromDirectoryAux entry.path (.str previous entry.fileName))
     else if entry.path.extension = some "html" then
-      children := children.push <| .str previous (entry.fileName.dropRight ".html".length)
+      children := children.push <| .str previous (entry.fileName.dropEnd ".html".length).copy
   return children
 
 def fromDirectory (dir : System.FilePath) : IO Hierarchy := do
@@ -116,7 +116,7 @@ def fromDirectory (dir : System.FilePath) : IO Hierarchy := do
       else if ← entry.path.isDir then
         children := children ++ (← fromDirectoryAux entry.path (.mkSimple entry.fileName))
       else if entry.path.extension = some "html" then
-        children := children.push <| .mkSimple (entry.fileName.dropRight ".html".length)
+        children := children.push <| .mkSimple (entry.fileName.dropEnd ".html".length).copy
     return Hierarchy.fromArray children
 
 end Hierarchy

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "933fce7e893f65969714c60cdb4bd8376786044e",
+   "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "84b88f7ac9adf382b9668f852cee82487d616792",
+   "rev": "cff8377dbe50aae42cbd04213d5b3dacf742c3ba",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "3ab4379b2b92448717de66b7d3e254ac1487aede",
+   "rev": "f3872ff0d82a43e2ab57595524df3934210f2bb9",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",

lakefile.lean

@@ -36,11 +36,11 @@ def getGitSubDirectory (directory : System.FilePath := "." ) : IO System.FilePat
     let explanation := "Failed to execute git rev-parse --show-prefix"
     let err := s!"git exited with code {out.exitCode} while looking for the git subdirectory in {directory}"
     throw <| IO.userError <| explanation ++ "\n" ++ err
-  let subdir := out.stdout.trimRight
+  let subdir := out.stdout.trimAsciiEnd
   -- e.g. if the Lean package is under a directory "myleanpackage",
   -- `git rev-parse --show-prefix` would return "myleanpackage/".
   -- We drop the trailing path separator.
-  return if subdir = "" then "." else subdir.dropRight 1
+  return if subdir == "".toSlice then "." else subdir.dropEnd 1 |>.copy
 
 /--
 Obtain the Github URL of a project by parsing the origin remote.
@@ -55,7 +55,7 @@ def getGitRemoteUrl (directory : System.FilePath := "." ) (remote : String := "o
     let explanation := "Failed to find a git remote in your project, consider reading: https://github.com/leanprover/doc-gen4#source-locations"
     let err := s!"git exited with code {out.exitCode} while looking for the git remote in {directory}"
     throw <| IO.userError <| explanation ++ "\n" ++ err
-  return out.stdout.trimRight
+  return out.stdout.trimAsciiEnd.copy
 
 /--
 Obtain the git commit hash of the project that is currently getting analyzed.
@@ -68,7 +68,7 @@ def getProjectCommit (directory : System.FilePath := "." ) : IO String := do
   }
   if out.exitCode != 0 then
     throw <| IO.userError <| s!"git exited with code {out.exitCode} while looking for the current commit in {directory}"
-  return out.stdout.trimRight
+  return out.stdout.trimAsciiEnd.copy
 
 def filteredPath (path : FilePath) : List String := path.components.filter (· != ".")
 
@@ -82,11 +82,11 @@ Three link types from git supported:
 def getGithubBaseUrl (url : String) : Option String :=
   if url.startsWith "[email protected]:" && url.endsWith ".git" then
     let url := url.drop "[email protected]:".length
-    let url := url.dropRight ".git".length
+    let url := url.dropEnd ".git".length
     .some s!"https://github.com/{url}"
   else if url.startsWith "https://github.com/" then
     if url.endsWith ".git" then
-      .some <| url.dropRight ".git".length
+      .some <| url.dropEnd ".git".length |>.copy
     else
       .some url
   else
@@ -115,7 +115,7 @@ package_facet srcUri.github (pkg) : String := Job.async do
         s!"Could not interpret Git remote uri {url} as a Github source repo.\n"
           ++ "See README on source URIs for more details."
   let commit ← getProjectCommit pkg.dir
-  logInfo s!"Found git remote for {pkg.name} at {baseUrl} @ {commit}"
+  logInfo s!"Found git remote for {pkg.baseName} at {baseUrl} @ {commit}"
   let subdir ← getGitSubDirectory pkg.dir
   return "/".intercalate <| baseUrl :: "blob" :: commit :: filteredPath (subdir / pkg.config.srcDir)
 

lean-toolchain

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