Update to v4.27.0-rc1

Author: JOSHCLUNE

Auto/EvaluateAuto/TestAuto.lean

@@ -164,19 +164,19 @@ def readRunAutoOnConstsResult (resultFile : String) : CoreM (Array (Name × Resu
 where
   analyzeLine (fileName line : String) : CoreM (Name × Result × Nat × Nat) := do
     let line := (line.dropWhile (fun c => c != ' ')).drop 1
-    let s := line.takeWhile (fun c => c != ' ')
+    let s := (line.takeWhile (fun c => c != ' ')).toString
     let .some res := Result.ofConcise? s
       | throwError s!"{decl_name%} :: In file {fileName}, {s} is not a concise representation of a `Result`"
     let line := (line.dropWhile (fun c => c != ' ')).drop 1
-    let s := line.takeWhile (fun c => c != ' ')
+    let s := (line.takeWhile (fun c => c != ' ')).toString
     let .some time := String.toNat? s
       | throwError s!"{decl_name%} :: In file {fileName}, {s} is not a string representation of a Nat"
     let line := (line.dropWhile (fun c => c != ' ')).drop 1
-    let s := line.takeWhile (fun c => c != ' ')
+    let s := (line.takeWhile (fun c => c != ' ')).toString
     let .some hb := String.toNat? s
       | throwError s!"{decl_name%} :: In file {fileName}, {s} is not a string representation of a Nat"
     let line := (line.dropWhile (fun c => c != ' ')).drop 1
-    let name := Name.parseUniqRepr line
+    let name := Name.parseUniqRepr line.toString
     return (name, res, time, hb)
 
 def runAutoOnNamesFile (cfg : EvalAutoConfig) (fname : String) : CoreM Unit := do
@@ -332,7 +332,7 @@ def readEATAResult (config : EvalAutoAsyncConfig) :
   let allFiles := (← System.FilePath.readDir resultFolder).map IO.FS.DirEntry.path
   let mut ret := #[]
   for file in allFiles do
-    if !(← System.FilePath.isDir file) && file.toString.takeRight 7 == ".result" then
+    if !(← System.FilePath.isDir file) && (file.toString.takeEnd 7).toString == ".result" then
       ret := ret.append (← readRunAutoOnConstsResult file.toString)
   return ret
 

Auto/EvaluateAuto/TestTactics.lean

@@ -335,15 +335,15 @@ def readEvalTacticsAtModuleResult (resultFile : String) : CoreM (Array (Name ×
 where
   analyzeLine (fileName line : String) : CoreM (Name × Array (Result × Nat × Nat)) := do
     let line := (line.dropWhile (fun c => c != ' ')).drop 3
-    let tr := (line.takeWhile (fun c => c != ']')).splitOn ", "
+    let tr := ((line.takeWhile (fun c => c != ']')).toString.splitOn ", ")
     let tr : Array (Result × Nat × Nat) ← (Array.mk tr).mapM (fun s => do
       let [sr, st, sh] := s.splitOn " "
-        | throwError "s!{decl_name%} :: In file {fileName}, {s} is not of the form `<result> <time> <heartbeats>`"
+        | throwError s!"{decl_name%} :: In file {fileName}, {s} is not of the form `<result> <time> <heartbeats>`"
       match Result.ofConcise? sr, String.toNat? st, String.toNat? sh with
       | .some r, .some t, .some h => return (r, t, h)
       | _, _, _ => throwError s!"{decl_name%} :: In file {fileName}, {s} is not of the form `<result> <time> <heartbeats>`")
     let line := (line.dropWhile (fun c => c != ']')).drop 2
-    let name := Name.parseUniqRepr line
+    let name := Name.parseUniqRepr line.toString
     return (name, tr)
 
 structure EvalTacticOnMathlibConfig where
@@ -493,9 +493,9 @@ def readETMHTResult (config : EvalTacticOnMathlibConfig) :
   let allPaths ← System.FilePath.walkDir resultFolder
   let mut ret := #[]
   for path in allPaths do
-    if !(← System.FilePath.isDir path) && path.toString.takeRight 7 == ".result" then
+    if !(← System.FilePath.isDir path) && path.toString.takeEnd 7 == ".result" then
       let content ← readEvalTacticsAtModuleResult path.toString
-      let suffix := (path.toString.drop (resultFolder.length + 1)).dropRight 7
+      let suffix := ((path.toString.drop (resultFolder.length + 1)).dropEnd 7).toString
       let modName := (suffix.splitOn "/").foldl (fun a b => Name.str a b) .anonymous
       ret := ret.push (modName, content)
   return ret
@@ -513,13 +513,13 @@ def readETMHTResultAllowNonRet (config : EvalTacticOnMathlibConfig) :
   let mut ret := #[]
   let mut nonRet := #[]
   for path in allPaths do
-    if !(← System.FilePath.isDir path) && path.toString.takeRight 7 == ".result" then
+    if !(← System.FilePath.isDir path) && path.toString.takeEnd 7 == ".result" then
       let raw ← IO.FS.readFile path
       if raw.length == 0 then
-        nonRet := nonRet.push (path.toString.dropRight 7)
+        nonRet := nonRet.push ((path.toString.dropEnd 7).toString)
         continue
       let content ← readEvalTacticsAtModuleResult path.toString
-      let suffix := (path.toString.drop (resultFolder.length + 1)).dropRight 7
+      let suffix := ((path.toString.drop (resultFolder.length + 1)).dropEnd 7).toString
       let modName := (suffix.splitOn "/").foldl (fun a b => Name.str a b) .anonymous
       ret := ret.push (modName, content)
   return (nonRet, ret)
@@ -579,8 +579,8 @@ def readETMHTEvaluateFiles (config : EvalTacticOnMathlibConfig) : CoreM (Array N
     if line.contains ':' then
       let [name, retCode] := line.splitOn ":"
         | throwError "{decl_name%} :: Unexpected line format, line content : `{line}`"
-      let name := name.dropRight 1
-      let retCode := retCode.drop 1
+      let name := (name.dropEnd 1).toString
+      let retCode := (retCode.drop 1).toString
       let some retCode := retCode.toNat?
         | throwError "{decl_name%} :: Unexpected line format, line content : `{line}`"
       retEnd := retEnd.push (str2Name name, retCode)

Auto/EvaluateAuto/TestTranslation.lean

@@ -99,18 +99,18 @@ def readEvalMonoSizeResult (resultFile : String) : CoreM (Array (Name × Nat ×
   (Array.mk lines).mapM analyzeLine
 where analyzeLine (line : String) : CoreM (Name × Nat × Option Nat) := do
   let line := (line.dropWhile (fun c => c != ' ')).drop 1
-  let rawSizeStr := line.takeWhile (fun c => c != ' ')
+  let rawSizeStr := (line.takeWhile (fun c => c != ' ')).toString
   let line := (line.dropWhile (fun c => c != ' ')).drop 1
   let .some rawSize := rawSizeStr.toNat?
     | throwError "{decl_name%} :: {rawSizeStr} is not a string representation of a Nat"
-  let monoSizeStr := line.takeWhile (fun c => c != ' ')
+  let monoSizeStr := (line.takeWhile (fun c => c != ' ')).toString
   let line := (line.dropWhile (fun c => c != ' ')).drop 1
   let mut monoSize? : Option Nat := .none
   if monoSizeStr != "N" then
     let .some monoSize := monoSizeStr.toNat?
       | throwError "{decl_name%} :: {monoSizeStr} is not a string representation of a Nat"
     monoSize? := .some monoSize
-  let name := Name.parseUniqRepr line
+  let name := Name.parseUniqRepr line.toString
   return (name, rawSize, monoSize?)
 
 /--

Auto/IR/SMT.lean

@@ -14,7 +14,7 @@ namespace IR.SMT
 def isSimpleSymbol (s : String) : Bool :=
   let symbSpecials := "~!@$%^&*_-+=<>.?/"
   let front := s.front.isAlpha || (symbSpecials.contains s.front)
-  let body := s.all (fun c => c.isAlphanum || symbSpecials.contains c)
+  let body := s.all (fun c => Char.isAlphanum c || symbSpecials.contains c)
   s.length != 0 && front && body
 
 -- <index>      ::= <numeral> | <symbol>

Auto/Parser/SMTParser.lean

@@ -75,14 +75,14 @@ def LexVal.ofString (s : String) (attr : String) : LexVal :=
     let bdigs := s.drop 2
     .num (bdigs.foldl (fun x c => x * 2 + c.toNat - '0'.toNat) 0)
   | "string" =>
-    let subs := ((s.drop 1).take (s.length - 2)).splitOn "\"\""
+    let subs := ((s.drop 1).take (s.length - 2)).toString.splitOn "\"\""
     .str (String.intercalate "\"" subs)
   | "simplesymbol" => .symb s
-  | "quotedsymbol" => .symb ((s.drop 1).take (s.length - 2))
-  | "keyword"      => .kw (s.drop 1)
+  | "quotedsymbol" => .symb ((s.drop 1).take (s.length - 2)).toString
+  | "keyword"      => .kw (s.drop 1).toString
   | "comment"      =>
     let rn : Nat := if String.Pos.Raw.get s (String.Pos.Raw.prev s (String.Pos.Raw.prev s s.rawEndPos)) == '\r' then 1 else 0
-    .comment ((s.drop 1).take (s.length - 2 - rn))
+    .comment ((s.drop 1).take (s.length - 2 - rn)).toString
   | "reserved"     => .reserved s
   | "forall"       => .reserved "forall"
   | "exists"       => .reserved "exists"

Auto/Parser/TPTP.lean

@@ -400,7 +400,7 @@ def ident2StringConst (s : String) : Option StringConst :=
       match x, y.toNat? with
       | .some l, .some y' => .some (l.push (Char.ofNat y'))
       | _,       _        => .none
-    match s.take 9, (((s.drop 9).splitOn "d").drop 1).foldl foldFn (.some "") with
+    match s.take 9, (((s.drop 9).toString.splitOn "d").drop 1).foldl foldFn (.some "") with
     | "t_strVal_", .some s => .some (.strVal s)
     | _,         _       => .none
 
@@ -428,7 +428,7 @@ open Embedding.Lam in
 def ident2BitVecConst (s : String) : Option BitVecConst :=
   match s.take 7 with
   | "t_bvVal" =>
-    match (s.drop 7).splitOn "_" with
+    match (s.drop 7).toString.splitOn "_" with
     | ["", ns, is] =>
       match ns.toNat?, is.toNat? with
       | .some n, .some i => .some (.bvVal n i)
@@ -550,35 +550,35 @@ def ident2BitVecConst (s : String) : Option BitVecConst :=
       | "ashr", .some n => .some (.bvsmtashr n)
       | _,      _       => .none
   | "t_bvapp" =>
-    match s.take 11, (s.drop 11).splitOn "_" with
+    match s.take 11, (s.drop 11).toString.splitOn "_" with
     | "t_bvappend_", [ns, ms] =>
       match ns.toNat?, ms.toNat? with
       | .some n, .some m => .some (.bvappend n m)
       | _,       _       => .none
     | _,             _        => .none
   | "t_bvext" =>
-    match s.take 12, (s.drop 12).splitOn "_" with
+    match s.take 12, (s.drop 12).toString.splitOn "_" with
     | "t_bvextract_", [ns, hs, ls] =>
       match ns.toNat?, hs.toNat?, ls.toNat? with
       | .some n, .some h, .some l => .some (.bvextract n h l)
       | _,       _,       _       => .none
     | _,              _            => .none
   | "t_bvrep" =>
-    match s.take 11, (s.drop 11).splitOn "_" with
+    match s.take 11, (s.drop 11).toString.splitOn "_" with
     | "t_bvrepeat_", [ws, is] =>
       match ws.toNat?, is.toNat? with
       | .some w, .some i => .some (.bvrepeat w i)
       | _,       _       => .none
     | _,             _        => .none
   | "t_bvzer" =>
-    match s.take 15, (s.drop 15).splitOn "_" with
+    match s.take 15, (s.drop 15).toString.splitOn "_" with
     | "t_bvzeroExtend_", [ws, vs] =>
       match ws.toNat?, vs.toNat? with
       | .some w, .some v => .some (.bvzeroExtend w v)
       | _,       _       => .none
     | _,             _        => .none
   | "t_bvsig" =>
-    match s.take 15, (s.drop 15).splitOn "_" with
+    match s.take 15, (s.drop 15).toString.splitOn "_" with
     | "t_bvsignExtend_", [ws, vs] =>
       match ws.toNat?, vs.toNat? with
       | .some w, .some v => .some (.bvsignExtend w v)

Auto/Tactic.lean

@@ -347,7 +347,7 @@ def addTryThisTacticSeqSuggestion (ref : Syntax) (suggestion : TSyntax ``Lean.Pa
 where
   dedent (s : String) : String :=
     s.splitOn "\n"
-    |>.map (λ line => dropPrefix? line.toSubstring "  ".toSubstring |>.map (·.toString) |>.getD line)
+    |>.map (λ line => dropPrefix? line.toRawSubstring "  ".toRawSubstring |>.map (·.toString) |>.getD line)
     |> String.intercalate "\n"
 
 open Embedding.Lam in

Auto/Translation/LamFOL2SMT.lean

@@ -114,7 +114,7 @@ def SMTNamingInfo.exprToSuggestion (e : Expr) : MetaM String := do
     return toString (← PrettyPrinter.formatTerm ppSyntax)
 
 def SMTNamingInfo.suggestNameForSort (sni : SMTNamingInfo) (s : LamSort) := do
-  let suggestion := ((← go s).take 1).toLower
+  let suggestion := ((← go s).take 1).toString.toLower
   trace[auto.lamFOL2SMT.nameSuggestion] "`{suggestion}` for LamSort `{s}`"
   return suggestion
 where

lakefile.lean

@@ -57,7 +57,7 @@ post_update pkg do
   let v := if args.contains "-q" || args.contains "--quiet" then Verbosity.quiet else v
   let v := if args.contains "-v" || args.contains "--verbose" then Verbosity.verbose else v
   let exitCode? ← LoggerIO.toBaseIO (cfg := {outLv := v.minLogLv}) <| ws.runLakeT do
-    if let some pkg ← findPackage? __name__ then
+    if let some pkg ← findPackageByKey? __name__ then
       let zipperpositionZipFile := pkg.buildDir / zipperposition.zip_name
       let zipperpositionExeFile := pkg.buildDir / zipperposition.exe_name
       if !(← zipperpositionExeFile.pathExists) then
@@ -69,4 +69,4 @@ post_update pkg do
       logError "package not found"
       return 1
   let exitCode := exitCode?.getD 1
-  if exitCode = 0 then return () else error s!"{pkg.name}: failed to download/setup `zipperposition`"
+  if exitCode = 0 then return () else error s!"{pkg.baseName}: failed to download/setup `zipperposition`"

lean-toolchain

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