chore: bump toolchain to v4.27.0-rc1

REPL/JSON.lean

@@ -70,7 +70,7 @@ def Message.of (m : Lean.Message) : IO Message := do pure <|
     | .information => .info
     | .warning => .warning
     | .error => .error,
-    data := (← m.data.toString).trim }
+    data := (← m.data.toString).trimAscii.toString }
 
 /-- A Lean `sorry`. -/
 structure Sorry where

REPL/Main.lean

@@ -125,7 +125,7 @@ def tactics (trees : List InfoTree) (env? : Option Environment) : M m (List Tact
   trees.flatMap InfoTree.tactics |>.mapM
     fun ⟨ctx, stx, rootGoals, goals, pos, endPos, ns⟩ => do
       let proofState := some (← ProofSnapshot.create ctx none env? goals rootGoals)
-      let goals := s!"{(← ctx.ppGoals goals)}".trim
+      let goals := s!"{(← ctx.ppGoals goals)}".trimAscii.toString
       let tactic := Format.pretty (← ppTactic ctx stx)
       let proofStateId ← proofState.mapM recordProofSnapshot
       return Tactic.of goals tactic pos endPos proofStateId ns
@@ -134,7 +134,7 @@ def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment
   trees.flatMap InfoTree.rootGoals |>.mapM
     fun ⟨ctx, goals, pos⟩ => do
       let proofState := some (← ProofSnapshot.create ctx none env? goals goals)
-      let goals := s!"{(← ctx.ppGoals goals)}".trim
+      let goals := s!"{(← ctx.ppGoals goals)}".trimAscii.toString
       let proofStateId ← proofState.mapM recordProofSnapshot
       return Sorry.of goals pos pos proofStateId
 
@@ -369,10 +369,10 @@ open REPL
 /-- Get lines from stdin until a blank line is entered. -/
 partial def getLines : IO String := do
   let line ← (← IO.getStdin).getLine
-  if line.trim.isEmpty then
+  if line.trimAscii.isEmpty then
     return line
   else
-    return line.trimRight ++ (← getLines)
+    return line.trimAsciiEnd.toString ++ (← getLines)
 
 instance [ToJson α] [ToJson β] : ToJson (α ⊕ β) where
   toJson x := match x with

REPL/Snapshots.lean

@@ -161,11 +161,11 @@ def runTacticM' (p : ProofSnapshot) (t : TacticM α) : IO ProofSnapshot :=
 def newTraces (new : ProofSnapshot) (old? : Option ProofSnapshot := none) : IO (List String) :=
   match old? with
   | none => (·.1) <$> new.runCoreM (do
-     (← getTraces).toList.mapM fun t => do pure (← t.msg.toString).trim)
+     (← getTraces).toList.mapM fun t => do pure (← t.msg.toString).trimAscii.toString)
   | some old => do
     let oldCount ← (·.1) <$> old.runCoreM (return (← getTraces).size)
     (·.1) <$> new.runCoreM (do
-     ((← getTraces).toList.drop oldCount).mapM fun t => do pure (← t.msg.toString).trim)
+     ((← getTraces).toList.drop oldCount).mapM fun t => do pure (← t.msg.toString).trimAscii.toString)
 
 /--
 Evaluate a `Syntax` into a `TacticM` tactic, and run it in the current `ProofSnapshot`.

lean-toolchain

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

test/Mathlib/lake-manifest.json

@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "2df2f0150c275ad53cb3c90f7c98ec15a56a1a67",
+   "rev": "32d24245c7a12ded17325299fd41d412022cd3fe",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.26.0",
+   "inputRev": "v4.27.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "160af9e8e7d4ae448f3c92edcc5b6a8522453f11",
+   "rev": "8d3713f36dda48467eb61f8c1c4db89c49a6251a",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3591c3f664ac3719c4c86e4483e21e228707bfa2",
+   "rev": "19e5f5cc9c21199be466ef99489e3acab370f079",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e9f31324f15ead11048b1443e62c5deaddd055d2",
+   "rev": "4eb26e1a4806b200ddfe5179d0c2a0fae56c54a7",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b4fb2aa5290ebf61bc5f80a5375ba642f0a49192",
+   "rev": "ef8377f31b5535430b6753a974d685b0019d0681",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.83",
+   "inputRev": "v0.0.84",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2f6d238744c4cb07fdc91240feaf5d4221a27931",
+   "rev": "fb12f5535c80e40119286d9575c9393562252d21",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9312503909aa8e8bb392530145cc1677a6298574",
+   "rev": "523ec6fc8062d2f470fdc8de6f822fe89552b5e6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "24241822ef9d3e7f6a3bcc53ad136e12663db8f3",
+   "rev": "6254bed25866358ce4f841fa5a13b77de04ffbc8",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "933fce7e893f65969714c60cdb4bd8376786044e",
+   "rev": "726b98c53e2da249c1de768fbbbb5e67bc9cef60",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.26.0",
+   "inputRev": "v4.27.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "«repl-mathlib-tests»",

test/Mathlib/lakefile.toml

@@ -4,7 +4,7 @@ defaultTargets = ["ReplMathlibTests"]
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
-rev = "v4.26.0"
+rev = "v4.27.0-rc1"
 
 [[lean_lib]]
 name = "ReplMathlibTests"

test/Mathlib/lean-toolchain

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

test/root_goals.expected.out

@@ -11,7 +11,7 @@
  [{"severity": "info",
    "pos": {"line": 3, "column": 2},
    "endPos": {"line": 3, "column": 8},
-   "data": "Try this:\n  [apply] exact rfl"}],
+   "data": "Try this:\n  [apply] exact Nat.zero_eq_one_mod_iff.mp rfl"}],
  "env": 0}
 
 {"proofStatus": "Completed", "proofState": 2, "goals": []}