feat: fixes for v4.14.0-rc1

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 [],
@@ -130,7 +130,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,
@@ -151,7 +151,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

@@ -125,9 +125,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. -/
@@ -150,7 +150,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⟩ => 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 }
@@ -285,9 +285,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
+nightly

test/Mathlib/lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9c6c2d647e57b2b7a0b42dd8080c698bd33a1b6f",
+   "rev": "7c5548eeeb1748da5c2872dbd866d3acbaea4b3f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9d0bdd07bdfe53383567509348b1fe917fc08de4",
+   "rev": "1357f4f49450abb9dfd4783e38219f4ce84f9785",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "deb279eb7be16848d0bc8387f80d6e41bcdbe738",
+   "rev": "b20a88676fd00affb90cbc9f1ff004ae588103b3",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,16 +35,16 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a96aee5245720f588876021b6a0aa73efee49c76",
+   "rev": "baa65c6339a56bd22b7292aa4511c54b3cc7a6af",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.41",
+   "inputRev": "v0.0.43",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "scope": "",
+   "scope": "leanprover",
    "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
@@ -55,17 +55,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1ef0b288623337cb37edd1222b9c26b4b77c6620",
+   "rev": "9b4088ccf0f44ddd7b1132bb1348aef8cf481e12",
    "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/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8edf04f0977c3183d3b633792e03fd570be1777f",
+   "rev": "fa9f767f542d37d4b39ac10a2863c8367b67fce0",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",

test/Mathlib/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.11.0
+leanprover/lean4:v4.13.0-rc3

test/all_tactics.expected.out

@@ -7,7 +7,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}