feat: fixes for v4.14.0-rc1 (leanprover-community#57)

* Bump toolchain to 4.12

Signed-off-by: Andrew Wells <[email protected]>

* No longer need to drop messages and trees in proccessCommandsWithInfoTrees

Signed-off-by: Andrew Wells <[email protected]>

* bump toolchains to nightly

Signed-off-by: Andrew Wells <[email protected]>

* Reformat expected goal state

Signed-off-by: Andrew Wells <[email protected]>

* use flatten and flatMap instead of join and bind

Signed-off-by: Andrew Wells <[email protected]>

* filter out sorries with null position

Signed-off-by: Andrew Wells <[email protected]>

* Update Mathlib tests to nightly/master

Signed-off-by: Andrew Wells <[email protected]>

* Update to nightly-2024-10-21

Signed-off-by: Andrew Wells <[email protected]>

* move to v4.14.0-rc1

* update calc.expected.out

---------

Signed-off-by: Andrew Wells <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>

Author: andrewmw94

REPL/Frontend.lean

@@ -20,10 +20,7 @@ def processCommandsWithInfoTrees
     (commandState : Command.State) : IO (Command.State × List Message × List InfoTree) := do
   let commandState := { commandState with infoState.enabled := true }
   let s ← IO.processCommands inputCtx parserState commandState <&> Frontend.State.commandState
-  let msgs := s.messages.toList.drop commandState.messages.toList.length
-  let trees := s.infoState.trees.toList.drop commandState.infoState.trees.size
-
-  pure (s, msgs, trees)
+  pure (s, s.messages.toList, s.infoState.trees.toList)
 
 /--
 Process some text input, with or without an existing command state.

REPL/JSON.lean

@@ -83,7 +83,7 @@ structure Sorry where
 deriving FromJson
 
 instance : ToJson Sorry where
-  toJson r := Json.mkObj <| .join [
+  toJson r := Json.mkObj <| .flatten [
     [("goal", r.goal)],
     [("proofState", toJson r.proofState)],
     if r.pos.line ≠ 0 then [("pos", toJson r.pos)] else [],
@@ -132,7 +132,7 @@ def Json.nonemptyList [ToJson α] (k : String) : List α → List (String × Jso
   | l  => [⟨k, toJson l⟩]
 
 instance : ToJson CommandResponse where
-  toJson r := Json.mkObj <| .join [
+  toJson r := Json.mkObj <| .flatten [
     [("env", r.env)],
     Json.nonemptyList "messages" r.messages,
     Json.nonemptyList "sorries" r.sorries,
@@ -153,7 +153,7 @@ structure ProofStepResponse where
 deriving ToJson, FromJson
 
 instance : ToJson ProofStepResponse where
-  toJson r := Json.mkObj <| .join [
+  toJson r := Json.mkObj <| .flatten [
     [("proofState", r.proofState)],
     [("goals", toJson r.goals)],
     Json.nonemptyList "messages" r.messages,

REPL/Lean/Environment.lean

@@ -26,6 +26,6 @@ and then replace the new constants.
 def unpickle (path : FilePath) : IO (Environment × CompactedRegion) := unsafe do
   let ((imports, map₂), region) ← _root_.unpickle (Array Import × PHashMap Name ConstantInfo) path
   let env ← importModules imports {} 0
-  return (← env.replay (HashMap.ofList map₂.toList), region)
+  return (← env.replay (Std.HashMap.ofList map₂.toList), region)
 
 end Lean.Environment

REPL/Lean/InfoTree.lean

@@ -131,9 +131,9 @@ partial def filter (p : Info → Bool) (m : MVarId → Bool := fun _ => false) :
   | .context ctx tree => tree.filter p m |>.map (.context ctx)
   | .node info children =>
     if p info then
-      [.node info (children.toList.map (filter p m)).join.toPArray']
+      [.node info (children.toList.map (filter p m)).flatten.toPArray']
     else
-      (children.toList.map (filter p m)).join
+      (children.toList.map (filter p m)).flatten
   | .hole mvar => if m mvar then [.hole mvar] else []
 
 /-- Discard all nodes besides `.context` nodes and `TacticInfo` nodes. -/
@@ -156,7 +156,7 @@ partial def findAllInfo (t : InfoTree) (ctx? : Option ContextInfo) (p : Info →
   | context ctx t => t.findAllInfo (ctx.mergeIntoOuter? ctx?) p
   | node i ts  =>
     let info := if p i then [(i, ctx?)] else []
-    let rest := ts.toList.bind (fun t => t.findAllInfo ctx? p)
+    let rest := ts.toList.flatMap (fun t => t.findAllInfo ctx? p)
     info ++ rest
   | _ => []
 

REPL/Main.lean

@@ -95,18 +95,20 @@ def recordProofSnapshot (proofState : ProofSnapshot) : M m Nat := do
   return id
 
 def sorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) :=
-  trees.bind InfoTree.sorries |>.mapM
-    fun ⟨ctx, g, pos, endPos⟩ => do
-      let (goal, proofState) ← match g with
-      | .tactic g => do
-         let s ← ProofSnapshot.create ctx none env? [g]
-         pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s)
-      | .term lctx (some t) => do
-         let s ← ProofSnapshot.create ctx lctx env? [] [t]
-         pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s)
-      | .term _ none => unreachable!
-      let proofStateId ← proofState.mapM recordProofSnapshot
-      return Sorry.of goal pos endPos proofStateId
+  trees.flatMap InfoTree.sorries |>.filter (fun t => match t.2.1 with
+    | .term _ none => false
+    | _ => true ) |>.mapM
+      fun ⟨ctx, g, pos, endPos⟩ => do
+        let (goal, proofState) ← match g with
+        | .tactic g => do
+           let s ← ProofSnapshot.create ctx none env? [g]
+           pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s)
+        | .term lctx (some t) => do
+           let s ← ProofSnapshot.create ctx lctx env? [] [t]
+           pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s)
+        | .term _ none => unreachable!
+        let proofStateId ← proofState.mapM recordProofSnapshot
+        return Sorry.of goal pos endPos proofStateId
 
 def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format :=
   ctx.runMetaM {} try
@@ -115,7 +117,7 @@ def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format :=
     pure "<failed to pretty print>"
 
 def tactics (trees : List InfoTree) : M m (List Tactic) :=
-  trees.bind InfoTree.tactics |>.mapM
+  trees.flatMap InfoTree.tactics |>.mapM
     fun ⟨ctx, stx, goals, pos, endPos, ns⟩ => do
       let proofState := some (← ProofSnapshot.create ctx none none goals)
       let goals := s!"{(← ctx.ppGoals goals)}".trim
@@ -216,9 +218,9 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
   let env ← recordCommandSnapshot cmdSnapshot
   let jsonTrees := match s.infotree with
   | some "full" => trees
-  | some "tactics" => trees.bind InfoTree.retainTacticInfo
-  | some "original" => trees.bind InfoTree.retainTacticInfo |>.bind InfoTree.retainOriginal
-  | some "substantive" => trees.bind InfoTree.retainTacticInfo |>.bind InfoTree.retainSubstantive
+  | some "tactics" => trees.flatMap InfoTree.retainTacticInfo
+  | some "original" => trees.flatMap InfoTree.retainTacticInfo |>.flatMap InfoTree.retainOriginal
+  | some "substantive" => trees.flatMap InfoTree.retainTacticInfo |>.flatMap InfoTree.retainSubstantive
   | _ => []
   let infotree ← if jsonTrees.isEmpty then
     pure none

REPL/Snapshots.lean

@@ -83,7 +83,7 @@ def unpickle (path : FilePath) : IO (CommandSnapshot × CompactedRegion) := unsa
   let ((imports, map₂, cmdState, cmdContext), region) ←
     _root_.unpickle (Array Import × PHashMap Name ConstantInfo × CompactableCommandSnapshot ×
       Command.Context) path
-  let env ← (← importModules imports {} 0).replay (HashMap.ofList map₂.toList)
+  let env ← (← importModules imports {} 0).replay (Std.HashMap.ofList map₂.toList)
   let p' : CommandSnapshot :=
   { cmdState := { cmdState with env }
     cmdContext }
@@ -194,7 +194,6 @@ def create (ctx : ContextInfo) (lctx? : Option LocalContext) (env? : Option Envi
     (goals : List MVarId) (types : List Expr := []) : IO ProofSnapshot := do
   ctx.runMetaM (lctx?.getD {}) do
     let goals := goals ++ (← types.mapM fun t => Expr.mvarId! <$> Meta.mkFreshExprMVar (some t))
-    goals.head!.withContext do
     let s ← getThe Core.State
     let s := match env? with
     | none => s
@@ -285,9 +284,9 @@ def unpickle (path : FilePath) (cmd? : Option CommandSnapshot) :
   let env ← match cmd? with
   | none =>
     enableInitializersExecution
-    (← importModules imports {} 0).replay (HashMap.ofList map₂.toList)
+    (← importModules imports {} 0).replay (Std.HashMap.ofList map₂.toList)
   | some cmd =>
-    cmd.cmdState.env.replay (HashMap.ofList map₂.toList)
+    cmd.cmdState.env.replay (Std.HashMap.ofList map₂.toList)
   let p' : ProofSnapshot :=
   { coreState := { coreState with env }
     coreContext

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.11.0
+leanprover/lean4:v4.14.0-rc1

test/Mathlib/lake-manifest.json

@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9c6c2d647e57b2b7a0b42dd8080c698bd33a1b6f",
+   "rev": "76e9ebe4176d29cb9cc89c669ab9f1ce32b33c3d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9d0bdd07bdfe53383567509348b1fe917fc08de4",
+   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "deb279eb7be16848d0bc8387f80d6e41bcdbe738",
+   "rev": "45d016d59cf45bcf8493a203e9564cfec5203d9b",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,17 +35,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
+   "rev": "1383e72b40dd62a566896a6e348ffe868801b172",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.41",
+   "inputRev": "v0.0.46",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "scope": "",
-   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
+   "scope": "leanprover",
+   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,20 +55,40 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1ef0b288623337cb37edd1222b9c26b4b77c6620",
+   "rev": "ac7b989cbf99169509433124ae484318e953d201",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "7bedaed1ef024add1e171cc17706b012a9a37802",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "0f1430e6f1193929f13905d450b2a44a54f3927e",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8edf04f0977c3183d3b633792e03fd570be1777f",
+   "rev": "a7fc949f1b05c2a01e01c027fd9f480496a1253e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.14.0-rc1",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "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 = "master"
+rev = "v4.14.0-rc1"
 
 [[lean_lib]]
 name = "ReplMathlibTests"

test/Mathlib/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.11.0
+leanprover/lean4:v4.14.0-rc1

test/all_tactics.expected.out

@@ -9,7 +9,7 @@
    "tactic": "exact t",
    "proofState": 1,
    "pos": {"line": 1, "column": 32},
-   "goals": "t : Nat ⊢ Nat",
+   "goals": "t : Nat\n⊢ Nat",
    "endPos": {"line": 1, "column": 39}}],
  "env": 0}
 

test/calc.expected.out

@@ -1,22 +1,35 @@
 {"tactics":
  [{"usedConstants":
-   ["Trans.trans", "instOfNatNat", "instTransEq", "Nat", "OfNat.ofNat", "Eq"],
+   ["Trans.trans",
+    "sorryAx",
+    "instOfNatNat",
+    "instTransEq",
+    "Nat",
+    "OfNat.ofNat",
+    "Bool.false",
+    "Eq"],
    "tactic": "calc\n  3 = 4 := by sorry\n  4 = 5 := by sorry",
    "proofState": 2,
    "pos": {"line": 1, "column": 22},
    "goals": "⊢ 3 = 5",
    "endPos": {"line": 3, "column": 19}},
+  {"usedConstants": [],
+   "tactic": "\n  3 = 4 := by sorry\n  4 = 5 := by sorry",
+   "proofState": 3,
+   "pos": {"line": 2, "column": 2},
+   "goals": "no goals",
+   "endPos": {"line": 3, "column": 19}},
   {"usedConstants":
    ["sorryAx", "instOfNatNat", "Nat", "OfNat.ofNat", "Bool.false", "Eq"],
    "tactic": "sorry",
-   "proofState": 3,
+   "proofState": 4,
    "pos": {"line": 2, "column": 14},
    "goals": "⊢ 3 = 4",
    "endPos": {"line": 2, "column": 19}},
   {"usedConstants":
    ["sorryAx", "instOfNatNat", "Nat", "OfNat.ofNat", "Bool.false", "Eq"],
    "tactic": "sorry",
-   "proofState": 4,
+   "proofState": 5,
    "pos": {"line": 3, "column": 14},
    "goals": "⊢ 4 = 5",
    "endPos": {"line": 3, "column": 19}}],