chore: fix tests

leanprover · Aug 8, 2022 · f722465 · f722465
1 parent cf994f8
commit f722465
Show file tree

Hide file tree

Showing 19 changed files with 388 additions and 312 deletions.
diff --git a/tests/lean/1018unknowMVarIssue.lean.expected.out b/tests/lean/1018unknowMVarIssue.lean.expected.out
@@ -1,5 +1,5 @@
 [Elab.info] command @ ⟨6, 0⟩-⟨6, 31⟩ @ Lean.Elab.Command.elabSetOption
-  [.] (Command.set_option "set_option" `trace.Elab.info) @ ⟨6, 0⟩-⟨6, 26⟩
+      [.] (Command.set_option "set_option" `trace.Elab.info) @ ⟨6, 0⟩-⟨6, 26⟩
 1018unknowMVarIssue.lean:9:18-9:19: error: don't know how to synthesize placeholder
 context:
 α✝ β : Type
@@ -8,68 +8,68 @@ x : Fam2 α✝ β
 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⟩
-    α : Type @ ⟨7, 13⟩-⟨7, 14⟩
-  a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
-  α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
-    [.] `α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩
-    α : Type @ ⟨7, 13⟩-⟨7, 14⟩
-  a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
-  Fam2 α β : Type 1 @ ⟨7, 21⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabApp
-    [.] `Fam2 : some Sort.{?_uniq} @ ⟨7, 21⟩-⟨7, 25⟩
-    Fam2 : Type → Type → Type 1 @ ⟨7, 21⟩-⟨7, 25⟩
-    α : Type @ ⟨7, 26⟩-⟨7, 27⟩ @ Lean.Elab.Term.elabIdent
-      [.] `α : some Type @ ⟨7, 26⟩-⟨7, 27⟩
-      α : Type @ ⟨7, 26⟩-⟨7, 27⟩
-    β : Type @ ⟨7, 28⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabIdent
-      [.] `β : some Type @ ⟨7, 28⟩-⟨7, 29⟩
-      β : Type @ ⟨7, 28⟩-⟨7, 29⟩
-  x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
-  β : Type @ ⟨7, 33⟩-⟨7, 34⟩ @ Lean.Elab.Term.elabIdent
-    [.] `β : some Sort.{?_uniq} @ ⟨7, 33⟩-⟨7, 34⟩
-    β : Type @ ⟨7, 33⟩-⟨7, 34⟩
-  _example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩†-⟨10, 19⟩†
-  a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
-  x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
-  _example.match_1 (fun α β x a => β) α β x a (fun α_1 a => ?m x α_1 a) fun n a =>
-    n : <failed-to-infer-type> @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch
-    x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
-    [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
-    [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
-    @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
-    [.] `Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
-    Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
-    [.] `n : none @ ⟨10, 13⟩-⟨10, 14⟩
-    [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
-    [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
-    @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
-    [.] `a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
-    [.] `Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨9, 4⟩-⟨9, 12⟩
-    [.] `a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
-    α (isBinder := true) : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-    α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-    Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
-      α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
-    a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-    FVarAlias _uniq.669 -> _uniq.327
-    FVarAlias _uniq.668 -> _uniq.325
-    ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
-    [.] `Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
-    Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
-    [.] `n : none @ ⟨10, 13⟩-⟨10, 14⟩
-    [.] `a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
-    [.] `Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨10, 4⟩-⟨10, 12⟩
-    [.] `n : some Nat @ ⟨10, 13⟩-⟨10, 14⟩
-    [.] `a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
-    Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-    Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
-    Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
-      n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
-    a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
-    FVarAlias _uniq.700 -> _uniq.327
-    FVarAlias _uniq.699 -> _uniq.325
-    n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
-      [.] `n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
-      n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
-  @_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩-⟨7, 7⟩
+      α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
+        [.] `α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩
+        α : Type @ ⟨7, 13⟩-⟨7, 14⟩
+      a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
+      α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent
+        [.] `α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩
+        α : Type @ ⟨7, 13⟩-⟨7, 14⟩
+      a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
+      Fam2 α β : Type 1 @ ⟨7, 21⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabApp
+        [.] `Fam2 : some Sort.{?_uniq} @ ⟨7, 21⟩-⟨7, 25⟩
+        Fam2 : Type → Type → Type 1 @ ⟨7, 21⟩-⟨7, 25⟩
+        α : Type @ ⟨7, 26⟩-⟨7, 27⟩ @ Lean.Elab.Term.elabIdent
+          [.] `α : some Type @ ⟨7, 26⟩-⟨7, 27⟩
+          α : Type @ ⟨7, 26⟩-⟨7, 27⟩
+        β : Type @ ⟨7, 28⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabIdent
+          [.] `β : some Type @ ⟨7, 28⟩-⟨7, 29⟩
+          β : Type @ ⟨7, 28⟩-⟨7, 29⟩
+      x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
+      β : Type @ ⟨7, 33⟩-⟨7, 34⟩ @ Lean.Elab.Term.elabIdent
+        [.] `β : some Sort.{?_uniq} @ ⟨7, 33⟩-⟨7, 34⟩
+        β : Type @ ⟨7, 33⟩-⟨7, 34⟩
+      _example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩†-⟨10, 19⟩†
+      a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩
+      x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩
+      _example.match_1 (fun α β x a => β) α β x a (fun α_1 a => ?m x α_1 a) fun n a =>
+        n : <failed-to-infer-type> @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch
+        x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩
+        [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
+        [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
+        @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
+        [.] `Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
+        Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
+        [.] `n : none @ ⟨10, 13⟩-⟨10, 14⟩
+        [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
+        [.] `Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩
+        @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩
+        [.] `a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
+        [.] `Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨9, 4⟩-⟨9, 12⟩
+        [.] `a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
+        α (isBinder := true) : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+        α : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+        Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
+          α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
+        a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
+        FVarAlias _uniq.669 -> _uniq.327
+        FVarAlias _uniq.668 -> _uniq.325
+        ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
+        [.] `Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
+        Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
+        [.] `n : none @ ⟨10, 13⟩-⟨10, 14⟩
+        [.] `a : none @ ⟨8, 2⟩†-⟨10, 19⟩†
+        [.] `Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨10, 4⟩-⟨10, 12⟩
+        [.] `n : some Nat @ ⟨10, 13⟩-⟨10, 14⟩
+        [.] `a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩†
+        Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+        Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩†
+        Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
+          n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
+        a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
+        FVarAlias _uniq.700 -> _uniq.327
+        FVarAlias _uniq.699 -> _uniq.325
+        n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
+          [.] `n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
+          n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
+      @_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩-⟨7, 7⟩
diff --git a/tests/lean/1079.lean b/tests/lean/1079.lean
@@ -2,7 +2,7 @@ theorem bad : ∀ (m n : Nat), (if m = n then Ordering.eq else Ordering.gt) = Or
   intros m n
   cases (Nat.decEq m n) with -- an error as expected: "alternative `isFalse` has not bee provided"
   | isTrue h =>
-    set_option trace.Meta.Tactic true in
+    set_option trace.Meta.Tactic.simp true in
     simp [h]
 
 theorem bad' : ∀ (m n : Nat), (if m = n then Ordering.eq else Ordering.gt) = Ordering.lt → False := by

diff --git a/tests/lean/1079.lean.expected.out b/tests/lean/1079.lean.expected.out
@@ -2,12 +2,12 @@
 [Meta.Tactic.simp.rewrite] h:1000, m ==> n
 [Meta.Tactic.simp.rewrite] eq_self:1000, n = n ==> True
 [Meta.Tactic.simp.unify] ite_self:1000, failed to unify
-  if ?c then ?a else ?a
-with
-  if True then Ordering.eq else Ordering.gt
+      if ?c then ?a else ?a
+    with
+      if True then Ordering.eq else Ordering.gt
 [Meta.Tactic.simp.rewrite] ite_true:1000, if True then Ordering.eq else Ordering.gt ==> Ordering.eq
 [Meta.Tactic.simp.unify] eq_self:1000, failed to unify
-  ?a = ?a
-with
-  Ordering.eq = Ordering.lt
+      ?a = ?a
+    with
+      Ordering.eq = Ordering.lt
 [Meta.Tactic.simp.rewrite] false_implies:1000, False → False ==> True
diff --git a/tests/lean/366.lean.expected.out b/tests/lean/366.lean.expected.out
@@ -1,12 +1,6 @@
-[Meta.synthInstance] preprocess: Inhabited Nat ==> Inhabited Nat
-  [Meta.synthInstance] 
-    [Meta.synthInstance] main goal Inhabited Nat
-    [Meta.synthInstance.newSubgoal] Inhabited Nat
-    [Meta.synthInstance.globalInstances] Inhabited Nat, [@instInhabited, instInhabitedNat]
-    [Meta.synthInstance.generate] instance instInhabitedNat
-    [Meta.synthInstance.tryResolve] 
-      [Meta.synthInstance.tryResolve] Inhabited Nat =?= Inhabited Nat
-      [Meta.synthInstance.tryResolve] success
-    [Meta.synthInstance.newAnswer] size: 0, Inhabited Nat
-    [Meta.synthInstance.newAnswer] val: instInhabitedNat
+[Meta.synthInstance] ✅ Inhabited Nat
+  [Meta.synthInstance] new goal Inhabited Nat
+    [Meta.synthInstance.instances] #[@instInhabited, instInhabitedNat]
+  [Meta.synthInstance] ✅ apply instInhabitedNat to Inhabited Nat
+    [Meta.synthInstance.tryResolve] ✅ Inhabited Nat ≟ Inhabited Nat
   [Meta.synthInstance] result instInhabitedNat
diff --git a/tests/lean/815b.lean b/tests/lean/815b.lean
@@ -11,11 +11,5 @@ instance comp (f : β → γ) (g : α → β) [IsSmooth f] [IsSmooth g] : IsSmoo
 instance diag (f : β → δ → γ) (g : α → β) (h : α → δ) [IsSmooth f] [∀ b, IsSmooth (f b)] [IsSmooth g] [IsSmooth h] : IsSmooth (λ a => f (g a) (h a)) := sorry
 
 set_option trace.Meta.synthInstance true
-set_option trace.Meta.synthInstance.globalInstances false
-set_option trace.Meta.synthInstance.newSubgoal false
-set_option trace.Meta.synthInstance.tryResolve false
-set_option trace.Meta.synthInstance.resume false
-set_option trace.Meta.synthInstance.generate false
-set_option trace.Meta.synthInstance.newAnswer false
 set_option trace.Meta.synthInstance.unusedArgs true
 example (f : β → δ → γ) [IsSmooth f] (d : δ) : IsSmooth (λ (g : α → β) a => f (g a) d) := by infer_instance