From 3c7cc5c7d83bc0e6869060877e392cd9b16307ad Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 15 Dec 2025 06:22:45 +1100 Subject: [PATCH 1/3] chore: bump toolchain to v4.27.0-rc1 --- lean-toolchain | 2 +- test/Mathlib/lake-manifest.json | 24 ++++++++++++------------ test/Mathlib/lakefile.toml | 2 +- test/Mathlib/lean-toolchain | 2 +- 4 files changed, 15 insertions(+), 15 deletions(-) diff --git a/lean-toolchain b/lean-toolchain index e59446d5..bd19bde0 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.26.0 +leanprover/lean4:v4.27.0-rc1 diff --git a/test/Mathlib/lake-manifest.json b/test/Mathlib/lake-manifest.json index 7586b608..f91f1b95 100644 --- a/test/Mathlib/lake-manifest.json +++ b/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»", diff --git a/test/Mathlib/lakefile.toml b/test/Mathlib/lakefile.toml index c8812e9b..a94e91b3 100644 --- a/test/Mathlib/lakefile.toml +++ b/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" diff --git a/test/Mathlib/lean-toolchain b/test/Mathlib/lean-toolchain index e59446d5..bd19bde0 100644 --- a/test/Mathlib/lean-toolchain +++ b/test/Mathlib/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.26.0 +leanprover/lean4:v4.27.0-rc1 From 84c3613ccf78e521af7f11cd8c73e4df7cbd0784 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 15 Dec 2025 06:24:09 +1100 Subject: [PATCH 2/3] fix: replace deprecated String.trim with String.trimAscii --- REPL/JSON.lean | 2 +- REPL/Main.lean | 8 ++++---- REPL/Snapshots.lean | 4 ++-- 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/REPL/JSON.lean b/REPL/JSON.lean index ebec4c56..aaeec551 100644 --- a/REPL/JSON.lean +++ b/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 diff --git a/REPL/Main.lean b/REPL/Main.lean index b05583f7..9b36b27d 100644 --- a/REPL/Main.lean +++ b/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 diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean index f6936245..eaebffc4 100644 --- a/REPL/Snapshots.lean +++ b/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`. From 257618cfa92f7020be1ff4d62dc3b458169aac07 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Mon, 15 Dec 2025 06:31:54 +1100 Subject: [PATCH 3/3] test: update expected output for apply? in v4.27.0-rc1 --- test/root_goals.expected.out | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/root_goals.expected.out b/test/root_goals.expected.out index a2cff5bd..7bbd1281 100644 --- a/test/root_goals.expected.out +++ b/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": []}