leanprover · Kha · Jul 19, 2023
@@ -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
@@ -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
@@ -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

@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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'