deprecations and test output

Author: kim-em

REPL/Frontend.lean

@@ -20,7 +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.msgs.toList.drop commandState.messages.msgs.size
+  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)

REPL/Main.lean

@@ -208,7 +208,11 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
   let cmdSnapshot :=
   { cmdState
     cmdContext := (cmdSnapshot?.map fun c => c.cmdContext).getD
-      { fileName := "", fileMap := default, tacticCache? := none, snap? := none } }
+      { fileName := "",
+        fileMap := default,
+        tacticCache? := none,
+        snap? := none,
+        cancelTk? := none } }
   let env ← recordCommandSnapshot cmdSnapshot
   let jsonTrees := match s.infotree with
   | some "full" => trees

REPL/Snapshots.lean

@@ -116,8 +116,8 @@ open Lean Elab Tactic
 /-- New messages in a `ProofSnapshot`, relative to an optional previous `ProofSnapshot`. -/
 def newMessages (new : ProofSnapshot) (old? : Option ProofSnapshot := none) : List Lean.Message :=
   match old? with
-  | none => new.coreState.messages.msgs.toList
-  | some old => new.coreState.messages.msgs.toList.drop (old.coreState.messages.msgs.size)
+  | none => new.coreState.messages.toList
+  | some old => new.coreState.messages.toList.drop (old.coreState.messages.toList.length)
 
 /-- New info trees in a `ProofSnapshot`, relative to an optional previous `ProofSnapshot`. -/
 def newInfoTrees (new : ProofSnapshot) (old? : Option ProofSnapshot := none) : List InfoTree :=

test/name_generator.expected.out

@@ -24,13 +24,13 @@
  "goals": []}
 
 {"traces":
- ["[Meta.Tactic.simp.rewrite] @gt_iff_lt:1000, x > 0 ==> 0 < x",
+ ["[Meta.Tactic.simp.rewrite] gt_iff_lt:1000, x > 0 ==> 0 < x",
   "[Meta.Tactic.simp.rewrite] h0:1000, 0 < x ==> True"],
  "proofState": 6,
  "goals": []}
 
 {"traces":
- ["[Meta.Tactic.simp.rewrite] @gt_iff_lt:1000, x > 0 ==> 0 < x",
+ ["[Meta.Tactic.simp.rewrite] gt_iff_lt:1000, x > 0 ==> 0 < x",
   "[Meta.Tactic.simp.rewrite] h0:1000, 0 < x ==> True"],
  "proofState": 7,
  "goals": []}

test/no_goal_sorry.expected.out

@@ -4,8 +4,8 @@
    "endPos": {"line": 2, "column": 18},
    "data": "type expected, got\n  (set Nat : ?m.8 PUnit)"},
   {"severity": "error",
-   "pos": {"line": 3, "column": 2},
-   "endPos": {"line": 3, "column": 7},
-   "data": "no goals to be solved"}],
+   "pos": {"line": 2, "column": 22},
+   "endPos": {"line": 2, "column": 24},
+   "data": "Case tag 'body' not found.\n\nThere are no cases to select."}],
  "env": 0}
 

test/trace_simp.expected.out

@@ -9,7 +9,7 @@
    "pos": {"line": 1, "column": 23},
    "endPos": {"line": 1, "column": 27},
    "data":
-   "[Meta.Tactic.simp.rewrite] f_def:1000, f ==> 37\n[Meta.Tactic.simp.rewrite] @eq_self:1000, 37 = 37 ==> True"}],
+   "[Meta.Tactic.simp.rewrite] f_def:1000, f ==> 37\n[Meta.Tactic.simp.rewrite] eq_self:1000, 37 = 37 ==> True"}],
  "env": 3}
 
 {"sorries":
@@ -28,7 +28,7 @@
 
 {"traces":
  ["[Meta.Tactic.simp.rewrite] f_def:1000, f ==> 37",
-  "[Meta.Tactic.simp.rewrite] @eq_self:1000, 37 = 37 ==> True"],
+  "[Meta.Tactic.simp.rewrite] eq_self:1000, 37 = 37 ==> True"],
  "proofState": 2,
  "goals": []}