diff --git a/tests/lean/1162.lean.expected.out b/tests/lean/1162.lean.expected.out
index e6dd4e316e..f8ab5643f8 100644
--- a/tests/lean/1162.lean.expected.out
+++ b/tests/lean/1162.lean.expected.out
@@ -1,2 +1 @@
 1162.lean:10:12: error: equation compiler error, equation #2 has not been used in the compilation, note that the left-hand-side of equation #1 is a variable
-1162.lean:7:4: warning: declaration 'ppday' uses sorry
diff --git a/tests/lean/1299.lean.expected.out b/tests/lean/1299.lean.expected.out
index 013a8ecaaf..eec7a58a70 100644
--- a/tests/lean/1299.lean.expected.out
+++ b/tests/lean/1299.lean.expected.out
@@ -5,4 +5,4 @@ new_ax
 (a, a)
 1299.lean:13:8: error: invalid theorem 'd2', theorems should not depend on axioms introduced using tactics (solution: mark theorem as a definition)
 theorem d2 : true = true :=
-[incorrect proof]
+sorry
diff --git a/tests/lean/1369.lean.expected.out b/tests/lean/1369.lean.expected.out
index 001d5b1df2..fe30fcc18c 100644
--- a/tests/lean/1369.lean.expected.out
+++ b/tests/lean/1369.lean.expected.out
@@ -1,7 +1,7 @@
-1369.lean:15:8: warning: declaration '_example' uses sorry
+1369.lean:15:0: warning: declaration '[anonymous]' uses sorry
 17 ≤ 555555
 ⊢ 17 ≤ 555555
-1369.lean:21:8: warning: declaration '_example' uses sorry
+1369.lean:21:0: warning: declaration '[anonymous]' uses sorry
 ?m_1 ≤ 555555
 ⊢ ?m_1 ≤ 555555
-1369.lean:33:8: warning: declaration '_example' uses sorry
+1369.lean:33:0: warning: declaration '[anonymous]' uses sorry
diff --git a/tests/lean/anc1.lean.expected.out b/tests/lean/anc1.lean.expected.out
index 2c44b9ec1f..9326c24d80 100644
--- a/tests/lean/anc1.lean.expected.out
+++ b/tests/lean/anc1.lean.expected.out
@@ -1,6 +1,6 @@
 (1, 2) : ℕ × ℕ
 and.intro trivial trivial : true ∧ true
-anc1.lean:5:8: warning: declaration '_example' uses sorry
+anc1.lean:5:0: warning: declaration '[anonymous]' uses sorry
 ⟨1, sorry⟩ : Σ' (x : ℕ), x > 0
 show true, from true.intro : true
 Exists.intro 1 (id_locked (1 ≠ 0) (λ (a : 1 = 0), nat.no_confusion a)) : ∃ (x : ℕ), 1 ≠ 0
diff --git a/tests/lean/assertion1.lean.expected.out b/tests/lean/assertion1.lean.expected.out
index 5cb4980b95..169a8b1b82 100644
--- a/tests/lean/assertion1.lean.expected.out
+++ b/tests/lean/assertion1.lean.expected.out
@@ -1,2 +1 @@
 assertion1.lean:37:21: error: invalid '^.' notation, function 'MonoidalCategory.tensorObjects' does not have explicit argument with type (MonoidalCategory ...)
-assertion1.lean:35:11: warning: declaration 'tensor_on_left' uses sorry
diff --git a/tests/lean/aux_decl_zeta.lean.expected.out b/tests/lean/aux_decl_zeta.lean.expected.out
index 94b1284b3e..7382fbffeb 100644
--- a/tests/lean/aux_decl_zeta.lean.expected.out
+++ b/tests/lean/aux_decl_zeta.lean.expected.out
@@ -8,4 +8,3 @@ has type
   vec ℕ n
 but is expected to have type
   vec ℕ 10
-aux_decl_zeta.lean:5:11: warning: declaration 'f' uses sorry
diff --git a/tests/lean/bad_error2.lean.expected.out b/tests/lean/bad_error2.lean.expected.out
index 4c40faaae1..838f3039fa 100644
--- a/tests/lean/bad_error2.lean.expected.out
+++ b/tests/lean/bad_error2.lean.expected.out
@@ -7,4 +7,3 @@ _match : (∃ (k_1 : ℕ), k + n + k_1 = k + m) → n ≤ m,
 w : ℕ,
 hw : (λ (k_1 : ℕ), k + n + k_1 = k + m) w
 ⊢ n + w = m
-bad_error2.lean:3:8: warning: declaration '_example' uses sorry
diff --git a/tests/lean/bad_error3.lean.expected.out b/tests/lean/bad_error3.lean.expected.out
index 3ea1971fe2..4c4ebcb3e8 100644
--- a/tests/lean/bad_error3.lean.expected.out
+++ b/tests/lean/bad_error3.lean.expected.out
@@ -10,4 +10,3 @@ bad_error3.lean:7:0: error: tactic failed, there are unsolved goals
 state:
 p : ℕ → ℕ → Prop
 ⊢ sorry
-bad_error3.lean:5:4: warning: declaration 'ex' uses sorry
diff --git a/tests/lean/bad_error4.lean.expected.out b/tests/lean/bad_error4.lean.expected.out
index 81c98ea497..b68ddf1942 100644
--- a/tests/lean/bad_error4.lean.expected.out
+++ b/tests/lean/bad_error4.lean.expected.out
@@ -4,4 +4,3 @@ has type
   Π (a : unit) (b : delayed[?m_1]), delayed[?m_2]
 but is expected to have type
   unit → unit
-bad_error4.lean:4:11: warning: declaration 'bar' uses sorry
diff --git a/tests/lean/bad_error5.lean.expected.out b/tests/lean/bad_error5.lean.expected.out
index 56451cb2cc..73f3b6b94a 100644
--- a/tests/lean/bad_error5.lean.expected.out
+++ b/tests/lean/bad_error5.lean.expected.out
@@ -5,4 +5,3 @@ c : S
 bad_error5.lean:13:10: error: failed to add declaration '_interaction' to environment, value has metavariables
 remark: set 'formatter.hide_full_terms' to false to see the complete term
   …
-bad_error5.lean:9:11: warning: declaration 'V' uses sorry
diff --git a/tests/lean/bad_inaccessible.lean.expected.out b/tests/lean/bad_inaccessible.lean.expected.out
index 238b2a1cb2..2bfa2331f3 100644
--- a/tests/lean/bad_inaccessible.lean.expected.out
+++ b/tests/lean/bad_inaccessible.lean.expected.out
@@ -1,10 +1,7 @@
 bad_inaccessible.lean:3:5: error: invalid use of inaccessible term, it is not fixed by other arguments
-bad_inaccessible.lean:2:11: warning: declaration 'f1' uses sorry
 bad_inaccessible.lean:6:7: error: invalid use of inaccessible term, the provided term is
   b
 but is expected to be
   a
-bad_inaccessible.lean:5:11: warning: declaration 'f2' uses sorry
 bad_inaccessible.lean:14:3: error: invalid use of inaccessible term, it is not completely fixed by other arguments
   .?m_1 + 1
-bad_inaccessible.lean:12:11: warning: declaration 'foo' uses sorry
diff --git a/tests/lean/bad_inaccessible2.lean.expected.out b/tests/lean/bad_inaccessible2.lean.expected.out
index 237af993a3..4a7471c3be 100644
--- a/tests/lean/bad_inaccessible2.lean.expected.out
+++ b/tests/lean/bad_inaccessible2.lean.expected.out
@@ -7,4 +7,3 @@ has type
 but is expected to have type
   vec A .(.?m_2 + 1)
 bad_inaccessible2.lean:31:46: error: ill-formed match/equations expression
-bad_inaccessible2.lean:29:11: warning: declaration 'map_head' uses sorry
diff --git a/tests/lean/cls_err.lean.expected.out b/tests/lean/cls_err.lean.expected.out
index 1e51638450..56275436c4 100644
--- a/tests/lean/cls_err.lean.expected.out
+++ b/tests/lean/cls_err.lean.expected.out
@@ -1,4 +1,3 @@
 cls_err.lean:13:2: error: failed to synthesize type class instance for
 A : Type u
 ⊢ H A
-cls_err.lean:12:13: warning: declaration 'tst' uses sorry
diff --git a/tests/lean/crash.lean.expected.out b/tests/lean/crash.lean.expected.out
index 6faee8713c..9bfd19e761 100644
--- a/tests/lean/crash.lean.expected.out
+++ b/tests/lean/crash.lean.expected.out
@@ -16,4 +16,3 @@ P : Prop,
 H : P,
 H' : ¬P
 ⊢ sorry
-crash.lean:6:11: warning: declaration 'crash' uses sorry
diff --git a/tests/lean/ctx.lean.expected.out b/tests/lean/ctx.lean.expected.out
index c02c5723db..a31a6df19a 100644
--- a/tests/lean/ctx.lean.expected.out
+++ b/tests/lean/ctx.lean.expected.out
@@ -6,4 +6,3 @@ b1 b2 b3 : bool,
 h : A = B,
 p1 p2 : A × B
 ⊢ ℕ
-ctx.lean:2:11: warning: declaration 'foo' uses sorry
diff --git a/tests/lean/elab_error_msgs.lean.expected.out b/tests/lean/elab_error_msgs.lean.expected.out
index 89ce929abc..3292e5d0b2 100644
--- a/tests/lean/elab_error_msgs.lean.expected.out
+++ b/tests/lean/elab_error_msgs.lean.expected.out
@@ -8,7 +8,7 @@ but is expected to have type
   ?m_1 → ?m_2 → ?m_4
 Additional information:
 elab_error_msgs.lean:2:0: context: 'eliminator' elaboration was not used for 'and.rec' because it is not fully applied, #2 explicit arguments expected
-elab_error_msgs.lean:5:4: warning: declaration 'bogus_elim' uses sorry
+elab_error_msgs.lean:4:0: warning: declaration 'bogus_elim' uses sorry
 elab_error_msgs.lean:9:0: error: type mismatch at application
   bogus_elim trivial
 term
diff --git a/tests/lean/elab_error_recovery.lean.expected.out b/tests/lean/elab_error_recovery.lean.expected.out
index 5d189125a4..aa8127f7cb 100644
--- a/tests/lean/elab_error_recovery.lean.expected.out
+++ b/tests/lean/elab_error_recovery.lean.expected.out
@@ -35,7 +35,6 @@ elab_error_recovery.lean:8:29: error: don't know how to synthesize placeholder
 context:
 half_baked : ℕ → ℕ
 ⊢ ℕ
-elab_error_recovery.lean:1:4: warning: declaration 'half_baked' uses sorry
 def half_baked._main : ℕ → ℕ :=
 λ (a : ℕ),
   ite (a = 3) 2
diff --git a/tests/lean/empty.lean.expected.out b/tests/lean/empty.lean.expected.out
index a596cf86ed..c0d6a6c209 100644
--- a/tests/lean/empty.lean.expected.out
+++ b/tests/lean/empty.lean.expected.out
@@ -1,3 +1,2 @@
 empty.lean:6:39: error: failed to synthesize type class instance for
 ⊢ nonempty Empty
-empty.lean:6:25: warning: declaration 'v2' uses sorry
diff --git a/tests/lean/eqn_hole.lean.expected.out b/tests/lean/eqn_hole.lean.expected.out
index e7ad3e3c43..647e48b03b 100644
--- a/tests/lean/eqn_hole.lean.expected.out
+++ b/tests/lean/eqn_hole.lean.expected.out
@@ -3,11 +3,9 @@ context:
 f : ℕ → ℕ
 ⊢ ℕ
 eqn_hole.lean:2:11: error: invalid non-exhaustive set of equations (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
-eqn_hole.lean:2:11: warning: declaration 'f' uses sorry
 eqn_hole.lean:8:13: error: don't know how to synthesize placeholder
 context:
 g : ℕ → ℕ,
 n : ℕ
 ⊢ ℕ
 eqn_hole.lean:6:11: error: support for well-founded recursion has not been implemented yet, use 'set_option trace.eqn_compiler true' for additional information
-eqn_hole.lean:6:11: warning: declaration 'g' uses sorry
diff --git a/tests/lean/error_pos.lean.expected.out b/tests/lean/error_pos.lean.expected.out
index 7b9d30fe63..73a9f90ce1 100644
--- a/tests/lean/error_pos.lean.expected.out
+++ b/tests/lean/error_pos.lean.expected.out
@@ -1,6 +1,6 @@
 error_pos.lean:1:39: error: type expected at
   B
-error_pos.lean:1:8: warning: declaration '_example' uses sorry
+error_pos.lean:1:0: warning: declaration '[anonymous]' uses sorry
 error_pos.lean:4:43: error: type expected at
   B
 error_pos.lean:9:40: error: type expected at
diff --git a/tests/lean/eval_expr_error.lean.expected.out b/tests/lean/eval_expr_error.lean.expected.out
index 4db938f794..92b3e72303 100644
--- a/tests/lean/eval_expr_error.lean.expected.out
+++ b/tests/lean/eval_expr_error.lean.expected.out
@@ -5,7 +5,6 @@ A : Type,
 tst1 : tactic unit,
 a : expr
 ⊢ Type
-eval_expr_error.lean:3:9: warning: declaration 'tst1' uses sorry
 eval_expr_error.lean:8:0: error: invalid eval_expr, type mismatch
 state:
 ⊢ true
diff --git a/tests/lean/exact_error_pos.lean.expected.out b/tests/lean/exact_error_pos.lean.expected.out
index b67b812b74..2a635f4bb4 100644
--- a/tests/lean/exact_error_pos.lean.expected.out
+++ b/tests/lean/exact_error_pos.lean.expected.out
@@ -8,7 +8,6 @@ but is expected to have type
   ℕ
 state:
 ⊢ ℕ
-exact_error_pos.lean:4:4: warning: declaration 'ex1' uses sorry
 exact_error_pos.lean:15:14: error: type mismatch at application
   f 0 tt
 term
@@ -19,4 +18,3 @@ but is expected to have type
   ℕ
 state:
 ⊢ ℕ
-exact_error_pos.lean:12:4: warning: declaration 'ex₂' uses sorry
diff --git a/tests/lean/hole_in_fn.lean.expected.out b/tests/lean/hole_in_fn.lean.expected.out
index eacabdaae1..bf2284477d 100644
--- a/tests/lean/hole_in_fn.lean.expected.out
+++ b/tests/lean/hole_in_fn.lean.expected.out
@@ -2,4 +2,3 @@ hole_in_fn.lean:6:13: error: don't know how to synthesize placeholder
 context:
 n : ℕ
 ⊢ ℕ
-hole_in_fn.lean:5:11: warning: declaration 'f' uses sorry
diff --git a/tests/lean/hole_issue2.lean.expected.out b/tests/lean/hole_issue2.lean.expected.out
index 96167fffa5..b85b37bd08 100644
--- a/tests/lean/hole_issue2.lean.expected.out
+++ b/tests/lean/hole_issue2.lean.expected.out
@@ -1,4 +1,4 @@
-hole_issue2.lean:12:25: warning: declaration 'count' uses sorry
+hole_issue2.lean:12:0: warning: declaration 'count' uses sorry
 hole_issue2.lean:22:74: error: don't know how to synthesize placeholder
 context:
 A : Type,
@@ -10,7 +10,6 @@ h : ⟦l₁⟧ ⊆ ⟦l₂⟧,
 w : A,
 hw : ¬list.count w l₁ ≤ list.count w l₂
 ⊢ false
-hole_issue2.lean:18:25: warning: declaration 'decidable_subbag_1' uses sorry
 hole_issue2.lean:29:65: error: don't know how to synthesize placeholder
 context:
 A : Type,
@@ -20,7 +19,6 @@ _match : Π (b : bool), subcount l₁ l₂ = b → decidable (⟦l₁⟧ ⊆ ⟦
 H : subcount l₁ l₂ = ff,
 h : ⟦l₁⟧ ⊆ ⟦l₂⟧
 ⊢ ∀ (a : A), ¬list.count a l₁ ≤ list.count a l₂ → false
-hole_issue2.lean:25:25: warning: declaration 'decidable_subbag_2' uses sorry
 hole_issue2.lean:36:28: error: don't know how to synthesize placeholder
 context:
 A : Type,
@@ -30,4 +28,3 @@ _match : Π (b : bool), subcount l₁ l₂ = b → decidable (⟦l₁⟧ ⊆ ⟦
 H : subcount l₁ l₂ = ff,
 h : ⟦l₁⟧ ⊆ ⟦l₂⟧
 ⊢ false
-hole_issue2.lean:32:25: warning: declaration 'decidable_subbag_3' uses sorry
diff --git a/tests/lean/inaccessible.lean.expected.out b/tests/lean/inaccessible.lean.expected.out
index 1a11f459b4..e69c0c0ed9 100644
--- a/tests/lean/inaccessible.lean.expected.out
+++ b/tests/lean/inaccessible.lean.expected.out
@@ -3,7 +3,6 @@ inaccessible.lean:14:10: error: function expected at
 inaccessible.lean:14:2: error: invalid occurrence of macro expression in pattern (possible solution, mark term as inaccessible using '.( )')
   sorry
 inaccessible.lean:14:17: error: ill-formed match/equations expression
-inaccessible.lean:13:11: warning: declaration 'inv_3' uses sorry
 inaccessible.lean:17:11: error: invalid inaccessible annotation, it cannot be used around functions in applications
 inaccessible.lean:25:12: error: invalid pattern, 'a' already appeared in this pattern
 inaccessible.lean:28:3: error: function expected at
@@ -17,8 +16,6 @@ has type
 but is expected to have type
   imf f sorry
 inaccessible.lean:28:16: error: ill-formed match/equations expression
-inaccessible.lean:27:11: warning: declaration 'inv_7' uses sorry
 inaccessible.lean:31:4: error: invalid pattern, 'a' already appeared in this pattern
 inaccessible.lean:82:3: error: invalid use of inaccessible term, it is not completely fixed by other arguments
   .?m_1 + 1
-inaccessible.lean:80:11: warning: declaration 'map_6' uses sorry
diff --git a/tests/lean/inaccessible2.lean.expected.out b/tests/lean/inaccessible2.lean.expected.out
index 9ee3b6fba9..614ca5c89a 100644
--- a/tests/lean/inaccessible2.lean.expected.out
+++ b/tests/lean/inaccessible2.lean.expected.out
@@ -3,9 +3,7 @@ inaccessible2.lean:5:4: error: invalid use of inaccessible term, the provided te
   f sorry
 but is expected to be
   f a
-inaccessible2.lean:4:11: warning: declaration 'inv_1' uses sorry
 inaccessible2.lean:8:10: error: invalid pattern, must be an application, constant, variable, type ascription or inaccessible term
 inaccessible2.lean:11:39: error: invalid expression, `)` expected
 inaccessible2.lean:14:9: error: invalid pattern, in a constructor application, the parameters of the inductive datatype must be marked as inaccessible
 inaccessible2.lean:14:20: error: ill-formed match/equations expression
-inaccessible2.lean:13:11: warning: declaration 'symm' uses sorry
diff --git a/tests/lean/instance_cache1.lean.expected.out b/tests/lean/instance_cache1.lean.expected.out
index c6ae8091b8..461a6c7a1e 100644
--- a/tests/lean/instance_cache1.lean.expected.out
+++ b/tests/lean/instance_cache1.lean.expected.out
@@ -3,16 +3,13 @@ A : Type ?,
 a : A,
 this : has_add A
 ⊢ has_add A
-instance_cache1.lean:1:11: warning: declaration 'f1' uses sorry
 instance_cache1.lean:6:7: error: failed to synthesize type class instance for
 A : Type ?,
 a : A,
 s : has_add A
 ⊢ has_add A
-instance_cache1.lean:5:11: warning: declaration 'f2' uses sorry
 instance_cache1.lean:9:19: error: failed to synthesize type class instance for
 A : Type ?,
 a : A,
 s : has_add A
 ⊢ has_add A
-instance_cache1.lean:8:11: warning: declaration 'f3' uses sorry
diff --git a/tests/lean/interactive/1313.lean.expected.out b/tests/lean/interactive/1313.lean.expected.out
index 707a0393d1..e96ed8f95f 100644
--- a/tests/lean/interactive/1313.lean.expected.out
+++ b/tests/lean/interactive/1313.lean.expected.out
@@ -1,8 +1,8 @@
-{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":5,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p ∧ q ∧ p"},"response":"additional_message"}
-{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":12,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"additional_message"}
-{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":18,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"additional_message"}
-{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":25,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"additional_message"}
-{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":34,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"additional_message"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":5,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p ∧ q ∧ p"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":5,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p ∧ q ∧ p"},{"caption":"","file_name":"f","pos_col":0,"pos_line":12,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":5,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p ∧ q ∧ p"},{"caption":"","file_name":"f","pos_col":0,"pos_line":12,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},{"caption":"","file_name":"f","pos_col":0,"pos_line":18,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":5,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p ∧ q ∧ p"},{"caption":"","file_name":"f","pos_col":0,"pos_line":12,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},{"caption":"","file_name":"f","pos_col":0,"pos_line":18,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},{"caption":"","file_name":"f","pos_col":0,"pos_line":25,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":5,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p ∧ q ∧ p"},{"caption":"","file_name":"f","pos_col":0,"pos_line":12,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},{"caption":"","file_name":"f","pos_col":0,"pos_line":18,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},{"caption":"","file_name":"f","pos_col":0,"pos_line":25,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},{"caption":"","file_name":"f","pos_col":0,"pos_line":34,"severity":"error","text":"tactic failed, there are unsolved goals\nstate:\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
 {"record":{"state":"p q : Prop,\na : p,\nb : q\n⊢ p ∧ q ∧ p"},"response":"ok","seq_num":4}
 {"record":{"state":"p q : Prop,\na : p,\nb : q\n⊢ p\n\np q : Prop,\na : p,\nb : q\n⊢ q ∧ p"},"response":"ok","seq_num":11}
diff --git a/tests/lean/interactive/complete_field.lean.expected.out b/tests/lean/interactive/complete_field.lean.expected.out
index d1d06b9b2e..1ee8c474d1 100644
--- a/tests/lean/interactive/complete_field.lean.expected.out
+++ b/tests/lean/interactive/complete_field.lean.expected.out
@@ -1,7 +1,7 @@
-{"msg":{"caption":"","file_name":"f","pos_col":14,"pos_line":4,"severity":"error","text":"invalid '^.' notation, 'l' is not a valid \"field\" because environment does not contain 'and.l'\n  h y\nwhich has type\n  p y ∧ q y"},"response":"additional_message"}
-{"msg":{"caption":"","file_name":"f","pos_col":14,"pos_line":8,"severity":"error","text":"invalid '^.' notation, 'le' is not a valid \"field\" because environment does not contain 'and.le'\n  h y\nwhich has type\n  p y ∧ q y"},"response":"additional_message"}
-{"msg":{"caption":"","file_name":"f","pos_col":14,"pos_line":12,"severity":"error","text":"invalid '^.' notation, 'r' is not a valid \"field\" because environment does not contain 'and.r'\n  h y\nwhich has type\n  p y ∧ q y"},"response":"additional_message"}
-{"msg":{"caption":"","file_name":"f","pos_col":39,"pos_line":17,"severity":"error","text":"invalid '^.' notation, identifier or numeral expected"},"response":"additional_message"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":14,"pos_line":4,"severity":"error","text":"invalid '^.' notation, 'l' is not a valid \"field\" because environment does not contain 'and.l'\n  h y\nwhich has type\n  p y ∧ q y"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":14,"pos_line":4,"severity":"error","text":"invalid '^.' notation, 'l' is not a valid \"field\" because environment does not contain 'and.l'\n  h y\nwhich has type\n  p y ∧ q y"},{"caption":"","file_name":"f","pos_col":14,"pos_line":8,"severity":"error","text":"invalid '^.' notation, 'le' is not a valid \"field\" because environment does not contain 'and.le'\n  h y\nwhich has type\n  p y ∧ q y"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":14,"pos_line":4,"severity":"error","text":"invalid '^.' notation, 'l' is not a valid \"field\" because environment does not contain 'and.l'\n  h y\nwhich has type\n  p y ∧ q y"},{"caption":"","file_name":"f","pos_col":14,"pos_line":8,"severity":"error","text":"invalid '^.' notation, 'le' is not a valid \"field\" because environment does not contain 'and.le'\n  h y\nwhich has type\n  p y ∧ q y"},{"caption":"","file_name":"f","pos_col":14,"pos_line":12,"severity":"error","text":"invalid '^.' notation, 'r' is not a valid \"field\" because environment does not contain 'and.r'\n  h y\nwhich has type\n  p y ∧ q y"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":14,"pos_line":4,"severity":"error","text":"invalid '^.' notation, 'l' is not a valid \"field\" because environment does not contain 'and.l'\n  h y\nwhich has type\n  p y ∧ q y"},{"caption":"","file_name":"f","pos_col":14,"pos_line":8,"severity":"error","text":"invalid '^.' notation, 'le' is not a valid \"field\" because environment does not contain 'and.le'\n  h y\nwhich has type\n  p y ∧ q y"},{"caption":"","file_name":"f","pos_col":14,"pos_line":12,"severity":"error","text":"invalid '^.' notation, 'r' is not a valid \"field\" because environment does not contain 'and.r'\n  h y\nwhich has type\n  p y ∧ q y"},{"caption":"","file_name":"f","pos_col":39,"pos_line":17,"severity":"error","text":"invalid '^.' notation, identifier or numeral expected"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
 {"completions":[{"source":,"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":405},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"}],"prefix":"l","response":"ok","seq_num":5}
 {"completions":[{"source":,"text":"left","type":"?a ∧ ?b → ?a"},{"source":{"column":14,"file":"/library/init/logic.lean","line":405},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"}],"prefix":"le","response":"ok","seq_num":9}
diff --git a/tests/lean/interactive/complete_import.lean.expected.out b/tests/lean/interactive/complete_import.lean.expected.out
index 36ca120ddf..b6e2483714 100644
--- a/tests/lean/interactive/complete_import.lean.expected.out
+++ b/tests/lean/interactive/complete_import.lean.expected.out
@@ -1,15 +1,15 @@
-{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},"response":"additional_message"}
-{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},"response":"additional_message"}
-{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},"response":"additional_message"}
-{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},"response":"additional_message"}
-{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},"response":"additional_message"}
-{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},"response":"additional_message"}
-{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},"response":"additional_message"}
-{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},"response":"additional_message"}
-{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},"response":"additional_message"}
-{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},"response":"additional_message"}
-{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},"response":"additional_message"}
-{"msg":{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: bar\ncould not resolve import: bar"},"response":"additional_message"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: bar\ncould not resolve import: bar"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
 {"response":"ok","seq_num":2}
 {"prefix":"","response":"ok","seq_num":4}
diff --git a/tests/lean/interactive/complete_scanner_error.lean.expected.out b/tests/lean/interactive/complete_scanner_error.lean.expected.out
index 0e408f4928..1041602890 100644
--- a/tests/lean/interactive/complete_scanner_error.lean.expected.out
+++ b/tests/lean/interactive/complete_scanner_error.lean.expected.out
@@ -1,3 +1,3 @@
-{"msg":{"caption":"","file_name":"f","pos_col":9,"pos_line":4,"severity":"error","text":"unexpected token"},"response":"additional_message"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":9,"pos_line":4,"severity":"error","text":"unexpected token"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
 {"prefix":"","response":"ok","seq_num":2}
diff --git a/tests/lean/interactive/complete_tactic.lean.expected.out b/tests/lean/interactive/complete_tactic.lean.expected.out
index cfd90f61e3..89e1e7deac 100644
--- a/tests/lean/interactive/complete_tactic.lean.expected.out
+++ b/tests/lean/interactive/complete_tactic.lean.expected.out
@@ -1,6 +1,6 @@
-{"msg":{"caption":"","file_name":"f","pos_col":14,"pos_line":1,"severity":"error","text":"assumption tactic failed\nstate:\n⊢ ?m_1"},"response":"additional_message"}
-{"msg":{"caption":"","file_name":"f","pos_col":8,"pos_line":1,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"},"response":"additional_message"}
-{"msg":{"caption":"","file_name":"f","pos_col":66,"pos_line":5,"severity":"error","text":"invalid expression, unexpected token"},"response":"additional_message"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":14,"pos_line":1,"severity":"error","text":"assumption tactic failed\nstate:\n⊢ ?m_1"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":14,"pos_line":1,"severity":"error","text":"assumption tactic failed\nstate:\n⊢ ?m_1"},{"caption":"","file_name":"f","pos_col":8,"pos_line":1,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":14,"pos_line":1,"severity":"error","text":"assumption tactic failed\nstate:\n⊢ ?m_1"},{"caption":"","file_name":"f","pos_col":8,"pos_line":1,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"},{"caption":"","file_name":"f","pos_col":66,"pos_line":5,"severity":"error","text":"invalid expression, unexpected token"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
 {"prefix":"","response":"ok","seq_num":2}
 {"prefix":"","response":"ok","seq_num":5}
diff --git a/tests/lean/interactive/do_info.lean.expected.out b/tests/lean/interactive/do_info.lean.expected.out
index 84d15baa7c..b3e538d180 100644
--- a/tests/lean/interactive/do_info.lean.expected.out
+++ b/tests/lean/interactive/do_info.lean.expected.out
@@ -1,4 +1,4 @@
-{"msg":{"caption":"trace output","file_name":"f","pos_col":3,"pos_line":4,"severity":"information","text":"a b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ a = ?m_1\n\na b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ ?m_1 = c\n"},"response":"additional_message"}
+{"msgs":[{"caption":"trace output","file_name":"f","pos_col":3,"pos_line":4,"severity":"information","text":"a b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ a = ?m_1\n\na b c : ℕ,\nh : a = b,\na_1 : c = b\n⊢ ?m_1 = c\n"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
 {"record":{"full-id":"tactic.intro","source":,"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"name → tactic expr"},"response":"ok","seq_num":6}
 {"record":{"full-id":"tactic.transitivity","source":,"state":"a b c : ℕ\n⊢ a = b → c = b → a = c","type":"opt_param transparency transparency.semireducible → tactic unit"},"response":"ok","seq_num":9}
diff --git a/tests/lean/interactive/info.lean.expected.out b/tests/lean/interactive/info.lean.expected.out
index 65eddb24f9..e02ab44e11 100644
--- a/tests/lean/interactive/info.lean.expected.out
+++ b/tests/lean/interactive/info.lean.expected.out
@@ -1,4 +1,4 @@
-{"msg":{"caption":"print result","file_name":"f","pos_col":0,"pos_line":18,"severity":"information","text":"@[inline]\ndef id : Π {α : Sort u}, α → α :=\nλ {α : Sort u} (a : α), a"},"response":"additional_message"}
+{"msgs":[{"caption":"print result","file_name":"f","pos_col":0,"pos_line":18,"severity":"information","text":"@[reducible]\ndef id : Π {α : Sort u}, α → α :=\nλ {α : Sort u} (a : α), a"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
 {"record":{"source":},"response":"ok","seq_num":2}
 {"record":{"doc":"reducible"},"response":"ok","seq_num":5}
diff --git a/tests/lean/interactive/my_tac_class.lean.expected.out b/tests/lean/interactive/my_tac_class.lean.expected.out
index 7b37be374e..029ee811f7 100644
--- a/tests/lean/interactive/my_tac_class.lean.expected.out
+++ b/tests/lean/interactive/my_tac_class.lean.expected.out
@@ -1,3 +1,3 @@
-{"msg":{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":58,"severity":"information","text":"test\n"},"response":"additional_message"}
+{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":58,"severity":"information","text":"test\n"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
 {"record":{"source":,"state":"Custom state: 2\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":62}
diff --git a/tests/lean/interactive/nested_traces.lean.expected.out b/tests/lean/interactive/nested_traces.lean.expected.out
index 6aee00eb68..26bf178d4c 100644
--- a/tests/lean/interactive/nested_traces.lean.expected.out
+++ b/tests/lean/interactive/nested_traces.lean.expected.out
@@ -1,3 +1,3 @@
-{"msg":{"caption":"trace output","file_name":"f","pos_col":22,"pos_line":5,"severity":"information","text":"hello\n"},"response":"additional_message"}
-{"msg":{"caption":"trace output","file_name":"f","pos_col":23,"pos_line":6,"severity":"information","text":"test\n"},"response":"additional_message"}
+{"msgs":[{"caption":"trace output","file_name":"f","pos_col":22,"pos_line":5,"severity":"information","text":"hello\n"}],"response":"all_messages"}
+{"msgs":[{"caption":"trace output","file_name":"f","pos_col":22,"pos_line":5,"severity":"information","text":"hello\n"},{"caption":"trace output","file_name":"f","pos_col":23,"pos_line":6,"severity":"information","text":"test\n"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
diff --git a/tests/lean/interactive/rb_map_ts.lean.expected.out b/tests/lean/interactive/rb_map_ts.lean.expected.out
index 0e77fb71ce..15193b785f 100644
--- a/tests/lean/interactive/rb_map_ts.lean.expected.out
+++ b/tests/lean/interactive/rb_map_ts.lean.expected.out
@@ -1,7 +1,7 @@
-{"msg":{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":62,"severity":"information","text":"test\n"},"response":"additional_message"}
-{"msg":{"caption":"print result","file_name":"f","pos_col":0,"pos_line":71,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"},"response":"additional_message"}
-{"msg":{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":77,"severity":"information","text":"test\n"},"response":"additional_message"}
-{"msg":{"caption":"print result","file_name":"f","pos_col":0,"pos_line":85,"severity":"information","text":"theorem ex₂ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"},"response":"additional_message"}
+{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":62,"severity":"information","text":"test\n"}],"response":"all_messages"}
+{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":62,"severity":"information","text":"test\n"},{"caption":"print result","file_name":"f","pos_col":0,"pos_line":71,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"}],"response":"all_messages"}
+{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":62,"severity":"information","text":"test\n"},{"caption":"print result","file_name":"f","pos_col":0,"pos_line":71,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"},{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":77,"severity":"information","text":"test\n"}],"response":"all_messages"}
+{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":62,"severity":"information","text":"test\n"},{"caption":"print result","file_name":"f","pos_col":0,"pos_line":71,"severity":"information","text":"theorem ex₁ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"},{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":77,"severity":"information","text":"test\n"},{"caption":"print result","file_name":"f","pos_col":0,"pos_line":85,"severity":"information","text":"theorem ex₂ : ∀ (p q : Prop), p → q → p ∧ q :=\nλ (p q : Prop) (a : p) (a_1 : q), and.intro a a_1"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
 {"record":{"source":,"state":"Custom state: ⟨x ← 10⟩\np q : Prop,\na : p,\na_1 : q\n⊢ p ∧ q","tactic_params":["(string)"],"text":"trace","type":"string → mytac unit"},"response":"ok","seq_num":63}
 {"record":{"source":,"state":"Custom state: ⟨y ← 20, x ← 10⟩\np q : Prop,\na : p,\na_1 : q\n⊢ p\n\np q : Prop,\na : p,\na_1 : q\n⊢ q","tactic_params":[],"text":"assumption","type":"mytac unit"},"response":"ok","seq_num":67}
diff --git a/tests/lean/interactive/trace.lean.expected.out b/tests/lean/interactive/trace.lean.expected.out
index 88e2406792..ac28d186ba 100644
--- a/tests/lean/interactive/trace.lean.expected.out
+++ b/tests/lean/interactive/trace.lean.expected.out
@@ -1,3 +1,3 @@
-{"msg":{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":3,"severity":"information","text":"foo\n"},"response":"additional_message"}
-{"msg":{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":5,"severity":"information","text":"hello world\n"},"response":"additional_message"}
+{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":3,"severity":"information","text":"foo\n"}],"response":"all_messages"}
+{"msgs":[{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":3,"severity":"information","text":"foo\n"},{"caption":"trace output","file_name":"f","pos_col":2,"pos_line":5,"severity":"information","text":"hello world\n"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
diff --git a/tests/lean/meta_equation_pos.lean.expected.out b/tests/lean/meta_equation_pos.lean.expected.out
index b858f7a35c..00cbacd11b 100644
--- a/tests/lean/meta_equation_pos.lean.expected.out
+++ b/tests/lean/meta_equation_pos.lean.expected.out
@@ -4,5 +4,4 @@ has type
   bool
 but is expected to have type
   ℕ
-meta_equation_pos.lean:1:9: warning: declaration 'f' uses sorry
 ℕ : Type
diff --git a/tests/lean/minimize_errors.lean.expected.out b/tests/lean/minimize_errors.lean.expected.out
index 2353d324c6..2a81ace7b4 100644
--- a/tests/lean/minimize_errors.lean.expected.out
+++ b/tests/lean/minimize_errors.lean.expected.out
@@ -4,7 +4,6 @@ has type
   ℕ → ℕ
 but is expected to have type
   ℕ → ℕ → ℕ
-minimize_errors.lean:1:4: warning: declaration 'f' uses sorry
 f : ℕ → ℕ → ℕ
 g : ℕ → ℕ → ℕ
 def g : ℕ → ℕ → ℕ :=
diff --git a/tests/lean/no_meta_rec_inst.lean.expected.out b/tests/lean/no_meta_rec_inst.lean.expected.out
index bb75af584b..befcbb3fb6 100644
--- a/tests/lean/no_meta_rec_inst.lean.expected.out
+++ b/tests/lean/no_meta_rec_inst.lean.expected.out
@@ -3,4 +3,3 @@ no_meta_rec_inst.lean:5:3: error: tactic.mk_instance failed to generate instance
 state:
 n_has_false : has_false ℕ
 ⊢ has_false ℕ
-no_meta_rec_inst.lean:4:9: warning: declaration 'n_has_false' uses sorry
diff --git a/tests/lean/non_exhaustive_error.lean.expected.out b/tests/lean/non_exhaustive_error.lean.expected.out
index 64298dfb31..56703eab52 100644
--- a/tests/lean/non_exhaustive_error.lean.expected.out
+++ b/tests/lean/non_exhaustive_error.lean.expected.out
@@ -1,2 +1 @@
 non_exhaustive_error.lean:2:11: error: invalid non-exhaustive set of equations (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
-non_exhaustive_error.lean:2:11: warning: declaration 'f' uses sorry
diff --git a/tests/lean/print_ax3.lean.expected.out b/tests/lean/print_ax3.lean.expected.out
index 5faa7cf2d5..633d9a4ca5 100644
--- a/tests/lean/print_ax3.lean.expected.out
+++ b/tests/lean/print_ax3.lean.expected.out
@@ -1,4 +1,4 @@
-print_ax3.lean:13:6: warning: declaration 'foo5' uses sorry
+print_ax3.lean:13:0: warning: declaration 'foo5' uses sorry
 no axioms
 ------
 quot.sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → quot.mk r a = quot.mk r b
diff --git a/tests/lean/quot_bug.lean.expected.out b/tests/lean/quot_bug.lean.expected.out
index d49b118ee6..25310cb708 100644
--- a/tests/lean/quot_bug.lean.expected.out
+++ b/tests/lean/quot_bug.lean.expected.out
@@ -1,2 +1,2 @@
 λ (x : A), f x
-quot_bug.lean:8:8: warning: declaration '_example' uses sorry
+quot_bug.lean:8:0: warning: declaration '[anonymous]' uses sorry
diff --git a/tests/lean/set_attr1.lean.expected.out b/tests/lean/set_attr1.lean.expected.out
index 86e0c2ddd4..a5e7ab33f3 100644
--- a/tests/lean/set_attr1.lean.expected.out
+++ b/tests/lean/set_attr1.lean.expected.out
@@ -2,4 +2,3 @@ set_attr1.lean:14:3: error: tactic failed, there are unsolved goals
 state:
 n : ℕ
 ⊢ f n = n + 1
-set_attr1.lean:13:11: warning: declaration 'ex2' uses sorry
diff --git a/tests/lean/structure_instance_bug.lean.expected.out b/tests/lean/structure_instance_bug.lean.expected.out
index 8508dc43d2..5c1809dd8e 100644
--- a/tests/lean/structure_instance_bug.lean.expected.out
+++ b/tests/lean/structure_instance_bug.lean.expected.out
@@ -1,2 +1 @@
 structure_instance_bug.lean:11:0: error: invalid structure value {...}, field 'B' is implicit and must not be provided
-structure_instance_bug.lean:10:11: warning: declaration 'foo3' uses sorry
diff --git a/tests/lean/structure_instance_bug2.lean.expected.out b/tests/lean/structure_instance_bug2.lean.expected.out
index 285d1aafd2..0d7ac96c71 100644
--- a/tests/lean/structure_instance_bug2.lean.expected.out
+++ b/tests/lean/structure_instance_bug2.lean.expected.out
@@ -1,2 +1 @@
 structure_instance_bug2.lean:4:0: error: invalid structure instance, 'default_smt_pre_config' is not the name of a structure type
-structure_instance_bug2.lean:3:4: warning: declaration 'my_pre_config1' uses sorry
diff --git a/tests/lean/vm_sorry.lean.expected.out b/tests/lean/vm_sorry.lean.expected.out
index 29f9c7954a..9b7ae85324 100644
--- a/tests/lean/vm_sorry.lean.expected.out
+++ b/tests/lean/vm_sorry.lean.expected.out
@@ -1,8 +1,8 @@
-vm_sorry.lean:1:4: warning: declaration 'half_baked' uses sorry
+vm_sorry.lean:1:0: warning: declaration 'half_baked' uses sorry
 42
 vm_sorry.lean:6:0: error: half_baked._main._val_1: trying to evaluate sorry
 vm_sorry.lean:12:0: error: undefined
 (some nat)
-vm_sorry.lean:18:8: warning: declaration '_example' uses sorry
-vm_sorry.lean:19:8: warning: declaration '_example' uses sorry
-vm_sorry.lean:20:8: warning: declaration '_example' uses sorry
+vm_sorry.lean:18:0: warning: declaration '[anonymous]' uses sorry
+vm_sorry.lean:19:0: warning: declaration '[anonymous]' uses sorry
+vm_sorry.lean:20:0: warning: declaration '[anonymous]' uses sorry