chore: bump to latest Lean release (4.26.0)

book/FPLean/DependentTypes/IndicesParametersUniverses.lean

@@ -84,7 +84,7 @@ The provided argument
 is not definitionally equal to the expected parameter
   α
 
-Note: The value of parameter 'α' must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary.
+Note: The value of parameter `α` must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary.
 ```
 Similarly, attempting to name an index results in an error:
 ```anchor WithNamedIndex
@@ -100,7 +100,7 @@ The provided argument
 is not definitionally equal to the expected parameter
   α
 
-Note: The value of parameter 'α' must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary.
+Note: The value of parameter `α` must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary.
 ```
 
 Using an appropriate universe level and placing the index after the colon results in a declaration that is acceptable:
@@ -142,7 +142,7 @@ The provided argument
 is not definitionally equal to the expected parameter
   n
 
-Note: The value of parameter 'n' must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary.
+Note: The value of parameter `n` must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary.
 ```
 Using the {anchorName NatParam}`n` as suggested causes the declaration to be accepted:
 

book/FPLean/Examples.lean

@@ -153,14 +153,11 @@ div.paragraph > .eval-steps:not(:last-child), div.paragraph > .eval-steps:not(:l
 
 "#
 
-block_extension Block.leanEvalSteps (steps : Array Highlighted) where
+block_extension Block.leanEvalSteps (steps : Array Highlighted) via withHighlighting where
   data := ToJson.toJson steps
   traverse _ _ _ := pure none
   toTeX := none
-  extraCss := [highlightingStyle, evalStepsStyle]
-  extraJs := [highlightingJs]
-  extraJsFiles := [{filename := "popper.js", contents := popper, sourceMap? := none}, {filename := "tippy.js", contents := tippy, sourceMap? := none}]
-  extraCssFiles := [("tippy-border.css", tippy.border.css)]
+  extraCss := [evalStepsStyle]
   toHtml :=
     open Verso.Output.Html in
     some <| fun _ _ _ data _ => do
@@ -253,18 +250,14 @@ private def getClass : MessageSeverity → String
   | .information => "information"
   | .warning => "warning"
 
-block_extension Block.leanOutput (severity : MessageSeverity) (message : String) (summarize : Bool := false) where
+block_extension Block.leanOutput (severity : MessageSeverity) (message : String) (summarize : Bool := false) via withHighlighting where
   data := ToJson.toJson (severity, message, summarize)
   traverse _ _ _ := do
     pure none
   toTeX :=
     some <| fun _ go _ _ content => do
       pure <| .seq <| ← content.mapM fun b => do
         pure <| .seq #[← go b, .raw "\n"]
-  extraCss := [highlightingStyle]
-  extraJs := [highlightingJs]
-  extraJsFiles := [{filename := "popper.js", contents := popper, sourceMap? := none}, {filename := "tippy.js", contents := tippy, sourceMap? := none}]
-  extraCssFiles := [("tippy-border.css", tippy.border.css)]
   toHtml :=
     open Verso.Output.Html in
     some <| fun _ _ _ data _ => do
@@ -379,25 +372,30 @@ structure EvalStepContext extends CodeContext where
 instance [Monad m] [MonadOptions m] [MonadError m] [MonadLiftT CoreM m] : FromArgs EvalStepContext m where
   fromArgs := (fun x y => EvalStepContext.mk y x) <$> .positional' `step <*> fromArgs
 
+private def replicateString (n : Nat) (c : Char) : String :=
+  n.fold (init := "") fun _ _ s => s.push c
+
+private theorem replicateString_length {n c} : (replicateString n c).length = n := by
+  simp [replicateString]
+  induction n <;> simp [Nat.fold, *]
+
 private def quoteCode (str : String) : String := Id.run do
   let str := if str.startsWith "`" || str.endsWith "`" then " " ++ str ++ " " else str
   let mut n := 1
   let mut run := none
-  let mut iter := str.iter
-  while h : iter.hasNext do
-    let c := iter.curr' h
-    iter := iter.next
+  let mut iter := str.startPos
+  while h : iter ≠ str.endPos do
+    let c := iter.get h
+    iter := iter.next h
     if c == '`' then
       run := some (run.getD 0 + 1)
     else if let some k := run then
       if k > n then n := k
       run := none
 
-  let delim := String.mk (List.replicate n '`')
+  let delim := replicateString n '`'
   return delim ++ str ++ delim
 
-
-
 @[role_expander moduleEvalStep]
 def moduleEvalStep : RoleExpander
   | args, inls => do
@@ -432,7 +430,7 @@ def moduleEvalStep : RoleExpander
 
     if let some step := steps[step.val]? then
       if let some code := code? then
-        _ ← ExpectString.expectString "step" code step.toString.trim
+        _ ← ExpectString.expectString "step" code step.toString.trimAscii.copy
         return #[← ``(Inline.other (Inline.lean $(quote step) {}) #[])]
       else
         let stepStr := step.toString
@@ -462,17 +460,17 @@ private def editCodeBlock [Monad m] [MonadFileMap m] (stx : Syntax) (newContents
   let { start := {line := l1, ..}, .. } := txt.utf8RangeToLspRange rng
   let line1 := (txt.lineStart (l1 + 1)).extract txt.source (txt.lineStart (l1 + 2))
   if line1.startsWith "```" then
-    return some s!"{delims}{line1.dropWhile (· == '`') |>.trim}\n{withNl newContents}{delims}"
+    return some s!"{delims}{line1.dropWhile (· == '`') |>.trimAscii.copy}\n{withNl newContents}{delims}"
   else
     return none
 where
   delims : String := Id.run do
     let mut n := 3
     let mut run := none
-    let mut iter := newContents.iter
-    while h : iter.hasNext do
-      let c := iter.curr' h
-      iter := iter.next
+    let mut iter := newContents.startPos
+    while h : iter ≠ newContents.endPos do
+      let c := iter.get h
+      iter := iter.next h
       if c == '`' then
         run := some (run.getD 0 + 1)
       else if let some k := run then
@@ -491,7 +489,7 @@ def moduleEvalStepBlock : CodeBlockExpander
       let steps := splitHighlighted (· == "===>") fragment
 
       if let some step := steps[step.val]? then
-        _ ← ExpectString.expectString "step" code (withNl step.toString.trim)
+        _ ← ExpectString.expectString "step" code (withNl step.toString.trimAscii.copy)
         return #[← ``(Block.other (Block.lean $(quote step) {}) #[])]
       else
         let ok := steps.mapIdx fun i s => ({suggestion := toString i, postInfo? := some s.toString})
@@ -532,7 +530,7 @@ def moduleEqSteps : CodeBlockExpander
       let steps := splitHighlighted (· ∈ ["={", "}="]) fragment
       let steps ← steps.mapM fun hl => do
         if let some ((.token ⟨.docComment, txt⟩), _) := hl.firstToken then
-          let txt := txt.trim |>.stripPrefix "/--" |>.stripSuffix "-/" |>.trim
+          let txt := txt.trimAscii |>.dropPrefix "/--" |>.dropSuffix "-/" |>.trimAscii |>.copy
           if let some ⟨#[.p txts]⟩ := MD4Lean.parse txt then
             let mut out : Array Term := #[]
             for txt in txts do
@@ -711,15 +709,15 @@ def commandOut : RoleExpander
     let cmd ← oneCodeStr inls
     let output ← Commands.commandOut container cmd
     logSilentInfo output
-    return #[← ``(Inline.code $(quote output.trim))]
+    return #[← ``(Inline.code $(quote output.trimAscii.copy))]
 
 @[code_block_expander commandOut]
 def commandOutCodeBlock : CodeBlockExpander
   | args, outStr => do
     let (container, command) ← ArgParse.run ((·, ·) <$> .positional `container .ident <*> .positional `command .strLit) args
     let output ← Commands.commandOut container command
 
-    _ ← ExpectString.expectString "command output" outStr (withNl output) (useLine := fun l => !l.trim.isEmpty) (preEq := String.trim)
+    _ ← ExpectString.expectString "command output" outStr (withNl output) (useLine := fun l => !l.trimAscii.isEmpty) (preEq := (·.trimAscii.copy))
 
     logSilentInfo output
     return #[← ``(Block.code $(quote output))]
@@ -778,20 +776,20 @@ def commands : CodeBlockExpander
     let mut quoted := false
     for line in specStr.splitOn "\n" do
       if line.startsWith "$$" then
-        commands := commands.push (.quote (line.drop 2 |>.trim))
+        commands := commands.push (.quote (line.drop 2 |>.trimAscii |>.copy))
         quoted := true
       else if line.startsWith "$" then
-        let line := line.drop 1 |>.trim
+        let line := line.drop 1 |>.trimAscii
         quoted := false
         if line.contains '#' then
           let cmd := line.takeWhile (· ≠ '#')
-          let rest := (line.drop (cmd.length + 1)).trim
-          commands := commands.push (.run cmd.trim (some rest))
+          let rest := (line.drop (cmd.positions.count + 1)).trimAscii.copy
+          commands := commands.push (.run cmd.trimAscii.copy (some rest))
         else
-          commands := commands.push (.run line none)
+          commands := commands.push (.run line.copy none)
 
       else if quoted then
-        commands := commands.push (.out line.trimRight)
+        commands := commands.push (.out line.trimAsciiEnd.copy)
     let mut out := #[]
     let mut outStr := ""
     for cmdSpec in commands do
@@ -816,8 +814,8 @@ def commands : CodeBlockExpander
       | .out txt =>
         out := out.push (txt, false)
         outStr := outStr ++ withNl txt
-    unless str.getString.trim == "" && outStr.trim == "" do
-      _ ← ExpectString.expectString "commands" str outStr (preEq := String.trim)
+    unless str.getString.trimAscii.isEmpty && outStr.trimAscii.isEmpty do
+      _ ← ExpectString.expectString "commands" str outStr (preEq := (·.trimAscii.copy))
     if «show» then
       pure #[← ``(Block.other (Block.shellCommands $(quote out)) #[])]
     else pure #[]
@@ -898,7 +896,7 @@ def moduleOutText : RoleExpander
           if let `(inline|role{ $_ $_* }[ $x ]) := (← getRef) then x.raw else str
 
         let suggs : Array Suggestion := strings.map fun msg => {
-          suggestion := quoteCode msg.trim
+          suggestion := quoteCode msg.trimAscii.copy
         }
         let h ←
           if suggs.isEmpty then pure m!""
@@ -917,7 +915,7 @@ def moduleOutText : RoleExpander
               mkNullNode #[tok1, tok2]
             else mkNullNode contents
           for (msg, _) in infos do
-            let msg := msg.toString.trim
+            let msg := msg.toString.trimAscii.copy
             Suggestion.saveSuggestion stx (quoteCode <| ExpectString.abbreviateString msg) (quoteCode msg)
 
       return #[← ``(sorryAx _ true)]
@@ -927,17 +925,17 @@ where
     let str := if str.startsWith "`" || str.endsWith "`" then " " ++ str ++ " " else str
     let mut n := 1
     let mut run := none
-    let mut iter := str.iter
-    while h : iter.hasNext do
-      let c := iter.curr' h
-      iter := iter.next
+    let mut iter := str.startPos
+    while h : iter ≠ str.endPos do
+      let c := iter.get h
+      iter := iter.next h
       if c == '`' then
         run := some (run.getD 0 + 1)
       else if let some k := run then
         if k > n then n := k
         run := none
 
-    let delim := String.mk (List.replicate n '`')
+    let delim := replicateString n '`'
     return delim ++ str ++ delim
 
 macro_rules
@@ -953,22 +951,3 @@ macro_rules
     `(inline|role{%$rs moduleOutText MessageSeverity.error anchor:=$a $arg*}%$re [%$s $str* ]%$e)
   | `(inline|role{%$rs anchorWarningText $a:arg_val $arg*}%$re [%$s $str* ]%$e) =>
     `(inline|role{%$rs moduleOutText MessageSeverity.warning anchor:=$a $arg*}%$re [%$s $str* ]%$e)
-
-
-def hasSubstring (s pattern : String) : Bool :=
-  if h : pattern.endPos.1 = 0 then false
-  else
-    have hPatt := Nat.zero_lt_of_ne_zero h
-    let rec loop (pos : String.Pos.Raw) :=
-      if h : pos.byteIdx + pattern.endPos.byteIdx > s.endPos.byteIdx then
-        false
-      else
-        have := Nat.lt_of_lt_of_le (Nat.add_lt_add_left hPatt _) (Nat.ge_of_not_lt h)
-        if pos.substrEq s pattern 0 pattern.endPos.byteIdx then
-          have := Nat.sub_lt_sub_left this (Nat.add_lt_add_left hPatt _)
-          true
-        else
-          have := Nat.sub_lt_sub_left this (pos.byteIdx_lt_byteIdx_next s)
-          loop (pos.next s)
-      termination_by s.endPos.1 - pos.1
-    loop 0

book/FPLean/Examples/Commands.lean

@@ -35,6 +35,18 @@ def requireContainer (container : Ident) : m Container := do
 private def localeVars : Array String :=
   #["LANG", "LC_ALL"]
 
+private def lakeVars : Array String :=
+  #["ELAN_TOOLCHAIN", "LEAN_SYSROOT", "LEAN", "LAKE", "LAKE_HOME", "LEAN_PATH", "LAKE_CACHE_DIR", "LEAN_AR", "LEAN_CC", "DYLD_LIBRARY_PATH"]
+
+private def fixPath (path : String) :=
+  System.SearchPath.parse path
+    |>.iter
+    |>.map (·.toString)
+    |>.filter (fun p => ((p.find? ".elan").isNone || (p.find? "toolchains").isNone))
+    |>.toList
+    |> System.SearchPath.separator.toString.intercalate
+
+
 def command (container : Ident) (dir : System.FilePath) (command : StrLit) (viaShell := false) : m IO.Process.Output := do
   let c ← ensureContainer container
   unless dir.isRelative do
@@ -49,13 +61,13 @@ def command (container : Ident) (dir : System.FilePath) (command : StrLit) (viaS
     cmd := cmd,
     args := args,
     cwd := dir,
-    env := #[("PATH", some (extraPath ++ path))] ++ localeVars.map (·, some "C.UTF-8")
+    env := #[("PATH", some (extraPath ++ fixPath path))] ++ lakeVars.map (·, none) ++ localeVars.map (·, some "C.UTF-8")
   }
   if out.exitCode != 0 then
     let stdout := m!"Stdout: {indentD out.stdout}"
     let stderr := m!"Stderr: {indentD out.stderr}"
     throwErrorAt command "Non-zero exit code from '{command.getString}' ({out.exitCode}).\n{indentD stdout}\n{indentD stderr}"
-  modifyEnv (containersExt.modifyState · (·.insert container.getId { c with outputs := c.outputs.insert command.getString.trim out.stdout }))
+  modifyEnv (containersExt.modifyState · (·.insert container.getId { c with outputs := c.outputs.insert command.getString.trimAscii.copy out.stdout }))
   return out
 
 where
@@ -71,7 +83,7 @@ where
 
 def commandOut (container : Ident) (command : StrLit) : m String := do
   let c ← requireContainer container
-  if let some out := c.outputs[command.getString.trim]? then
+  if let some out := c.outputs[command.getString.trimAscii.copy]? then
     return out
   else throwErrorAt command "Output not found: {indentD command}"
 

book/FPLean/Examples/Commands/ShLex.lean

@@ -8,12 +8,12 @@ private inductive State where
 
 def shlex (cmd : String) : Except String (Array String) := do
   let mut state : State := .normal
-  let mut iter := cmd.iter
+  let mut iter := cmd.startPos
   let mut out : Array String := #[]
   let mut current : Option String := none
-  while h : iter.hasNext do
-    let c := iter.curr' h
-    iter := iter.next' h
+  while h : iter ≠ cmd.endPos do
+    let c := iter.get h
+    iter := iter.next h
     match state, c with
     | .normal, '\\' =>
       state := .escaped state

book/FPLean/Examples/OtherLanguages.lean

@@ -157,16 +157,16 @@ An anchor consists of a line that contains `ANCHOR:` or `ANCHOR_END:` followed b
 of the anchor.
 -/
 def anchor? (line : String) : Except String (String × Bool) := do
-  let mut line := line.trim
+  let mut line := line.trimAscii
   line := line.dropWhile (· ≠ 'A')
   if line.startsWith "ANCHOR:" then
-    line := line.stripPrefix "ANCHOR:"
-    line := line.trimLeft
-    if line.isEmpty then throw "Expected name after `ANCHOR: `" else return (line, true)
+    line := line.dropPrefix "ANCHOR:"
+    line := line.trimAsciiStart
+    if line.isEmpty then throw "Expected name after `ANCHOR: `" else return (line.copy, true)
   else if line.startsWith "ANCHOR_END:" then
-    line := line.stripPrefix "ANCHOR_END:"
-    line := line.trimLeft
-    if line.isEmpty then throw "Expected name after `ANCHOR_END: `" else return (line, false)
+    line := line.dropPrefix "ANCHOR_END:"
+    line := line.trimAsciiStart
+    if line.isEmpty then throw "Expected name after `ANCHOR_END: `" else return (line.copy, false)
   else throw s!"Expected `ANCHOR:` or `ANCHOR_END:`, got {line}"
 
 private def stringAnchors (s : String) : Except String (String × HashMap String String) := do

book/FPLean/FunctorApplicativeMonad/Applicative.lean

@@ -126,7 +126,7 @@ There is a value with type {anchorName Pairpure2}`β` in scope (namely {anchorNa
 def Pair.pure (x : β) : Pair α β := Pair.mk _ x
 ```
 ```anchorError Pairpure2
-don't know how to synthesize placeholder for argument 'first'
+don't know how to synthesize placeholder for argument `first`
 context:
 β α : Type
 x : β

book/FPLean/GettingToKnow/DatatypesPatterns.lean

@@ -301,7 +301,7 @@ Not considering parameter n of evenLoops:
   it is unchanged in the recursive calls
 no parameters suitable for structural recursion
 
-well-founded recursion cannot be used, 'evenLoops' does not take any (non-fixed) arguments
+well-founded recursion cannot be used, `evenLoops` does not take any (non-fixed) arguments
 ```
 
 :::

book/FPLean/GettingToKnow/Evaluating.lean

@@ -158,7 +158,7 @@ In particular, the example
 yields a quite long error message:
 
 ```anchorError stringAppendReprFunction
-could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type
+could not synthesize a `ToExpr`, `Repr`, or `ToString` instance for type
   String → String
 ```