diff --git a/src/Init/Data/Ord.lean b/src/Init/Data/Ord.lean
index 83ff19025250..4d8ad8e498a5 100644
--- a/src/Init/Data/Ord.lean
+++ b/src/Init/Data/Ord.lean
@@ -59,6 +59,13 @@ instance : Ord USize where
 instance : Ord Char where
   compare x y := compareOfLessAndEq x y
 
+instance [Ord α] : Ord (Option α) where
+  compare
+    | .none, .none     => .eq
+    | .none, _         => .lt
+    | _    , .none     => .gt
+    | .some a, .some b => compare a b
+
 /-- The lexicographic order on pairs. -/
 def lexOrd [Ord α] [Ord β] : Ord (α × β) where
   compare p1 p2 := match compare p1.1 p2.1 with
diff --git a/src/Lean/Data/Position.lean b/src/Lean/Data/Position.lean
index 23bcbb6a5f67..6f876625654f 100644
--- a/src/Lean/Data/Position.lean
+++ b/src/Lean/Data/Position.lean
@@ -11,7 +11,7 @@ namespace Lean
 structure Position where
   line   : Nat
   column : Nat
-  deriving Inhabited, DecidableEq, Repr
+  deriving Inhabited, DecidableEq, Repr, Ord
 
 namespace Position
 protected def lt : Position → Position → Bool
diff --git a/src/Lean/Elab/Frontend.lean b/src/Lean/Elab/Frontend.lean
index 080687cae980..84235a207a8c 100644
--- a/src/Lean/Elab/Frontend.lean
+++ b/src/Lean/Elab/Frontend.lean
@@ -111,7 +111,7 @@ def runFrontend
     commandState := { commandState with infoState.enabled := true }
 
   let s ← IO.processCommands inputCtx parserState commandState
-  for msg in s.commandState.messages.toList do
+  for msg in s.commandState.messages do
     IO.print (← msg.toString (includeEndPos := getPrintMessageEndPos opts))
 
   if let some ileanFileName := ileanFileName? then
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index a738d781bc19..d1f12894a6e0 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -175,7 +175,7 @@ where
           -- We do not store `unsupportedSyntaxExceptionId`, see throwExs
           s.restore (restoreInfo := true); k failures
         else if id == abortTacticExceptionId then
-          for msg in (← Core.getMessageLog).toList do
+          for msg in (← Core.getMessageLog) do
             trace[Elab.tactic.backtrack] msg.data
           let failures := failures.push ⟨ex, ← Tactic.saveState⟩
           s.restore (restoreInfo := true); k failures
diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean
index 0c9ae5a452cb..5c0aafd2d604 100644
--- a/src/Lean/Message.lean
+++ b/src/Lean/Message.lean
@@ -265,11 +265,17 @@ def errorsToWarnings (log : MessageLog) : MessageLog :=
 def getInfoMessages (log : MessageLog) : MessageLog :=
   { msgs := log.msgs.filter fun m => match m.severity with | MessageSeverity.information => true | _ => false }
 
+/-- Returns all messages sorted by position. -/
+def toArray (log : MessageLog) : Array Message :=
+  let _ := @lexOrd
+  log.msgs.toArray.qsort fun m₁ m₂ =>
+    Ord.compare (m₁.fileName, m₁.pos, m₁.endPos) (m₂.fileName, m₂.pos, m₂.endPos) == .lt
+
 def forM {m : Type → Type} [Monad m] (log : MessageLog) (f : Message → m Unit) : m Unit :=
-  log.msgs.forM f
+  log.toArray.forM f
 
-def toList (log : MessageLog) : List Message :=
-  (log.msgs.foldl (fun acc msg => msg :: acc) []).reverse
+instance : ForIn m MessageLog Message where
+  forIn log := log.toArray.forIn
 
 end MessageLog
 
diff --git a/tests/lean/1018unknowMVarIssue.lean.expected.out b/tests/lean/1018unknowMVarIssue.lean.expected.out
index 459e030cf4be..90e7fb76de84 100644
--- a/tests/lean/1018unknowMVarIssue.lean.expected.out
+++ b/tests/lean/1018unknowMVarIssue.lean.expected.out
@@ -1,13 +1,6 @@
 [Elab.info] • command @ ⟨6, 0⟩-⟨6, 31⟩ @ Lean.Elab.Command.elabSetOption
       • [.] (Command.set_option "set_option" `trace.Elab.info) @ ⟨6, 0⟩-⟨6, 26⟩
       • option trace.Elab.info @ ⟨6, 11⟩-⟨6, 26⟩
-1018unknowMVarIssue.lean:9:18-9:19: error: don't know how to synthesize placeholder
-context:
-α✝ β : Type
-x : Fam2 α✝ β
-α : Type
-a : α
-⊢ α
 [Elab.info] • command @ ⟨7, 0⟩-⟨10, 19⟩ @ Lean.Elab.Command.elabDeclaration
       • α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
         • [.] α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩
@@ -80,4 +73,11 @@ a : α
           • [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
           • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
       • @_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩-⟨7, 7⟩
+1018unknowMVarIssue.lean:9:18-9:19: error: don't know how to synthesize placeholder
+context:
+α✝ β : Type
+x : Fam2 α✝ β
+α : Type
+a : α
+⊢ α
 [Elab.info] • command @ ⟨11, 0⟩-⟨11, 0⟩ @ Lean.Elab.Command.elabEoi
diff --git a/tests/lean/1026.lean.expected.out b/tests/lean/1026.lean.expected.out
index 93bfff8ecb73..6b075d7622c4 100644
--- a/tests/lean/1026.lean.expected.out
+++ b/tests/lean/1026.lean.expected.out
@@ -1,6 +1,6 @@
 1026.lean:1:4-1:7: warning: declaration uses 'sorry'
-1026.lean:10:2-10:12: warning: declaration uses 'sorry'
 1026.lean:9:8-9:10: warning: declaration uses 'sorry'
+1026.lean:10:2-10:12: warning: declaration uses 'sorry'
 foo._unfold (n : Nat) :
   foo n =
     if n = 0 then 0
diff --git a/tests/lean/1358.lean.expected.out b/tests/lean/1358.lean.expected.out
index 7bee343402be..0de3e061fa92 100644
--- a/tests/lean/1358.lean.expected.out
+++ b/tests/lean/1358.lean.expected.out
@@ -1,2 +1,2 @@
-foo
 1358.lean:9:2-9:8: error: error
+foo
diff --git a/tests/lean/1616.lean.expected.out b/tests/lean/1616.lean.expected.out
index 7f3cc26342ee..9376f31f0710 100644
--- a/tests/lean/1616.lean.expected.out
+++ b/tests/lean/1616.lean.expected.out
@@ -1,20 +1,15 @@
-1616.lean:9:23-9:39: error: don't know how to synthesize implicit argument
-  @Linear ?m (?m :: ?m) ?m (?m :: ?m) (Cover.left c)
-context:
-c : Cover ?m ?m ?m
-⊢ List ?m
-1616.lean:10:24-10:41: error: don't know how to synthesize implicit argument
-  @Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
+1616.lean:9:11-9:19: error: don't know how to synthesize implicit argument
+  @Linear ?m ?m ?m ?m c
 context:
 c : Cover ?m ?m ?m
 ⊢ Type u_1
-1616.lean:10:12-10:20: error: don't know how to synthesize implicit argument
-  @Linear ?m ?m ?m ?m c
+1616.lean:9:23-9:39: error: don't know how to synthesize implicit argument
+  @Linear ?m (?m :: ?m) ?m (?m :: ?m) (Cover.left c)
 context:
 c : Cover ?m ?m ?m
 ⊢ Type u_1
-1616.lean:10:24-10:41: error: don't know how to synthesize implicit argument
-  @Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
+1616.lean:9:23-9:39: error: don't know how to synthesize implicit argument
+  @Linear ?m (?m :: ?m) ?m (?m :: ?m) (Cover.left c)
 context:
 c : Cover ?m ?m ?m
 ⊢ List ?m
@@ -28,23 +23,28 @@ c : Cover ?m ?m ?m
 context:
 c : Cover ?m ?m ?m
 ⊢ Type u_1
+1616.lean:10:12-10:20: error: don't know how to synthesize implicit argument
+  @Linear ?m ?m ?m ?m c
+context:
+c : Cover ?m ?m ?m
+⊢ Type u_1
 1616.lean:10:24-10:41: error: don't know how to synthesize implicit argument
   @Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
 context:
 c : Cover ?m ?m ?m
-⊢ List ?m
-1616.lean:10:32-10:40: error: don't know how to synthesize implicit argument
-  @Cover.right ?m ?m ?m ?m ?m c
+⊢ Type u_1
+1616.lean:10:24-10:41: error: don't know how to synthesize implicit argument
+  @Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
 context:
 c : Cover ?m ?m ?m
-⊢ Type u_1
-1616.lean:9:11-9:19: error: don't know how to synthesize implicit argument
-  @Linear ?m ?m ?m ?m c
+⊢ List ?m
+1616.lean:10:24-10:41: error: don't know how to synthesize implicit argument
+  @Linear ?m ?m (?m :: ?m) (?m :: ?m) (Cover.right c)
 context:
 c : Cover ?m ?m ?m
-⊢ Type u_1
-1616.lean:9:23-9:39: error: don't know how to synthesize implicit argument
-  @Linear ?m (?m :: ?m) ?m (?m :: ?m) (Cover.left c)
+⊢ List ?m
+1616.lean:10:32-10:40: error: don't know how to synthesize implicit argument
+  @Cover.right ?m ?m ?m ?m ?m c
 context:
 c : Cover ?m ?m ?m
 ⊢ Type u_1
diff --git a/tests/lean/1719.lean.expected.out b/tests/lean/1719.lean.expected.out
index 15d27d9932b3..d0e30f450b7e 100644
--- a/tests/lean/1719.lean.expected.out
+++ b/tests/lean/1719.lean.expected.out
@@ -1,6 +1,6 @@
-1719.lean:2:8-2:12: error: invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant
-  ?m
 1719.lean:1:27-2:12: error: unsolved goals
 P Q : Prop
 h : P
 ⊢ P ∨ Q
+1719.lean:2:8-2:12: error: invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant
+  ?m
diff --git a/tests/lean/1781.lean.expected.out b/tests/lean/1781.lean.expected.out
index d862f4630071..b3078a9f94ec 100644
--- a/tests/lean/1781.lean.expected.out
+++ b/tests/lean/1781.lean.expected.out
@@ -3,5 +3,5 @@
 but it is expected to have type
   Type (imax 1 u)
 1781.lean:25:12-25:17: error: unknown identifier 'Univ''
-1781.lean:26:15-26:19: error: unknown identifier 'Univ'
 1781.lean:26:8-26:12: error: unknown identifier 'Univ'
+1781.lean:26:15-26:19: error: unknown identifier 'Univ'
diff --git a/tests/lean/2040.lean.expected.out b/tests/lean/2040.lean.expected.out
index 58cb3305ed5a..87675f0fed9c 100644
--- a/tests/lean/2040.lean.expected.out
+++ b/tests/lean/2040.lean.expected.out
@@ -2,11 +2,11 @@
   HPow Nat Nat Int
 2040.lean:9:8-9:13: error: failed to synthesize instance
   HPow Nat Nat Int
-2040.lean:15:8-15:13: error: failed to synthesize instance
-  HPow Nat Nat Int
 2040.lean:13:2-15:22: error: type mismatch
   trans (sorryAx (a = 37)) (sorryAx (37 = 2 ^ n))
 has type
   a = @OfNat.ofNat Nat 2 (instOfNatNat 2) ^ n : Prop
 but is expected to have type
   a = @OfNat.ofNat Int 2 instOfNatInt ^ n : Prop
+2040.lean:15:8-15:13: error: failed to synthesize instance
+  HPow Nat Nat Int
diff --git a/tests/lean/255.lean.expected.out b/tests/lean/255.lean.expected.out
index b163a7dcb813..2edd8b2aa429 100644
--- a/tests/lean/255.lean.expected.out
+++ b/tests/lean/255.lean.expected.out
@@ -1,6 +1,6 @@
 A : α
 id x✝ : α
+id (sorryAx ?m true) : ?m
 255.lean:16:7-16:8: error: unknown constant 'x✝'
 id (sorryAx ?m true) : ?m
 255.lean:20:9-20:10: error: unknown constant 'x✝'
-id (sorryAx ?m true) : ?m
diff --git a/tests/lean/276.lean.expected.out b/tests/lean/276.lean.expected.out
index cb778a59bf8f..a6f760a5768f 100644
--- a/tests/lean/276.lean.expected.out
+++ b/tests/lean/276.lean.expected.out
@@ -1,3 +1,3 @@
-276.lean:5:27-5:50: error: failed to elaborate eliminator, expected type is not available
 fun {α : Sort v} => @?m α : {α : Sort v} → @?m α
+276.lean:5:27-5:50: error: failed to elaborate eliminator, expected type is not available
 276.lean:9:32-9:55: error: failed to elaborate eliminator, expected type is not available
diff --git a/tests/lean/277a.lean.expected.out b/tests/lean/277a.lean.expected.out
index 6e15b41861bc..357b3ae6856a 100644
--- a/tests/lean/277a.lean.expected.out
+++ b/tests/lean/277a.lean.expected.out
@@ -1,2 +1,2 @@
-277a.lean:4:7-4:15: error: unknown identifier 'nonexistant'
 277a.lean:4:0-4:25: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
+277a.lean:4:7-4:15: error: unknown identifier 'nonexistant'
diff --git a/tests/lean/277b.lean.expected.out b/tests/lean/277b.lean.expected.out
index 3abe48b75b36..5b94333e292e 100644
--- a/tests/lean/277b.lean.expected.out
+++ b/tests/lean/277b.lean.expected.out
@@ -1,3 +1,3 @@
+277b.lean:8:0-8:16: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
 277b.lean:8:10-8:16: error: invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor 
   List Point
-277b.lean:8:0-8:16: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
diff --git a/tests/lean/343.lean.expected.out b/tests/lean/343.lean.expected.out
index b6c0daaf99b7..abc8ec027311 100644
--- a/tests/lean/343.lean.expected.out
+++ b/tests/lean/343.lean.expected.out
@@ -1,13 +1,13 @@
 343.lean:24:4-24:24: warning: declaration uses 'sorry'
-343.lean:30:0-30:54: error: stuck at solving universe constraint
-  max (?u+1) (?u+1) =?= max (?u+1) (?u+1)
-while trying to unify
-  Catish.Obj Catish.Obj
-with
-  CatIsh.{max ?u ?u, max (?u + 1) (?u + 1)}
 343.lean:30:0-30:54: error: failed to solve universe constraint
   max (?u+1) (?u+1) =?= max (?u+1) (?u+1)
 while trying to unify
   Catish.Obj : Type (max ((max (u_1 + 1) (u_2 + 1)) + 1) ((max u_3 u_4) + 1))
 with
   CatIsh : Type (max ((max u_4 u_3) + 1) ((max (u_4 + 1) (u_3 + 1)) + 1))
+343.lean:30:0-30:54: error: stuck at solving universe constraint
+  max (?u+1) (?u+1) =?= max (?u+1) (?u+1)
+while trying to unify
+  Catish.Obj Catish.Obj
+with
+  CatIsh.{max ?u ?u, max (?u + 1) (?u + 1)}
diff --git a/tests/lean/361.lean.expected.out b/tests/lean/361.lean.expected.out
index 18ab15f98c04..339afd975e0f 100644
--- a/tests/lean/361.lean.expected.out
+++ b/tests/lean/361.lean.expected.out
@@ -1,18 +1,18 @@
-361.lean:3:0: error: expected '{' or tactic
 361.lean:1:60-1:62: error: unsolved goals
 p q r : Prop
 h1 : p ∨ q
 h2 : p → q
 ⊢ q
-361.lean:6:0: error: unexpected end of input; expected '{'
-361.lean:5:11-5:13: error: unsolved goals
-p q r : Prop
-h2 : p → q
-h✝ : p
-⊢ q
+361.lean:3:0: error: expected '{' or tactic
 361.lean:3:60-5:13: error: unsolved goals
 case inr
 p q r : Prop
 h2 : p → q
 h✝ : q
 ⊢ q
+361.lean:5:11-5:13: error: unsolved goals
+p q r : Prop
+h2 : p → q
+h✝ : p
+⊢ q
+361.lean:6:0: error: unexpected end of input; expected '{'
diff --git a/tests/lean/439.lean.expected.out b/tests/lean/439.lean.expected.out
index 3a5aeae62c8b..58f01f44ae42 100644
--- a/tests/lean/439.lean.expected.out
+++ b/tests/lean/439.lean.expected.out
@@ -9,6 +9,7 @@ term has type
   Bar.fn ?m
 Fn.imp fn : Bar.fn p
 Fn.imp fn' Bp : Bar.fn p
+Fn.imp fn' (sorryAx (Bar.fn ?m) true) : Bar.fn ?m
 439.lean:39:11-39:12: error: application type mismatch
   Fn.imp fn' p
 argument
@@ -17,4 +18,3 @@ has type
   P : Sort u
 but is expected to have type
   Bar.fn ?m : Sort ?u
-Fn.imp fn' (sorryAx (Bar.fn ?m) true) : Bar.fn ?m
diff --git a/tests/lean/450.lean.expected.out b/tests/lean/450.lean.expected.out
index 8017fe9571ca..2ba2013d9e7f 100644
--- a/tests/lean/450.lean.expected.out
+++ b/tests/lean/450.lean.expected.out
@@ -1,4 +1,4 @@
+450.lean:2:6-2:7: error: failed to infer 'let' declaration type
 450.lean:2:11-2:12: error: don't know how to synthesize placeholder
 context:
 ⊢ ?m
-450.lean:2:6-2:7: error: failed to infer 'let' declaration type
diff --git a/tests/lean/586.lean.expected.out b/tests/lean/586.lean.expected.out
index 4ff6ac93cd6d..b397d03837c4 100644
--- a/tests/lean/586.lean.expected.out
+++ b/tests/lean/586.lean.expected.out
@@ -1,4 +1,4 @@
-Nat.zero : Nat
 `Nat.succ : Lean.Name
-586.lean:13:0-13:3: error: unknown identifier 'zero✝'
+Nat.zero : Nat
 586.lean:13:0-13:3: error: unknown constant 'succ✝'
+586.lean:13:0-13:3: error: unknown identifier 'zero✝'
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index 685d3a2f8825..7403cbdb5c09 100644
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/tests/lean/StxQuot.lean.expected.out
@@ -43,8 +43,8 @@ StxQuot.lean:19:15: error: expected term
 "(Term.sufficesDecl\n (hygieneInfo `_@.UnhygienicMain._hyg.1)\n `x._@.UnhygienicMain._hyg.1\n (Term.fromTerm \"from\" `x._@.UnhygienicMain._hyg.1))"
 "#[(num \"1\"), [(num \"2\") (num \"3\")], (num \"4\")]"
 "#[(num \"2\")]"
-StxQuot.lean:95:39-95:44: error: unexpected antiquotation splice
 fun x => sorryAx (?m x) true : (x : ?m) → ?m x
+StxQuot.lean:95:39-95:44: error: unexpected antiquotation splice
 "#[(some 1), (some 2)]"
 StxQuot.lean:102:13-102:14: error: unknown identifier 'x' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check.
 "`id._@.UnhygienicMain._hyg.1"
diff --git a/tests/lean/argNameAtPlaceholderError.lean.expected.out b/tests/lean/argNameAtPlaceholderError.lean.expected.out
index d955d184eb0d..54d2d16f9b7d 100644
--- a/tests/lean/argNameAtPlaceholderError.lean.expected.out
+++ b/tests/lean/argNameAtPlaceholderError.lean.expected.out
@@ -1,3 +1,7 @@
+argNameAtPlaceholderError.lean:8:11-8:12: error: don't know how to synthesize placeholder for argument 'stx'
+context:
+stx : Syntax
+⊢ Syntax
 argNameAtPlaceholderError.lean:8:13-8:14: error: don't know how to synthesize placeholder for argument 'expectedType?'
 context:
 stx : Syntax
@@ -6,7 +10,3 @@ argNameAtPlaceholderError.lean:8:15-8:16: error: don't know how to synthesize pl
 context:
 stx : Syntax
 ⊢ Bool
-argNameAtPlaceholderError.lean:8:11-8:12: error: don't know how to synthesize placeholder for argument 'stx'
-context:
-stx : Syntax
-⊢ Syntax
diff --git a/tests/lean/byStrictIndent.lean.expected.out b/tests/lean/byStrictIndent.lean.expected.out
index 6765b63fc3ca..8bf0b9fb82c6 100644
--- a/tests/lean/byStrictIndent.lean.expected.out
+++ b/tests/lean/byStrictIndent.lean.expected.out
@@ -1,15 +1,15 @@
 theorem byTopLevelNoIndent : ∀ (n : Nat), n > 1 → n > 1 :=
 fun n h => h
-byStrictIndent.lean:12:2: error: expected '{' or indented tactic sequence
-byStrictIndent.lean:11:25-11:27: error: unsolved goals
+byStrictIndent.lean:10:62-11:27: error: unsolved goals
 n : Nat
 h : n > 0
+helper : n > 1
 ⊢ n > 1
-byStrictIndent.lean:10:62-11:27: error: unsolved goals
+byStrictIndent.lean:11:25-11:27: error: unsolved goals
 n : Nat
 h : n > 0
-helper : n > 1
 ⊢ n > 1
+byStrictIndent.lean:12:2: error: expected '{' or indented tactic sequence
 byStrictIndent.lean:16:54-18:9: error: unsolved goals
 n : Nat
 h : n > 0
diff --git a/tests/lean/defInst.lean.expected.out b/tests/lean/defInst.lean.expected.out
index 126cd16e2cab..09f39fb6f42d 100644
--- a/tests/lean/defInst.lean.expected.out
+++ b/tests/lean/defInst.lean.expected.out
@@ -1,7 +1,7 @@
 [4, 5, 6]
+fun x y => sorryAx (?m x y) true : (x y : Foo) → ?m x y
 defInst.lean:8:26-8:32: error: failed to synthesize instance
   BEq Foo
-fun x y => sorryAx (?m x y) true : (x y : Foo) → ?m x y
 [4, 5, 6]
 fun x y => x == y : Foo → Foo → Bool
 [("hello", "hello")]
diff --git a/tests/lean/deprecated.lean.expected.out b/tests/lean/deprecated.lean.expected.out
index 40a428f3d456..2474ddf713b1 100644
--- a/tests/lean/deprecated.lean.expected.out
+++ b/tests/lean/deprecated.lean.expected.out
@@ -1,11 +1,11 @@
-deprecated.lean:11:6-11:7: warning: `f` has been deprecated, use `g` instead
 2
-deprecated.lean:13:6-13:7: warning: `h` has been deprecated
+deprecated.lean:11:6-11:7: warning: `f` has been deprecated, use `g` instead
 1
+deprecated.lean:13:6-13:7: warning: `h` has been deprecated
 deprecated.lean:15:13-15:15: error: unknown constant 'g1'
 deprecated.lean:23:13-23:15: error: unknown constant 'g1'
+2
 deprecated.lean:30:6-30:8: warning: `f2` has been deprecated, use `Foo.g1` instead
 2
 2
 deprecated.lean:33:6-33:8: warning: `f4` has been deprecated, use `Foo.g1` instead
-2
diff --git a/tests/lean/doLetLoop.lean.expected.out b/tests/lean/doLetLoop.lean.expected.out
index d7d4ca528253..517fda802079 100644
--- a/tests/lean/doLetLoop.lean.expected.out
+++ b/tests/lean/doLetLoop.lean.expected.out
@@ -1,2 +1,2 @@
-doLetLoop.lean:4:0: error: unexpected end of input
 doLetLoop.lean:2:4-2:5: warning: declaration uses 'sorry'
+doLetLoop.lean:4:0: error: unexpected end of input
diff --git a/tests/lean/doNotation1.lean.expected.out b/tests/lean/doNotation1.lean.expected.out
index 2986c334d144..892d2eaa93b7 100644
--- a/tests/lean/doNotation1.lean.expected.out
+++ b/tests/lean/doNotation1.lean.expected.out
@@ -5,14 +5,14 @@ doNotation1.lean:20:7-20:22: error: invalid reassignment, value has type
   Vector Nat (n + 1) : Type
 but is expected to have type
   Vector Nat n : Type
-doNotation1.lean:25:7-25:11: error: invalid reassignment, value has type
-  Bool : Type
-but is expected to have type
-  Nat : Type
 doNotation1.lean:24:0-25:11: error: type mismatch, `for` has type
   PUnit : Sort ?u
 but is expected to have type
   List Bool : Type
+doNotation1.lean:25:7-25:11: error: invalid reassignment, value has type
+  Bool : Type
+but is expected to have type
+  Nat : Type
 doNotation1.lean:28:0-29:14: error: type mismatch, `for` has type
   PUnit : Sort ?u
 but is expected to have type
diff --git a/tests/lean/doSeqRightIssue.lean.expected.out b/tests/lean/doSeqRightIssue.lean.expected.out
index 405f86ef10e3..14de2baf0791 100644
--- a/tests/lean/doSeqRightIssue.lean.expected.out
+++ b/tests/lean/doSeqRightIssue.lean.expected.out
@@ -1,3 +1,3 @@
 doSeqRightIssue.lean:5:23-5:24: error: unknown universe level 'v'
-doSeqRightIssue.lean:8:0-9:40: warning: declaration uses 'sorry'
 doSeqRightIssue.lean:7:8-7:10: warning: declaration uses 'sorry'
+doSeqRightIssue.lean:8:0-9:40: warning: declaration uses 'sorry'
diff --git a/tests/lean/evalNone.lean.expected.out b/tests/lean/evalNone.lean.expected.out
index 7fdcd9ce11cd..f5abf4e7dc43 100644
--- a/tests/lean/evalNone.lean.expected.out
+++ b/tests/lean/evalNone.lean.expected.out
@@ -2,11 +2,11 @@ evalNone.lean:1:6-1:10: error: don't know how to synthesize implicit argument
   @none ?m
 context:
 ⊢ Type ?u
-evalNone.lean:3:6-3:14: error: don't know how to synthesize implicit argument
-  @List.head? ?m []
-context:
-⊢ Type ?u
 evalNone.lean:3:6-3:8: error: don't know how to synthesize implicit argument
   @List.nil ?m
 context:
 ⊢ Type ?u
+evalNone.lean:3:6-3:14: error: don't know how to synthesize implicit argument
+  @List.head? ?m []
+context:
+⊢ Type ?u
diff --git a/tests/lean/evalWithMVar.lean.expected.out b/tests/lean/evalWithMVar.lean.expected.out
index 350971fecd15..388f412569c7 100644
--- a/tests/lean/evalWithMVar.lean.expected.out
+++ b/tests/lean/evalWithMVar.lean.expected.out
@@ -1,11 +1,11 @@
 Sum.someRight c : Option Nat
-evalWithMVar.lean:13:20-13:21: error: don't know how to synthesize implicit argument
-  @c ?m
-context:
-⊢ Type ?u
 evalWithMVar.lean:13:6-13:21: error: don't know how to synthesize implicit argument
   @Sum.someRight ?m Nat c
 context:
 ⊢ Type ?u
+evalWithMVar.lean:13:20-13:21: error: don't know how to synthesize implicit argument
+  @c ?m
+context:
+⊢ Type ?u
 Sum.someRight c : Option Nat
 Sum.someRight c : Option Nat
diff --git a/tests/lean/exactErrorPos.lean.expected.out b/tests/lean/exactErrorPos.lean.expected.out
index 0f8b632f9e62..2be85883fd9a 100644
--- a/tests/lean/exactErrorPos.lean.expected.out
+++ b/tests/lean/exactErrorPos.lean.expected.out
@@ -1,3 +1,9 @@
+exactErrorPos.lean:3:99-4:14: error: unsolved goals
+f : Nat → Nat
+x : Nat
+h1 : ∀ (x : Nat), x > 0 → f x = x
+h2 : x > 0
+⊢ f x = x
 exactErrorPos.lean:4:13-4:14: error: don't know how to synthesize placeholder
 context:
 f : Nat → Nat
@@ -5,7 +11,7 @@ x : Nat
 h1 : ∀ (x : Nat), x > 0 → f x = x
 h2 : x > 0
 ⊢ x > 0
-exactErrorPos.lean:3:99-4:14: error: unsolved goals
+exactErrorPos.lean:6:99-7:15: error: unsolved goals
 f : Nat → Nat
 x : Nat
 h1 : ∀ (x : Nat), x > 0 → f x = x
@@ -18,7 +24,7 @@ x : Nat
 h1 : ∀ (x : Nat), x > 0 → f x = x
 h2 : x > 0
 ⊢ x > 0
-exactErrorPos.lean:6:99-7:15: error: unsolved goals
+exactErrorPos.lean:21:99-23:12: error: unsolved goals
 f : Nat → Nat
 x : Nat
 h1 : ∀ (x : Nat), x > 0 → f x = x
@@ -31,9 +37,3 @@ x : Nat
 h1 : ∀ (x : Nat), x > 0 → f x = x
 h2 : x > 0
 ⊢ x > 0
-exactErrorPos.lean:21:99-23:12: error: unsolved goals
-f : Nat → Nat
-x : Nat
-h1 : ∀ (x : Nat), x > 0 → f x = x
-h2 : x > 0
-⊢ f x = x
diff --git a/tests/lean/funParen.lean.expected.out b/tests/lean/funParen.lean.expected.out
index ff14986b4a4e..6e49c4cbd4aa 100644
--- a/tests/lean/funParen.lean.expected.out
+++ b/tests/lean/funParen.lean.expected.out
@@ -1,4 +1,4 @@
 fun α [Repr α] => repr : (α : Type u_1) → [inst : Repr α] → α → Std.Format
 fun x y => x : (x : ?m) → ?m x → ?m
-funParen.lean:4:12-4:16: error: invalid pattern, constructor or constant marked with '[match_pattern]' expected
 fun x => ?m x : (x : ?m) → ?m x
+funParen.lean:4:12-4:16: error: invalid pattern, constructor or constant marked with '[match_pattern]' expected
diff --git a/tests/lean/have.lean.expected.out b/tests/lean/have.lean.expected.out
index 2265fae1b7b4..83f2f22a62e0 100644
--- a/tests/lean/have.lean.expected.out
+++ b/tests/lean/have.lean.expected.out
@@ -1,7 +1,7 @@
-have.lean:4:0: error: expected term
 have.lean:2:18-2:19: error: don't know how to synthesize placeholder
 context:
 ⊢ False
+have.lean:4:0: error: expected term
 have.lean:7:2-7:3: error: type mismatch
   f
 has type
diff --git a/tests/lean/hidingInaccessibleNames.lean.expected.out b/tests/lean/hidingInaccessibleNames.lean.expected.out
index 929513dea211..9084951f7286 100644
--- a/tests/lean/hidingInaccessibleNames.lean.expected.out
+++ b/tests/lean/hidingInaccessibleNames.lean.expected.out
@@ -1,34 +1,34 @@
-hidingInaccessibleNames.lean:4:15-4:16: error: don't know how to synthesize placeholder
+hidingInaccessibleNames.lean:2:16-2:17: error: don't know how to synthesize placeholder
 context:
-x✝² : List Nat
 x✝¹ : Nat
-x✝ : x✝² ≠ []
+x✝ : [] ≠ []
 ⊢ Nat
 hidingInaccessibleNames.lean:3:19-3:20: error: don't know how to synthesize placeholder
 context:
 a b x✝¹ : Nat
 x✝ : [a, b] ≠ []
 ⊢ Nat
-hidingInaccessibleNames.lean:2:16-2:17: error: don't know how to synthesize placeholder
+hidingInaccessibleNames.lean:4:15-4:16: error: don't know how to synthesize placeholder
 context:
+x✝² : List Nat
 x✝¹ : Nat
-x✝ : [] ≠ []
+x✝ : x✝² ≠ []
 ⊢ Nat
-hidingInaccessibleNames.lean:10:16-10:17: error: don't know how to synthesize placeholder
+hidingInaccessibleNames.lean:8:16-8:17: error: don't know how to synthesize placeholder
 context:
-x✝² : List Nat
 x✝¹ : Nat
-x✝ : x✝² ≠ []
+x✝ : [] ≠ []
 ⊢ Nat
 hidingInaccessibleNames.lean:9:19-9:20: error: don't know how to synthesize placeholder
 context:
 a b x✝¹ : Nat
 x✝ : [a, b] ≠ []
 ⊢ Nat
-hidingInaccessibleNames.lean:8:16-8:17: error: don't know how to synthesize placeholder
+hidingInaccessibleNames.lean:10:16-10:17: error: don't know how to synthesize placeholder
 context:
+x✝² : List Nat
 x✝¹ : Nat
-x✝ : [] ≠ []
+x✝ : x✝² ≠ []
 ⊢ Nat
 case inl
 p q : Prop
diff --git a/tests/lean/holeErrors.lean.expected.out b/tests/lean/holeErrors.lean.expected.out
index 0fe3920070d3..d013d61cbda3 100644
--- a/tests/lean/holeErrors.lean.expected.out
+++ b/tests/lean/holeErrors.lean.expected.out
@@ -5,18 +5,18 @@ context:
 ⊢ Sort u
 holeErrors.lean:5:9-5:10: error: failed to infer definition type
 when the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed
+holeErrors.lean:7:11-9:1: error: failed to infer definition type
+holeErrors.lean:8:4-8:5: error: failed to infer 'let' declaration type
 holeErrors.lean:8:9-8:15: error: don't know how to synthesize implicit argument
   @id ?m
 context:
 ⊢ Sort u
-holeErrors.lean:7:11-9:1: error: failed to infer definition type
-holeErrors.lean:8:4-8:5: error: failed to infer 'let' declaration type
-holeErrors.lean:11:11-11:15: error: failed to infer definition type
 holeErrors.lean:11:8-11:9: error: failed to infer binder type
+holeErrors.lean:11:11-11:15: error: failed to infer definition type
 holeErrors.lean:13:12-13:13: error: failed to infer binder type
 holeErrors.lean:13:15-13:19: error: failed to infer definition type
-holeErrors.lean:16:4-16:5: error: failed to infer binder type
 holeErrors.lean:15:7-16:10: error: failed to infer definition type
+holeErrors.lean:16:4-16:5: error: failed to infer binder type
 holeErrors.lean:19:8-19:9: error: failed to infer 'let rec' declaration type
 holeErrors.lean:19:13-19:19: error: don't know how to synthesize implicit argument
   @id ?m
diff --git a/tests/lean/holes.lean.expected.out b/tests/lean/holes.lean.expected.out
index 7829fec90dae..e23ec92dd485 100644
--- a/tests/lean/holes.lean.expected.out
+++ b/tests/lean/holes.lean.expected.out
@@ -1,22 +1,22 @@
 holes.lean:4:4-4:7: error: placeholders '_' cannot be used where a function is expected
-holes.lean:10:15-10:18: error: don't know how to synthesize implicit argument
+holes.lean:10:9-10:12: error: don't know how to synthesize implicit argument
   @g Nat (?m x) x
 context:
 x : Nat
 ⊢ Type
-holes.lean:10:9-10:12: error: don't know how to synthesize implicit argument
+holes.lean:10:15-10:18: error: don't know how to synthesize implicit argument
   @g Nat (?m x) x
 context:
 x : Nat
 ⊢ Type
-holes.lean:11:8-11:13: error: don't know how to synthesize placeholder
+holes.lean:11:4-11:5: error: don't know how to synthesize placeholder
 context:
-case hole
 x : Nat
 y : Nat := g x + g x
 ⊢ Nat
-holes.lean:11:4-11:5: error: don't know how to synthesize placeholder
+holes.lean:11:8-11:13: error: don't know how to synthesize placeholder
 context:
+case hole
 x : Nat
 y : Nat := g x + g x
 ⊢ Nat
diff --git a/tests/lean/implicitTypePos.lean.expected.out b/tests/lean/implicitTypePos.lean.expected.out
index 67464413a8dc..7491818549cd 100644
--- a/tests/lean/implicitTypePos.lean.expected.out
+++ b/tests/lean/implicitTypePos.lean.expected.out
@@ -1,5 +1,5 @@
-implicitTypePos.lean:1:8-1:9: error: failed to infer binder type
 implicitTypePos.lean:1:6-1:7: error: failed to infer binder type
+implicitTypePos.lean:1:8-1:9: error: failed to infer binder type
 implicitTypePos.lean:3:9-3:10: error: failed to infer binder type
 implicitTypePos.lean:5:9-5:10: error: failed to infer binder type
 implicitTypePos.lean:7:10-7:11: error: failed to infer binder type
diff --git a/tests/lean/jason1.lean.expected.out b/tests/lean/jason1.lean.expected.out
index dc2115268018..054dbfa87aee 100644
--- a/tests/lean/jason1.lean.expected.out
+++ b/tests/lean/jason1.lean.expected.out
@@ -1,9 +1,19 @@
-jason1.lean:48:119-48:124: error: don't know how to synthesize implicit argument
-  @EGrfl
-    (getCtx
-      (TAlgebra
-        (@TySyntaxLayer.nat G T EG getCtx
-          (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
+jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
+context:
+G T Tm : Type
+EG : G → G → Type
+ET : T → T → Type
+ETm : Tm → Tm → Type
+EGrfl : {Γ : G} → EG Γ Γ
+getCtx : T → G
+getTy : Tm → T
+GAlgebra : CtxSyntaxLayer G T EG getCtx → G
+TAlgebra : TySyntaxLayer G T EG getCtx → T
+Γ✝ : G
+⊢ G
+jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
 context:
 G T Tm : Type
 EG : G → G → Type
@@ -48,8 +58,8 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
 TAlgebra : TySyntaxLayer G T EG getCtx → T
 Γ✝ : G
 ⊢ G
-jason1.lean:46:40-46:57: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.top G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
+jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
+  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
 context:
 G T Tm : Type
 EG : G → G → Type
@@ -62,7 +72,7 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
 TAlgebra : TySyntaxLayer G T EG getCtx → T
 Γ✝ : G
 ⊢ G
-jason1.lean:48:71-48:88: error: don't know how to synthesize implicit argument
+jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
   @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
 context:
 G T Tm : Type
@@ -76,7 +86,7 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
 TAlgebra : TySyntaxLayer G T EG getCtx → T
 Γ✝ : G
 ⊢ G
-jason1.lean:48:125-48:130: error: don't know how to synthesize implicit argument
+jason1.lean:48:119-48:124: error: don't know how to synthesize implicit argument
   @EGrfl
     (getCtx
       (TAlgebra
@@ -94,22 +104,12 @@ GAlgebra : CtxSyntaxLayer G T EG getCtx → G
 TAlgebra : TySyntaxLayer G T EG getCtx → T
 Γ✝ : G
 ⊢ G
-jason1.lean:47:40-47:57: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
-context:
-G T Tm : Type
-EG : G → G → Type
-ET : T → T → Type
-ETm : Tm → Tm → Type
-EGrfl : {Γ : G} → EG Γ Γ
-getCtx : T → G
-getTy : Tm → T
-GAlgebra : CtxSyntaxLayer G T EG getCtx → G
-TAlgebra : TySyntaxLayer G T EG getCtx → T
-Γ✝ : G
-⊢ G
-jason1.lean:48:100-48:117: error: don't know how to synthesize implicit argument
-  @TySyntaxLayer.nat G T EG getCtx (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝)
+jason1.lean:48:125-48:130: error: don't know how to synthesize implicit argument
+  @EGrfl
+    (getCtx
+      (TAlgebra
+        (@TySyntaxLayer.nat G T EG getCtx
+          (?m G T Tm EG ET ETm EGrfl getCtx getTy GAlgebra TAlgebra getTyStep Γ✝))))
 context:
 G T Tm : Type
 EG : G → G → Type
diff --git a/tests/lean/jason2.lean.expected.out b/tests/lean/jason2.lean.expected.out
index 20d01eabe552..4ecd1be01fdc 100644
--- a/tests/lean/jason2.lean.expected.out
+++ b/tests/lean/jason2.lean.expected.out
@@ -1,8 +1,8 @@
-jason2.lean:4:30-4:37: error: don't know how to synthesize implicit argument
-  @Foo.foo ?m
-context:
-⊢ Nat
 jason2.lean:4:20-4:23: error: don't know how to synthesize implicit argument
   @Foo ?m
 context:
 ⊢ Nat
+jason2.lean:4:30-4:37: error: don't know how to synthesize implicit argument
+  @Foo.foo ?m
+context:
+⊢ Nat
diff --git a/tests/lean/linterUnusedVariables.lean.expected.out b/tests/lean/linterUnusedVariables.lean.expected.out
index b55d1ad6a2ae..539fb6815af6 100644
--- a/tests/lean/linterUnusedVariables.lean.expected.out
+++ b/tests/lean/linterUnusedVariables.lean.expected.out
@@ -38,7 +38,6 @@ a : Nat
 ⊢ Nat
 linterUnusedVariables.lean:227:0-227:7: warning: declaration uses 'sorry'
 linterUnusedVariables.lean:228:0-228:7: warning: declaration uses 'sorry'
-linterUnusedVariables.lean:231:0: error: expected '{' or tactic
 linterUnusedVariables.lean:229:27-229:29: error: unsolved goals
 bar : ?m
 bar' : Nat → Nat
@@ -47,3 +46,4 @@ bar' : Nat → Nat
 inst : ToString α
 a : Nat
 ⊢ Nat
+linterUnusedVariables.lean:231:0: error: expected '{' or tactic
diff --git a/tests/lean/longestParsePrio.lean.expected.out b/tests/lean/longestParsePrio.lean.expected.out
index 27680942ff5a..7c9a6edd06e6 100644
--- a/tests/lean/longestParsePrio.lean.expected.out
+++ b/tests/lean/longestParsePrio.lean.expected.out
@@ -1,4 +1,4 @@
-longestParsePrio.lean:4:0: error: unexpected end of input; expected ']'
 longestParsePrio.lean:2:19-3:26: error: unsolved goals
 this : True
 ⊢ False
+longestParsePrio.lean:4:0: error: unexpected end of input; expected ']'
diff --git a/tests/lean/macroSwizzle.lean.expected.out b/tests/lean/macroSwizzle.lean.expected.out
index d45ec0f9ccbc..0764efcb9801 100644
--- a/tests/lean/macroSwizzle.lean.expected.out
+++ b/tests/lean/macroSwizzle.lean.expected.out
@@ -1,5 +1,6 @@
 macroSwizzle.lean:4:7-4:23: error: failed to synthesize instance
   HAdd Bool String ?m
+Nat.succ (sorryAx Nat true) : Nat
 macroSwizzle.lean:6:7-6:10: error: application type mismatch
   Nat.succ "x"
 argument
@@ -8,4 +9,3 @@ has type
   String : Type
 but is expected to have type
   Nat : Type
-Nat.succ (sorryAx Nat true) : Nat
diff --git a/tests/lean/macroTrace.lean.expected.out b/tests/lean/macroTrace.lean.expected.out
index e1157c16b98c..d3ac2fa8b9bd 100644
--- a/tests/lean/macroTrace.lean.expected.out
+++ b/tests/lean/macroTrace.lean.expected.out
@@ -2,5 +2,5 @@
 0 : Nat
 [Meta.debug] macro tst executed
 hello
-hello
 [Meta.debug] macro cmdtst executed 3
+hello
diff --git a/tests/lean/match1.lean.expected.out b/tests/lean/match1.lean.expected.out
index ec02890f188b..70ad006f227f 100644
--- a/tests/lean/match1.lean.expected.out
+++ b/tests/lean/match1.lean.expected.out
@@ -19,9 +19,9 @@ match1.lean:119:0-119:41: error: dependent match elimination failed, inaccessibl
   .(j + j)
 constructor expected
 [false, true, true]
+fun x => ?m x : ?m × ?m → ?m
 match1.lean:136:7-136:22: error: invalid match-expression, type of pattern variable 'a' contains metavariables
   ?m
-fun x => ?m x : ?m × ?m → ?m
 fun x =>
   match x with
   | (a, b) => a + b : Nat × Nat → Nat
diff --git a/tests/lean/multiConstantError.lean.expected.out b/tests/lean/multiConstantError.lean.expected.out
index 4fe617b40f64..ec62b813ad89 100644
--- a/tests/lean/multiConstantError.lean.expected.out
+++ b/tests/lean/multiConstantError.lean.expected.out
@@ -1,6 +1,6 @@
-multiConstantError.lean:1:11-1:12: error: failed to infer binder type
-recall that you cannot declare multiple constants in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`
 multiConstantError.lean:1:9-1:10: error: failed to infer binder type
 recall that you cannot declare multiple constants in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`
+multiConstantError.lean:1:11-1:12: error: failed to infer binder type
+recall that you cannot declare multiple constants in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`
 multiConstantError.lean:3:9-3:10: error: failed to infer binder type
 recall that you cannot declare multiple constants in a single declaration. The identifier(s) `α`, `β` are being interpreted as parameters `(α : _)`, `(β : _)`
diff --git a/tests/lean/nameArgErrorIssue.lean.expected.out b/tests/lean/nameArgErrorIssue.lean.expected.out
index 80768a757305..e59884eaf187 100644
--- a/tests/lean/nameArgErrorIssue.lean.expected.out
+++ b/tests/lean/nameArgErrorIssue.lean.expected.out
@@ -1,4 +1,5 @@
 bla 5 2 : Nat
+bla (sorryAx Nat true) 5 : Nat
 nameArgErrorIssue.lean:5:20-5:24: error: application type mismatch
   bla "hi"
 argument
@@ -7,7 +8,7 @@ has type
   String : Type
 but is expected to have type
   Nat : Type
-bla (sorryAx Nat true) 5 : Nat
+nameArgErrorIssue.lean:6:11-6:19: error: invalid argument name 'z' for function 'bla'
 nameArgErrorIssue.lean:6:20-6:24: error: application type mismatch
   bla "hi"
 argument
@@ -16,5 +17,4 @@ has type
   String : Type
 but is expected to have type
   Nat : Type
-nameArgErrorIssue.lean:6:11-6:19: error: invalid argument name 'z' for function 'bla'
 nameArgErrorIssue.lean:7:11-7:19: error: invalid argument name 'z' for function 'bla'
diff --git a/tests/lean/namedHoles.lean.expected.out b/tests/lean/namedHoles.lean.expected.out
index 626a786aea8b..998006005e82 100644
--- a/tests/lean/namedHoles.lean.expected.out
+++ b/tests/lean/namedHoles.lean.expected.out
@@ -1,3 +1,4 @@
+f ?x (sorryAx Bool true) : Nat
 namedHoles.lean:9:12-9:14: error: application type mismatch
   f ?x ?x
 argument
@@ -6,13 +7,12 @@ has type
   Nat : Type
 but is expected to have type
   Bool : Type
-f ?x (sorryAx Bool true) : Nat
 g ?x ?x : Nat
 20
 foo (fun x => ?m x) ?hole : Nat
 bla ?hole fun x => ?hole : Nat
-namedHoles.lean:35:38-35:43: error: synthetic hole has already been defined with an incompatible local context
 boo (fun x => ?m x) fun y => sorryAx Nat true : Nat
+namedHoles.lean:35:38-35:43: error: synthetic hole has already been defined with an incompatible local context
 11
 12
 namedHoles.lean:58:26-58:31: error: synthetic hole has already been defined and assigned to value incompatible with the current context
diff --git a/tests/lean/noTabs.lean.expected.out b/tests/lean/noTabs.lean.expected.out
index 9e301c50810f..b0c8618d1604 100644
--- a/tests/lean/noTabs.lean.expected.out
+++ b/tests/lean/noTabs.lean.expected.out
@@ -1,3 +1,3 @@
-noTabs.lean:3:0: error: tabs are not allowed; please configure your editor to expand them
 let a := 1;
 sorryAx ?m true : ?m
+noTabs.lean:3:0: error: tabs are not allowed; please configure your editor to expand them
diff --git a/tests/lean/phashmap_inst_coherence.lean.expected.out b/tests/lean/phashmap_inst_coherence.lean.expected.out
index 201a304788b9..a8049b077fa9 100644
--- a/tests/lean/phashmap_inst_coherence.lean.expected.out
+++ b/tests/lean/phashmap_inst_coherence.lean.expected.out
@@ -1,3 +1,4 @@
+phashmap_inst_coherence.lean:12:0-12:56: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
 phashmap_inst_coherence.lean:12:53-12:54: error: application type mismatch
   PersistentHashMap.find? m
 argument
@@ -6,4 +7,3 @@ has type
   @PersistentHashMap Nat Nat instBEqNat instHashableNat : Type
 but is expected to have type
   @PersistentHashMap Nat Nat instBEqNat natDiffHash : Type
-phashmap_inst_coherence.lean:12:0-12:56: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
diff --git a/tests/lean/run/termParserAttr.lean b/tests/lean/run/termParserAttr.lean
index aa63738d01fa..35de3d74e237 100644
--- a/tests/lean/run/termParserAttr.lean
+++ b/tests/lean/run/termParserAttr.lean
@@ -7,7 +7,7 @@ def runCore (input : String) (failIff : Bool := true) : CoreM Unit := do
 let env  ← getEnv;
 let opts ← getOptions;
 let (env, messages) ← process input env opts;
-messages.toList.forM fun msg => do IO.println (← msg.toString)
+messages.forM fun msg => do IO.println (← msg.toString)
 if failIff && messages.hasErrors then throwError "errors have been found";
 if !failIff && !messages.hasErrors then throwError "there are no errors";
 pure ()
diff --git a/tests/lean/scientific.lean.expected.out b/tests/lean/scientific.lean.expected.out
index 28b77df7e339..b3d41ea54881 100644
--- a/tests/lean/scientific.lean.expected.out
+++ b/tests/lean/scientific.lean.expected.out
@@ -14,17 +14,17 @@ scientific.lean:15:6-15:7: error: invalid occurrence of `·` notation, it must b
 scientific.lean:15:7: error: expected command
 scientific.lean:16:6-16:7: error: invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`)
 scientific.lean:16:7: error: expected command
-scientific.lean:19:6-19:7: error: unknown identifier 'e'
 scientific.lean:19:0-19:9: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
+scientific.lean:19:6-19:7: error: unknown identifier 'e'
 scientific.lean:20:9: error: missing exponent digits in scientific literal
 scientific.lean:21:9: error: missing exponent digits in scientific literal
 scientific.lean:22:9: error: missing exponent digits in scientific literal
 scientific.lean:23:9: error: missing exponent digits in scientific literal
 scientific.lean:24:9: error: missing exponent digits in scientific literal
 scientific.lean:25:9: error: missing exponent digits in scientific literal
+scientific.lean:26:0-26:11: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
 scientific.lean:26:6-26:8: error: invalid dotted identifier notation, unknown identifier `Nat.E` from expected type
   Nat
-scientific.lean:26:0-26:11: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
-scientific.lean:27:7-27:9: error: unknown identifier 'E3'
 scientific.lean:27:0-27:9: error: cannot evaluate code because '_eval._lambda_1' uses 'sorry' and/or contains errors
+scientific.lean:27:7-27:9: error: unknown identifier 'E3'
 scientific.lean:28:7: error: missing exponent digits in scientific literal
diff --git a/tests/lean/scopedMacros.lean.expected.out b/tests/lean/scopedMacros.lean.expected.out
index a5fd1a7919e0..7de772c487d5 100644
--- a/tests/lean/scopedMacros.lean.expected.out
+++ b/tests/lean/scopedMacros.lean.expected.out
@@ -1,8 +1,8 @@
 10 + 1 : Nat
 scopedMacros.lean:11:7-11:11: error: unknown identifier 'foo!'
 10 + 1 : Nat
-scopedMacros.lean:19:7-19:50: error: scoped attributes must be used inside namespaces
 scopedMacros.lean:19:7-19:50: error: invalid syntax node kind 'termBla!_'
+scopedMacros.lean:19:7-19:50: error: scoped attributes must be used inside namespaces
 scopedMacros.lean:29:7-29:11: error: unknown identifier 'bla!'
 scopedMacros.lean:36:7-36:45: error: scoped attributes must be used inside namespaces
 10 + 20 : Nat
diff --git a/tests/lean/scopedunifhint.lean.expected.out b/tests/lean/scopedunifhint.lean.expected.out
index 5b4accc6104b..e73e479b763b 100644
--- a/tests/lean/scopedunifhint.lean.expected.out
+++ b/tests/lean/scopedunifhint.lean.expected.out
@@ -1,3 +1,4 @@
+mul (sorryAx ?m.α true) (sorryAx ?m.α true) : ?m.α
 scopedunifhint.lean:28:11-28:12: error: application type mismatch
   mul x
 argument
@@ -15,7 +16,7 @@ has type
   Nat × Nat : Type
 but is expected to have type
   ?m.α : Type ?u
-mul (sorryAx ?m.α true) (sorryAx ?m.α true) : ?m.α
+sorryAx ?m.α true*sorryAx ?m.α true : ?m.α
 scopedunifhint.lean:33:7-33:8: error: application type mismatch
   mul x
 argument
@@ -24,9 +25,9 @@ has type
   Nat : Type
 but is expected to have type
   ?m.α : Type ?u
-sorryAx ?m.α true*sorryAx ?m.α true : ?m.α
 x*x : Nat.Magma.α
 x*x : Nat.Magma.α
+sorryAx ?m.α true*sorryAx ?m.α true : ?m.α
 scopedunifhint.lean:39:11-39:17: error: application type mismatch
   mul (x, x)
 argument
@@ -35,8 +36,8 @@ has type
   Nat × Nat : Type
 but is expected to have type
   ?m.α : Type ?u
-sorryAx ?m.α true*sorryAx ?m.α true : ?m.α
 (x, x)*(x, x) : (Prod.Magma Nat.Magma Nat.Magma).α
+sorryAx ?m.α true*sorryAx ?m.α true : ?m.α
 scopedunifhint.lean:56:7-56:13: error: application type mismatch
   mul (x, x)
 argument
@@ -45,4 +46,3 @@ has type
   Nat × Nat : Type
 but is expected to have type
   ?m.α : Type ?u
-sorryAx ?m.α true*sorryAx ?m.α true : ?m.α
diff --git a/tests/lean/simp_trace.lean.expected.out b/tests/lean/simp_trace.lean.expected.out
index 01aa203e80e9..a3b3e2aab886 100644
--- a/tests/lean/simp_trace.lean.expected.out
+++ b/tests/lean/simp_trace.lean.expected.out
@@ -55,7 +55,7 @@ Try this: simp only [and_self]
 Try this: simp only [my_thm]
 [Meta.Tactic.simp.rewrite] @my_thm:1000, b ∧ b ==> b
 [Meta.Tactic.simp.rewrite] @eq_self:1000, (a ∧ b) = (a ∧ b) ==> True
-Try this: simp (discharger := sorry) only [Nat.sub_add_cancel]
 simp_trace.lean:83:0-83:7: warning: declaration uses 'sorry'
+Try this: simp (discharger := sorry) only [Nat.sub_add_cancel]
 [Meta.Tactic.simp.rewrite] @Nat.sub_add_cancel:1000, x - 1 + 1 ==> x
 [Meta.Tactic.simp.rewrite] @eq_self:1000, x = x ==> True
diff --git a/tests/lean/struct1.lean.expected.out b/tests/lean/struct1.lean.expected.out
index 1c39faa61b14..37d265bfac91 100644
--- a/tests/lean/struct1.lean.expected.out
+++ b/tests/lean/struct1.lean.expected.out
@@ -1,10 +1,10 @@
 struct1.lean:9:14-9:17: error: expected Type
 struct1.lean:12:20-12:29: error: expected structure
-struct1.lean:15:28-15:34: warning: field 'x' from 'A' has already been declared
 struct1.lean:15:28-15:34: error: parent field type mismatch, field 'x' from parent 'A' has type
   Bool : Type
 but is expected to have type
   Nat : Type
+struct1.lean:15:28-15:34: warning: field 'x' from 'A' has already been declared
 struct1.lean:18:27-18:33: error: parent field type mismatch, field 'x' from parent 'B' has type
   Bool : Type
 but is expected to have type
diff --git a/tests/lean/substBadMotive.lean.expected.out b/tests/lean/substBadMotive.lean.expected.out
index c546538db5af..27d787f4189f 100644
--- a/tests/lean/substBadMotive.lean.expected.out
+++ b/tests/lean/substBadMotive.lean.expected.out
@@ -1,5 +1,5 @@
 substBadMotive.lean:7:4-7:16: warning: declaration uses 'sorry'
 substBadMotive.lean:9:23-9:44: error: invalid `▸` notation, failed to compute motive for the substitution
-substBadMotive.lean:15:22-15:43: error: invalid `▸` notation, failed to compute motive for the substitution
 substBadMotive.lean:13:0-17:24: error: well-founded recursion cannot be used, 'Ex3.heapifyDown' does not take any (non-fixed) arguments
+substBadMotive.lean:15:22-15:43: error: invalid `▸` notation, failed to compute motive for the substitution
 substBadMotive.lean:34:30-34:53: error: invalid `▸` notation, failed to compute motive for the substitution
diff --git a/tests/lean/unknownTactic.lean.expected.out b/tests/lean/unknownTactic.lean.expected.out
index a80599a3117c..31130a171eb0 100644
--- a/tests/lean/unknownTactic.lean.expected.out
+++ b/tests/lean/unknownTactic.lean.expected.out
@@ -1,15 +1,15 @@
-unknownTactic.lean:3:3: error: unknown tactic
 unknownTactic.lean:1:41-3:8: error: unsolved goals
 x : Nat
 a✝ : x = x
 ⊢ x = x
+unknownTactic.lean:3:3: error: unknown tactic
 ---
-unknownTactic.lean:8:22: error: unknown tactic
 unknownTactic.lean:8:18-8:24: error: unsolved goals
 x : Nat
 ⊢ x = x
+unknownTactic.lean:8:22: error: unknown tactic
 ---
-unknownTactic.lean:14:22: error: unknown tactic
 unknownTactic.lean:14:18-14:24: error: unsolved goals
 x : Nat
 ⊢ x = x
+unknownTactic.lean:14:22: error: unknown tactic
diff --git a/tests/lean/warningAsError.lean.expected.out b/tests/lean/warningAsError.lean.expected.out
index 648ec65610fd..0e64d6b648d4 100644
--- a/tests/lean/warningAsError.lean.expected.out
+++ b/tests/lean/warningAsError.lean.expected.out
@@ -1,5 +1,5 @@
+1
 warningAsError.lean:8:6-8:7: warning: `g` has been deprecated, use `f` instead
 1
 warningAsError.lean:12:6-12:7: error: `g` has been deprecated, use `f` instead
-1
 warningAsError.lean:15:7-15:13: error: unused variable `unused` [linter.unusedVariables]
diff --git a/tests/playground/termParserAttr.lean b/tests/playground/termParserAttr.lean
deleted file mode 100644
index 648e585fd423..000000000000
--- a/tests/playground/termParserAttr.lean
+++ /dev/null
@@ -1,36 +0,0 @@
-import Lean
-open Lean
-open Lean.Elab
-
-def run (input : String) (failIff : Bool := true) : MetaIO Unit :=
-do env  ← MetaIO.getEnv;
-   opts ← MetaIO.getOptions;
-   let (env, messages) := process input env opts;
-   messages.toList.forM $ fun msg => IO.println msg;
-   when (failIff && messages.hasErrors) $ throw (IO.userError "errors have been found");
-   when (!failIff && !messages.hasErrors) $ throw (IO.userError "there are no errors");
-   pure ()
-
-open Lean.Parser
-@[term_parser] def tst := parser! "(|" >> term_parser >> "|)"
-
-@[term_parser] def boo : ParserDescr :=
-ParserDescr.node `boo
-  (ParserDescr.andthen
-    (ParserDescr.symbol "[|" 0)
-    (ParserDescr.andthen
-      (ParserDescr.parser `term 0)
-      (ParserDescr.symbol "|]" 0)))
-
-open Lean.Elab.Term
-
-@[term_elab tst] def elabTst : TermElab :=
-fun stx expected? =>
-  elabTerm (stx.getArg 1) expected?
-
-@[term_elab boo] def elabBoo : TermElab :=
-fun stx expected? =>
-  elabTerm (stx.getArg 1) expected?
-
-#eval run "#check [| @id.{1} Nat |]"
-#eval run "#check (| id 1 |)"