diff --git a/tests/lean/1207.lean.expected.out b/tests/lean/1207.lean.expected.out
index e7605b1966..0a75c18ac6 100644
--- a/tests/lean/1207.lean.expected.out
+++ b/tests/lean/1207.lean.expected.out
@@ -1,2 +1,15 @@
 1207.lean:15:2: error: unknown identifier 'h'
+1207.lean:15:2: error: don't know how to synthesize placeholder
+context:
+h : tactic unit,
+_example : true
+⊢ Type ?
+1207.lean:17:0: error: failed to add declaration '_interaction' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  …
 1207.lean:21:23: error: unknown identifier 'foo'
+1207.lean:21:23: error: don't know how to synthesize placeholder
+context:
+⊢ Type ?
+state:
+⊢ false
diff --git a/tests/lean/1290.lean.expected.out b/tests/lean/1290.lean.expected.out
index de648fdf09..adf5b20e95 100644
--- a/tests/lean/1290.lean.expected.out
+++ b/tests/lean/1290.lean.expected.out
@@ -1 +1,31 @@
 1290.lean:8:66: error: invalid declaration, '}' expected
+1290.lean:8:0: error: class expected, expression is not a constant
+1290.lean:8:61: error: don't know how to synthesize placeholder
+context:
+C : Category
+⊢ Sort ?
+1290.lean:8:63: error: don't know how to synthesize placeholder
+context:
+C : Category,
+A : ⁇
+⊢ Sort ?
+1290.lean:8:65: error: don't know how to synthesize placeholder
+context:
+C : Category,
+A : ⁇,
+B : ⁇
+⊢ Sort ?
+1290.lean:8:9: error: don't know how to synthesize placeholder
+context:
+C : Category,
+A : ⁇,
+B : ⁇,
+C : ⁇
+⊢ Sort ?
+1290.lean:8:9: error: don't know how to synthesize placeholder
+context:
+C : Category,
+A : ⁇,
+B : ⁇,
+C : ⁇
+⊢ Sort ?
diff --git a/tests/lean/1292.lean.expected.out b/tests/lean/1292.lean.expected.out
index 5fca1e3ef4..289b5a044a 100644
--- a/tests/lean/1292.lean.expected.out
+++ b/tests/lean/1292.lean.expected.out
@@ -1,2 +1,3 @@
 1292.lean:4:0: error: invalid expression, unexpected token
+1292.lean:2:0: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
 1292.lean:4:0: warning: using 'exit' to interrupt Lean
diff --git a/tests/lean/1293.lean.expected.out b/tests/lean/1293.lean.expected.out
index 2ff6293e51..73aa1b09fc 100644
--- a/tests/lean/1293.lean.expected.out
+++ b/tests/lean/1293.lean.expected.out
@@ -23,10 +23,10 @@ context:
 ⊢ Sort ?
 1293.lean:13:12: error: don't know how to synthesize placeholder
 context:
-foo : sorry
+foo : ⁇
 ⊢ Sort ?
 1293.lean:13:8: error: don't know how to synthesize placeholder
 context:
-foo : sorry,
-trivial : sorry
+foo : ⁇,
+trivial : ⁇
 ⊢ Sort ?
diff --git a/tests/lean/1299.lean.expected.out b/tests/lean/1299.lean.expected.out
index eec7a58a70..6ef86bd2ef 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 :=
-sorry
+⁇
diff --git a/tests/lean/bad_error1.lean.expected.out b/tests/lean/bad_error1.lean.expected.out
index 0d90e19eb6..05e95b2343 100644
--- a/tests/lean/bad_error1.lean.expected.out
+++ b/tests/lean/bad_error1.lean.expected.out
@@ -5,16 +5,16 @@ given argument
 expected argument
   m
 bad_error1.lean:4:22: error: unexpected argument at application
-  nat.bit1_ne_bit0 sorry m
+  nat.bit1_ne_bit0 n m
 given argument
   m
 expected argument
   n
 bad_error1.lean:4:13: error: type mismatch at application
-  ne.symm (nat.bit1_ne_bit0 sorry sorry)
+  ne.symm (nat.bit1_ne_bit0 n m)
 term
-  nat.bit1_ne_bit0 sorry sorry
+  nat.bit1_ne_bit0 n m
 has type
-  bit1 sorry ≠ bit0 sorry
+  bit1 n ≠ bit0 m
 but is expected to have type
   bit1 m ≠ bit0 n
diff --git a/tests/lean/bad_error3.lean.expected.out b/tests/lean/bad_error3.lean.expected.out
index 4c4ebcb3e8..ae6fa92935 100644
--- a/tests/lean/bad_error3.lean.expected.out
+++ b/tests/lean/bad_error3.lean.expected.out
@@ -3,10 +3,10 @@ bad_error3.lean:1:33: error: type expected at
 bad_error3.lean:3:0: error: tactic failed, there are unsolved goals
 state:
 p : ℕ → ℕ → Prop
-⊢ sorry
+⊢ ⁇
 bad_error3.lean:5:32: error: type expected at
   p 0
 bad_error3.lean:7:0: error: tactic failed, there are unsolved goals
 state:
 p : ℕ → ℕ → Prop
-⊢ sorry
+⊢ ⁇
diff --git a/tests/lean/bad_id.lean.expected.out b/tests/lean/bad_id.lean.expected.out
index 8742945dd1..2d5c6828b4 100644
--- a/tests/lean/bad_id.lean.expected.out
+++ b/tests/lean/bad_id.lean.expected.out
@@ -1 +1,5 @@
 bad_id.lean:5:12: error: invalid definition, '|' or ':=' expected
+bad_id.lean:5:11: error: don't know how to synthesize placeholder
+context:
+⊢ Sort ?
+bad_id.lean:5:12: error: command expected
diff --git a/tests/lean/bad_notation.lean.expected.out b/tests/lean/bad_notation.lean.expected.out
index 4a5c87283e..91858dfa53 100644
--- a/tests/lean/bad_notation.lean.expected.out
+++ b/tests/lean/bad_notation.lean.expected.out
@@ -1,2 +1,5 @@
 bad_notation.lean:6:23: error: invalid notation declaration, contains reference to local variables
 bad_notation.lean:9:18: error: unknown identifier 'a1'
+bad_notation.lean:9:11: error: don't know how to synthesize placeholder
+context:
+⊢ Sort ?
diff --git a/tests/lean/bad_open.lean.expected.out b/tests/lean/bad_open.lean.expected.out
index 50efe586ce..10f2607e19 100644
--- a/tests/lean/bad_open.lean.expected.out
+++ b/tests/lean/bad_open.lean.expected.out
@@ -1 +1,2 @@
 bad_open.lean:1:5: error: invalid 'open/export' command, identifier expected
+bad_open.lean:1:5: error: invalid namespace name '_'
diff --git a/tests/lean/bad_pattern2.lean.expected.out b/tests/lean/bad_pattern2.lean.expected.out
index 83b7aeab7c..c3e86a06bb 100644
--- a/tests/lean/bad_pattern2.lean.expected.out
+++ b/tests/lean/bad_pattern2.lean.expected.out
@@ -1 +1,11 @@
 bad_pattern2.lean:2:2: error: invalid pattern: variable, constructor or constant tagged as pattern expected
+bad_pattern2.lean:2:13: error: unknown identifier 'bla.boo'
+bad_pattern2.lean:2:2: error: type mismatch at application
+  foo bla.boo
+term
+  bla.boo
+has type
+  _
+but is expected to have type
+  ℕ
+bad_pattern2.lean:2:10: error: ill-formed match/equations expression
diff --git a/tests/lean/begin_end_bug.lean.expected.out b/tests/lean/begin_end_bug.lean.expected.out
index b06f669cc6..f39ab43182 100644
--- a/tests/lean/begin_end_bug.lean.expected.out
+++ b/tests/lean/begin_end_bug.lean.expected.out
@@ -1,2 +1,8 @@
 begin_end_bug.lean:3:24: error: unknown identifier 'a'
-begin_end_bug.lean:8:0: error: invalid 'end', there is no open namespace/section
+begin_end_bug.lean:3:18: error: don't know how to synthesize placeholder
+context:
+a b c : ℕ,
+hab : a = b,
+hac : a = c
+⊢ Type
+begin_end_bug.lean:3:48: error: _interaction._val_1: trying to evaluate sorry
diff --git a/tests/lean/crash.lean.expected.out b/tests/lean/crash.lean.expected.out
index 9bfd19e761..ab12244d47 100644
--- a/tests/lean/crash.lean.expected.out
+++ b/tests/lean/crash.lean.expected.out
@@ -10,9 +10,3 @@ P : Prop,
 H : P,
 H' : ¬P
 ⊢ Sort ?
-crash.lean:10:12: error: don't know how to synthesize placeholder
-context:
-P : Prop,
-H : P,
-H' : ¬P
-⊢ sorry
diff --git a/tests/lean/elab_error_recovery.lean.expected.out b/tests/lean/elab_error_recovery.lean.expected.out
index aa8127f7cb..6de0c17cdb 100644
--- a/tests/lean/elab_error_recovery.lean.expected.out
+++ b/tests/lean/elab_error_recovery.lean.expected.out
@@ -9,9 +9,6 @@ but is expected to have type
 elab_error_recovery.lean:8:13: error: failed to synthesize type class instance for
 half_baked : ℕ → ℕ
 ⊢ has_mem ℕ ℕ
-elab_error_recovery.lean:8:8: error: failed to synthesize type class instance for
-half_baked : ℕ → ℕ
-⊢ decidable (2 ∈ 3)
 elab_error_recovery.lean:10:11: error: don't know how to synthesize placeholder
 context:
 half_baked : ℕ → ℕ
@@ -38,9 +35,9 @@ half_baked : ℕ → ℕ
 def half_baked._main : ℕ → ℕ :=
 λ (a : ℕ),
   ite (a = 3) 2
-    (ite (a = 0) (1 + sorry) (ite (a = 5) (sorry + 4) (ite (a = 42) (ite (2 ∈ 3) 3 sorry) (ite (a = 7) sorry sorry))))
+    (ite (a = 0) (1 + ⁇) (ite (a = 5) (⁇ + 4) (ite (a = 42) (ite (2 ∈ 3) 3 ⁇) (ite (a = 7) ⁇ ⁇))))
 2
-nat.succ (nat.succ (nat.succ (nat.succ sorry)))
+nat.succ (nat.succ (nat.succ (nat.succ ⁇)))
 2
 elab_error_recovery.lean:21:13: error: type expected at
   0
diff --git a/tests/lean/emptyc_errors.lean.expected.out b/tests/lean/emptyc_errors.lean.expected.out
index 7dafbf312c..97ceedf3cc 100644
--- a/tests/lean/emptyc_errors.lean.expected.out
+++ b/tests/lean/emptyc_errors.lean.expected.out
@@ -8,11 +8,6 @@ context:
 A : Type u,
 x : A
 ⊢ Type ?
-emptyc_errors.lean:4:54: error: don't know how to synthesize placeholder
-context:
-A : Type u,
-x : A
-⊢ has_emptyc sorry
 emptyc_errors.lean:5:0: error: type mismatch, expression
   λ (h : x ∈ ∅), h
 has type
diff --git a/tests/lean/eqn_compiler_error_msg.lean.expected.out b/tests/lean/eqn_compiler_error_msg.lean.expected.out
index 87da101ec3..febe75ee50 100644
--- a/tests/lean/eqn_compiler_error_msg.lean.expected.out
+++ b/tests/lean/eqn_compiler_error_msg.lean.expected.out
@@ -1,3 +1,3 @@
 eqn_compiler_error_msg.lean:5:2: error: invalid function application in pattern, it cannot be reduced to a constructor (possible solution, mark term as inaccessible using '.( )')
   .p + .n
-eqn_compiler_error_msg.lean:5:28: error: ill-formed match/equations expression
+eqn_compiler_error_msg.lean:4:6: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
diff --git a/tests/lean/errors2.lean.expected.out b/tests/lean/errors2.lean.expected.out
index d18b595b9a..6aaddc7c5c 100644
--- a/tests/lean/errors2.lean.expected.out
+++ b/tests/lean/errors2.lean.expected.out
@@ -1 +1,2 @@
 errors2.lean:8:11: error: unknown identifier 'foo'
+errors2.lean:5:0: warning: declaration 'foo.tst1' uses sorry
diff --git a/tests/lean/inaccessible.lean.expected.out b/tests/lean/inaccessible.lean.expected.out
index 0e3c7c92ce..5185a7a4ee 100644
--- a/tests/lean/inaccessible.lean.expected.out
+++ b/tests/lean/inaccessible.lean.expected.out
@@ -1,20 +1,14 @@
 inaccessible.lean:14:10: error: function expected at
   mk
-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:14:4: error: invalid use of inaccessible term, it is not fixed by other arguments
 inaccessible.lean:17:12: error: invalid inaccessible annotation, it cannot be used around functions in applications
+inaccessible.lean:17:4: error: invalid use of inaccessible term, it is not fixed by other arguments
 inaccessible.lean:25:12: error: invalid pattern, 'a' already appeared in this pattern
+inaccessible.lean:25:3: error: function expected at
+  f
+inaccessible.lean:25:16: error: ill-formed match/equations expression
 inaccessible.lean:28:3: error: function expected at
   f
-inaccessible.lean:28:2: error: type mismatch at application
-  inv_7 sorry (mk b)
-term
-  mk b
-has type
-  imf .?m_3 (.?m_3 b)
-but is expected to have type
-  imf f sorry
 inaccessible.lean:28:16: error: ill-formed match/equations expression
 inaccessible.lean:31:4: error: invalid pattern, 'a' already appeared in this pattern
 inaccessible.lean:82:2: error: invalid use of inaccessible term, it is not completely fixed by other arguments
diff --git a/tests/lean/inaccessible2.lean.expected.out b/tests/lean/inaccessible2.lean.expected.out
index 3aec02af02..68473742f9 100644
--- a/tests/lean/inaccessible2.lean.expected.out
+++ b/tests/lean/inaccessible2.lean.expected.out
@@ -1,9 +1,7 @@
 inaccessible2.lean:5:8: error: invalid occurrence of 'inaccessible' annotation, it must only occur in patterns
-inaccessible2.lean:5:4: error: invalid use of inaccessible term, the provided term is
-  f sorry
-but is expected to be
-  f a
 inaccessible2.lean:8:10: error: invalid pattern, must be an application, constant, variable, type ascription or inaccessible term
+inaccessible2.lean:8:45: error: unknown identifier 'a'
+inaccessible2.lean:8:4: error: invalid use of inaccessible term, it is not fixed by other arguments
 inaccessible2.lean:11:39: error: inaccesible pattern notation `.(t)` can only be used in patterns
 inaccessible2.lean:14:13: error: invalid pattern, in a constructor application, the parameters of the inductive datatype must be marked as inaccessible
 inaccessible2.lean:14:24: error: ill-formed match/equations expression
diff --git a/tests/lean/interactive/complete_field.lean.expected.out b/tests/lean/interactive/complete_field.lean.expected.out
index 3bb6a96746..636b346abc 100644
--- a/tests/lean/interactive/complete_field.lean.expected.out
+++ b/tests/lean/interactive/complete_field.lean.expected.out
@@ -2,6 +2,7 @@
 {"msgs":[{"caption":"","file_name":"f","pos_col":14,"pos_line":4,"severity":"error","text":"invalid field 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 field 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 field 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 field 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 field 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 field 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 field 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 field 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":"identifier or numeral expected"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":14,"pos_line":4,"severity":"error","text":"invalid field 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 field 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 field 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":"identifier or numeral expected"},{"caption":"","file_name":"f","pos_col":14,"pos_line":16,"severity":"error","text":"invalid field notation, '_' is not a valid \"field\" because environment does not contain 'and._'\n  h y\nwhich has type\n  p y ∧ q y"}],"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":404},"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":404},"text":"left_comm","type":"?a ∧ ?b ∧ ?c ↔ ?b ∧ ?a ∧ ?c"}],"prefix":"le","response":"ok","seq_num":9}
diff --git a/tests/lean/interactive/complete_tactic.lean.expected.out b/tests/lean/interactive/complete_tactic.lean.expected.out
index 89e1e7deac..b6468e65c0 100644
--- a/tests/lean/interactive/complete_tactic.lean.expected.out
+++ b/tests/lean/interactive/complete_tactic.lean.expected.out
@@ -1,6 +1,9 @@
 {"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"}
+{"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"},{"caption":"","file_name":"f","pos_col":66,"pos_line":5,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Type ?"}],"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"},{"caption":"","file_name":"f","pos_col":66,"pos_line":5,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Type ?"},{"caption":"","file_name":"f","pos_col":66,"pos_line":5,"severity":"error","text":"failed to add declaration '_interaction' to environment, value has metavariables\nremark: set 'formatter.hide_full_terms' to false to see the complete term\n  …"}],"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"},{"caption":"","file_name":"f","pos_col":66,"pos_line":5,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Type ?"},{"caption":"","file_name":"f","pos_col":66,"pos_line":5,"severity":"error","text":"failed to add declaration '_interaction' to environment, value has metavariables\nremark: set 'formatter.hide_full_terms' to false to see the complete term\n  …"},{"caption":"","file_name":"f","pos_col":8,"pos_line":4,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"}],"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/correct_snapshot_invalidation.input.expected.out b/tests/lean/interactive/correct_snapshot_invalidation.input.expected.out
index 27542e4f01..748dd51c35 100644
--- a/tests/lean/interactive/correct_snapshot_invalidation.input.expected.out
+++ b/tests/lean/interactive/correct_snapshot_invalidation.input.expected.out
@@ -1,12 +1,17 @@
 {"message":"file invalidated","response":"ok","seq_num":0}
 {"message":"file invalidated","response":"ok","seq_num":1}
 {"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n  foo"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n  foo"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n  foo"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"invalid return type for 'foo.bar'"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":2}
-{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":3,"severity":"error","text":"unknown identifier 'd'"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"function expected at\n  foo"},{"caption":"","file_name":"f","pos_col":8,"pos_line":2,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"invalid return type for 'foo.bar'"}],"response":"all_messages"}
 {"msgs":[],"response":"all_messages"}
 {"msgs":[{"caption":"","file_name":"f","pos_col":3,"pos_line":3,"severity":"error","text":"invalid declaration, identifier expected"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":3,"pos_line":3,"severity":"error","text":"invalid declaration, identifier expected"},{"caption":"","file_name":"f","pos_col":3,"pos_line":3,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":3}
-{"msgs":[{"caption":"","file_name":"f","pos_col":3,"pos_line":3,"severity":"error","text":"invalid declaration, identifier expected"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":3,"pos_line":3,"severity":"error","text":"invalid declaration, identifier expected"},{"caption":"","file_name":"f","pos_col":3,"pos_line":3,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":3,"pos_line":3,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Sort ?"}],"response":"all_messages"}
 {"msgs":[],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":4}
 {"message":"file invalidated","response":"ok","seq_num":5}
diff --git a/tests/lean/interactive/field_info.lean.expected.out b/tests/lean/interactive/field_info.lean.expected.out
index 1eeec1c550..cfcdd0b0f0 100644
--- a/tests/lean/interactive/field_info.lean.expected.out
+++ b/tests/lean/interactive/field_info.lean.expected.out
@@ -1,6 +1,7 @@
 {"msgs":[{"caption":"","file_name":"f","pos_col":40,"pos_line":13,"severity":"error","text":"invalid expression, `)` expected"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":40,"pos_line":13,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"","file_name":"f","pos_col":0,"pos_line":12,"severity":"error","text":"don't know how to synthesize placeholder\ncontext:\n⊢ Type ?"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
 {"record":{"full-id":"nat.to_string","source":,"type":"ℕ → string"},"response":"ok","seq_num":2}
 {"record":{"full-id":"list.all","source":,"type":"Π {α : Type}, list α → (α → bool) → bool"},"response":"ok","seq_num":4}
 {"record":{"full-id":"list.all","source":,"type":"Π {α : Type}, list α → (α → bool) → bool"},"response":"ok","seq_num":9}
-{"record":{"full-id":"list.all","source":,"type":"Π {α : Type u}, list α → (α → bool) → bool"},"response":"ok","seq_num":13}
+{"record":{"full-id":"list.all","source":,"type":"Π {α : Type _elab_u.16.225}, list α → (α → bool) → bool"},"response":"ok","seq_num":13}
diff --git a/tests/lean/interactive/info_id_pre_elab.lean.expected.out b/tests/lean/interactive/info_id_pre_elab.lean.expected.out
index dd1d728c78..6bff823109 100644
--- a/tests/lean/interactive/info_id_pre_elab.lean.expected.out
+++ b/tests/lean/interactive/info_id_pre_elab.lean.expected.out
@@ -1,5 +1,7 @@
 {"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":6,"severity":"error","text":"invalid expression, `)` expected"}],"response":"all_messages"}
-{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":6,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"","file_name":"f","pos_col":27,"pos_line":7,"severity":"error","text":"invalid expression, `)` expected"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":6,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"","file_name":"f","pos_col":8,"pos_line":3,"severity":"error","text":"ambiguous overload, possible interpretations\n  trace\n  tactic.trace\nAdditional information:\nf:3:8: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":6,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"","file_name":"f","pos_col":8,"pos_line":3,"severity":"error","text":"ambiguous overload, possible interpretations\n  trace\n  tactic.trace\nAdditional information:\nf:3:8: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available"},{"caption":"","file_name":"f","pos_col":27,"pos_line":7,"severity":"error","text":"invalid expression, `)` expected"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":6,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"","file_name":"f","pos_col":8,"pos_line":3,"severity":"error","text":"ambiguous overload, possible interpretations\n  trace\n  tactic.trace\nAdditional information:\nf:3:8: context: switched to basic overload resolution where arguments are elaborated without any information about the expected type because expected type was not available"},{"caption":"","file_name":"f","pos_col":27,"pos_line":7,"severity":"error","text":"invalid expression, `)` expected"},{"caption":"check result","file_name":"f","pos_col":0,"pos_line":6,"severity":"information","text":"λ (tac : tactic unit), (abstract tac none) : tactic unit → tactic unit"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
 {"response":"ok","seq_num":4}
 {"record":{"full-id":"tactic.abstract","source":,"type":"tactic unit → opt_param (option name) none → opt_param bool tt → tactic unit"},"response":"ok","seq_num":7}
diff --git a/tests/lean/internal_names.lean.expected.out b/tests/lean/internal_names.lean.expected.out
index c69281a644..e7bb2af0f3 100644
--- a/tests/lean/internal_names.lean.expected.out
+++ b/tests/lean/internal_names.lean.expected.out
@@ -2,3 +2,4 @@ internal_names.lean:1:11: error: invalid declaration name '_foo', identifiers st
 internal_names.lean:3:10: error: invalid declaration name '_bla', identifiers starting with '_' are reserved to the system
 internal_names.lean:5:10: error: invalid declaration name '_empty', identifiers starting with '_' are reserved to the system
 internal_names.lean:7:10: error: invalid declaration name '_no', identifiers starting with '_' are reserved to the system
+internal_names.lean:7:13: error: invalid end of module, expecting 'end'
diff --git a/tests/lean/match_bug.lean.expected.out b/tests/lean/match_bug.lean.expected.out
index 25bd9ae537..3e579f72bd 100644
--- a/tests/lean/match_bug.lean.expected.out
+++ b/tests/lean/match_bug.lean.expected.out
@@ -1 +1,3 @@
 match_bug.lean:3:6: error: invalid pattern, must be an application, constant, variable, type ascription or inaccessible term
+match_bug.lean:3:12: error: invalid 'match' expression, ':=' expected
+match_bug.lean:2:0: error: equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)
diff --git a/tests/lean/private_structure.lean.expected.out b/tests/lean/private_structure.lean.expected.out
index 783cd33fd5..cada7bdeb0 100644
--- a/tests/lean/private_structure.lean.expected.out
+++ b/tests/lean/private_structure.lean.expected.out
@@ -8,13 +8,21 @@ point.x : point → ℕ
 point.y : point → ℕ
 bla : Type
 private_structure.lean:23:7: error: unknown identifier 'point'
+⁇ : ?M_1
 private_structure.lean:24:7: error: unknown identifier 'point.mk'
+⁇ : ?M_1
 private_structure.lean:25:7: error: unknown identifier 'point.rec'
+⁇ : ?M_1
 private_structure.lean:26:7: error: unknown identifier 'point.rec_on'
+⁇ : ?M_1
 private_structure.lean:27:7: error: unknown identifier 'point.cases_on'
+⁇ : ?M_1
 private_structure.lean:28:7: error: unknown identifier 'point.no_confusion'
+⁇ : ?M_1
 private_structure.lean:29:7: error: unknown identifier 'point.x'
+⁇ : ?M_1
 private_structure.lean:30:7: error: unknown identifier 'point.y'
+⁇ : ?M_1
 def foo.bla : Type :=
 point
 private_structure.lean:35:8: error: invalid constructor ⟨...⟩, type is a private inductive datatype
diff --git a/tests/lean/protected.lean.expected.out b/tests/lean/protected.lean.expected.out
index 628b2f6ece..319a53d5ca 100644
--- a/tests/lean/protected.lean.expected.out
+++ b/tests/lean/protected.lean.expected.out
@@ -1,2 +1,3 @@
 protected.lean:9:7: error: unknown identifier 'C'
+⁇ : ?M_1
 D : Prop
diff --git a/tests/lean/protected_consts.lean.expected.out b/tests/lean/protected_consts.lean.expected.out
index 08287b0600..2250397dda 100644
--- a/tests/lean/protected_consts.lean.expected.out
+++ b/tests/lean/protected_consts.lean.expected.out
@@ -1,15 +1,21 @@
 foo.A : Prop
 protected_consts.lean:14:7: error: unknown identifier 'A'
+⁇ : ?M_1
 foo.a : foo.A
 protected_consts.lean:16:7: error: unknown identifier 'a'
+⁇ : ?M_1
 foo.A₁ : Prop
 foo.A₂ : Prop
 protected_consts.lean:19:7: error: unknown identifier 'A₁'
+⁇ : ?M_1
 protected_consts.lean:20:7: error: unknown identifier 'A₂'
+⁇ : ?M_1
 foo.a₁ : foo.A
 foo.a₂ : foo.A
 protected_consts.lean:23:7: error: unknown identifier 'a₁'
+⁇ : ?M_1
 protected_consts.lean:24:7: error: unknown identifier 'a₂'
+⁇ : ?M_1
 B : Prop
 B : Prop
 b : B
diff --git a/tests/lean/protected_test.lean.expected.out b/tests/lean/protected_test.lean.expected.out
index d7159a0cfd..8e6d336d64 100644
--- a/tests/lean/protected_test.lean.expected.out
+++ b/tests/lean/protected_test.lean.expected.out
@@ -1,5 +1,7 @@
 protected_test.lean:2:9: error: unknown identifier 'induction_on'
+⁇ : ?M_1
 protected_test.lean:3:9: error: unknown identifier 'rec_on'
+⁇ : ?M_1
 less_than_or_equal.rec_on :
   less_than_or_equal ?M_1 ?M_3 →
   ?M_2 ?M_1 → (∀ {b : ℕ}, less_than_or_equal ?M_1 b → ?M_2 b → ?M_2 (succ b)) → ?M_2 ?M_3
@@ -7,6 +9,7 @@ less_than_or_equal.rec_on :
   less_than_or_equal ?M_1 ?M_3 →
   ?M_2 ?M_1 → (∀ {b : ℕ}, less_than_or_equal ?M_1 b → ?M_2 b → ?M_2 (succ b)) → ?M_2 ?M_3
 protected_test.lean:7:11: error: unknown identifier 'rec_on'
+⁇ : ?M_1
 less_than_or_equal.rec_on :
   less_than_or_equal ?M_1 ?M_3 →
   ?M_2 ?M_1 → (∀ {b : ℕ}, less_than_or_equal ?M_1 b → ?M_2 b → ?M_2 (succ b)) → ?M_2 ?M_3
diff --git a/tests/lean/record_rec_protected.lean.expected.out b/tests/lean/record_rec_protected.lean.expected.out
index 5ad63e0c1d..b31659cfa6 100644
--- a/tests/lean/record_rec_protected.lean.expected.out
+++ b/tests/lean/record_rec_protected.lean.expected.out
@@ -1 +1,2 @@
 record_rec_protected.lean:8:7: error: unknown identifier 'rec'
+⁇ : ?M_1
diff --git a/tests/lean/sec3.lean.expected.out b/tests/lean/sec3.lean.expected.out
index 07749811f8..1bee900b1f 100644
--- a/tests/lean/sec3.lean.expected.out
+++ b/tests/lean/sec3.lean.expected.out
@@ -1 +1,2 @@
 sec3.lean:5:9: error: invalid use of explicit universe parameter, identifier is a variable, parameter or a constant bound to parameters in a section
+tst : A → A
diff --git a/tests/lean/structure_instance_bug2.lean.expected.out b/tests/lean/structure_instance_bug2.lean.expected.out
index b4c3fe052c..4075881d58 100644
--- a/tests/lean/structure_instance_bug2.lean.expected.out
+++ b/tests/lean/structure_instance_bug2.lean.expected.out
@@ -1,2 +1,4 @@
 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:13:0: error: invalid structure update { src with ... }, field 'fst' was not provided, nor was it found in the source of type 'st'.
+structure_instance_bug2.lean:13:0: error: invalid structure update { src with ... }, field 'snd' was not provided, nor was it found in the source of type 'st'.
+structure_instance_bug2.lean:13:0: error: invalid structure value { ... }, 'i' is not a field of structure 'prod'
diff --git a/tests/lean/t12.lean.expected.out b/tests/lean/t12.lean.expected.out
index 8afbc19627..5f59b38a1f 100644
--- a/tests/lean/t12.lean.expected.out
+++ b/tests/lean/t12.lean.expected.out
@@ -1,2 +1,3 @@
 λ (f g : N → N → N) (x y : N), f x (g x y) : (N → N → N) → (N → N → N) → N → N → N
-t12.lean:7:8: error: invalid expression
+t12.lean:7:7: error: function expected at
+  a
diff --git a/tests/lean/t14.lean.expected.out b/tests/lean/t14.lean.expected.out
index ed667f6e60..385734148c 100644
--- a/tests/lean/t14.lean.expected.out
+++ b/tests/lean/t14.lean.expected.out
@@ -1,9 +1,11 @@
 b : A
 y : A
 t14.lean:12:9: error: unknown identifier 'c'
+⁇ : ?M_1
 a : foo.A
 x : foo.A
 t14.lean:19:9: error: unknown identifier 'c'
+⁇ : ?M_1
 t14.lean:23:26: error: invalid 'open/export' command option, mixing explicit and implicit 'open/export' options
 a : A
 c : A
diff --git a/tests/lean/t5.lean.expected.out b/tests/lean/t5.lean.expected.out
index 47bcf06573..d30b7d89de 100644
--- a/tests/lean/t5.lean.expected.out
+++ b/tests/lean/t5.lean.expected.out
@@ -3,3 +3,4 @@ h : N
 q : N
 foo.h : N
 t5.lean:13:7: error: unknown identifier 'q'
+⁇ : ?M_1