From f722465dc8d5028a4c67da7ee975edc6647f3d74 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Sun, 7 Aug 2022 16:08:53 +0200 Subject: [PATCH] chore: fix tests --- .../1018unknowMVarIssue.lean.expected.out | 132 ++++++------ tests/lean/1079.lean | 2 +- tests/lean/1079.lean.expected.out | 12 +- tests/lean/366.lean.expected.out | 16 +- tests/lean/815b.lean | 6 - tests/lean/815b.lean.expected.out | 200 ++++++++++++++---- tests/lean/973b.lean.expected.out | 9 +- tests/lean/byCasesMetaM.lean.expected.out | 24 +-- tests/lean/infoFromFailure.lean.expected.out | 18 +- tests/lean/ppNotationCode.lean.expected.out | 150 ++++++------- tests/lean/run/meta2.lean | 6 +- tests/lean/run/termElab.lean | 4 +- tests/lean/run/trace.lean | 6 +- .../sanitizeMacroScopes.lean.expected.out | 24 ++- tests/lean/simpDisch.lean.expected.out | 7 +- .../smartUnfoldingMatch.lean.expected.out | 4 +- .../syntaxInNamespacesAndPP.lean.expected.out | 22 -- tests/lean/syntaxPrec.lean.expected.out | 12 +- tests/lean/traceTacticSteps.lean.expected.out | 46 ++-- 19 files changed, 388 insertions(+), 312 deletions(-) diff --git a/tests/lean/1018unknowMVarIssue.lean.expected.out b/tests/lean/1018unknowMVarIssue.lean.expected.out index 1237c65eb9868..a5346e0352150 100644 --- 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 : @ ⟨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 : @ ⟨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 index 9d294800620a2..d1a60108347cf 100644 --- 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 index e192d6538e879..36423069dabe7 100644 --- 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 index ccac7ce637e4b..f32fe47022abb 100644 --- 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 index c3dd07a13fad3..33a2ea0cfe50d 100644 --- 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 diff --git a/tests/lean/815b.lean.expected.out b/tests/lean/815b.lean.expected.out index 5a41b130b9b1e..734c3220da77f 100644 --- a/tests/lean/815b.lean.expected.out +++ b/tests/lean/815b.lean.expected.out @@ -5,57 +5,171 @@ 815b.lean:9:9-9:13: warning: declaration uses 'sorry' 815b.lean:10:9-10:13: warning: declaration uses 'sorry' 815b.lean:11:9-11:13: warning: declaration uses 'sorry' -[Meta.synthInstance] preprocess: IsSmooth fun g a => f (g a) d ==> IsSmooth fun g a => f (g a) d - [Meta.synthInstance] - [Meta.synthInstance] main goal IsSmooth fun g a => f (g a) d +[Meta.synthInstance] ✅ IsSmooth fun g a => f (g a) d + [Meta.synthInstance] new goal IsSmooth fun g a => f (g a) d + [Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, @swap, inst✝] + [Meta.synthInstance] ❌ apply inst✝ to IsSmooth fun g a => f (g a) d + [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g a => f (g a) d ≟ IsSmooth f + [Meta.synthInstance] ✅ apply @swap to IsSmooth fun g a => f (g a) d + [Meta.synthInstance.tryResolve] ✅ IsSmooth fun g a => f (g a) d ≟ IsSmooth fun b a => f (b a) d + [Meta.synthInstance] new goal ∀ (a : α), IsSmooth fun g => f (g a) d + [Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝] + [Meta.synthInstance] ❌ apply inst✝ to ∀ (a : α), IsSmooth fun g => f (g a) d + [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => f (g a) d ≟ IsSmooth f + [Meta.synthInstance] ✅ apply @diag to ∀ (a : α), IsSmooth fun g => f (g a) d + [Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => f (a_1 a) d [Meta.synthInstance.unusedArgs] α → IsSmooth f - has unused arguments, reduced type - IsSmooth f - Transformer - fun redf a => redf + has unused arguments, reduced type + IsSmooth f + Transformer + fun redf a => redf + [Meta.synthInstance] new goal IsSmooth f + [Meta.synthInstance.instances] #[inst✝] + [Meta.synthInstance] ✅ apply inst✝ to IsSmooth f + [Meta.synthInstance.tryResolve] ✅ IsSmooth f ≟ IsSmooth f + [Meta.synthInstance.resume] propagating IsSmooth f to subgoal IsSmooth f of ∀ (a : α), IsSmooth fun g => f (g a) d + [Meta.synthInstance.resume] size: 1 [Meta.synthInstance.unusedArgs] α → IsSmooth f - has unused arguments, reduced type - IsSmooth f - Transformer - fun redf a => redf + has unused arguments, reduced type + IsSmooth f + Transformer + fun redf a => redf + [Meta.synthInstance.resume] propagating α → + IsSmooth f to subgoal α → IsSmooth f of ∀ (a : α), IsSmooth fun g => f (g a) d + [Meta.synthInstance.resume] size: 2 [Meta.synthInstance.unusedArgs] α → ∀ (b : β), IsSmooth (f b) - has unused arguments, reduced type - ∀ (b : β), IsSmooth (f b) - Transformer - fun redf a b => redf b + has unused arguments, reduced type + ∀ (b : β), IsSmooth (f b) + Transformer + fun redf a b => redf b + [Meta.synthInstance] new goal ∀ (b : β), IsSmooth (f b) + [Meta.synthInstance.instances] #[inst✝] + [Meta.synthInstance] ❌ apply inst✝ to ∀ (b : β), IsSmooth (f b) + [Meta.synthInstance.tryResolve] ❌ IsSmooth (f b) ≟ IsSmooth f + [Meta.synthInstance] ❌ apply @comp to ∀ (a : α), IsSmooth fun g => f (g a) d + [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => ?m a (?m a a_1) + [Meta.synthInstance] ✅ apply @parm to ∀ (a : α), IsSmooth fun g => f (g a) d + [Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => f (g a) d ≟ IsSmooth fun a_1 => f (a_1 a) d + [Meta.synthInstance] new goal ∀ (a : α), IsSmooth fun g => f (g a) + [Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, @swap, inst✝] + [Meta.synthInstance] ❌ apply inst✝ to ∀ (a : α), IsSmooth fun g => f (g a) + [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => f (g a) ≟ IsSmooth f + [Meta.synthInstance] ✅ apply @swap to ∀ (a : α), IsSmooth fun g => f (g a) + [Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => f (g a) ≟ IsSmooth fun b a_1 => f (b a) a_1 + [Meta.synthInstance] new goal ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1 + [Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝] + [Meta.synthInstance] ❌ apply inst✝ to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1 + [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => f (g a✝) a ≟ IsSmooth f + [Meta.synthInstance] ✅ apply @diag to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1 + [Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => f (a_1 a✝) a [Meta.synthInstance.unusedArgs] α → δ → IsSmooth f - has unused arguments, reduced type - IsSmooth f - Transformer - fun redf a a => redf + has unused arguments, reduced type + IsSmooth f + Transformer + fun redf a a => redf + [Meta.synthInstance.resume] propagating α → + δ → IsSmooth f to subgoal α → δ → IsSmooth f of ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1 + [Meta.synthInstance.resume] size: 1 [Meta.synthInstance.unusedArgs] α → δ → ∀ (b : β), IsSmooth (f b) - has unused arguments, reduced type - ∀ (b : β), IsSmooth (f b) - Transformer - fun redf a a b => redf b + has unused arguments, reduced type + ∀ (b : β), IsSmooth (f b) + Transformer + fun redf a a b => redf b + [Meta.synthInstance] ❌ apply @comp to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1 + [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => ?m a✝ a (?m a✝ a a_1) + [Meta.synthInstance] ✅ apply @parm to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1 + [Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => f (a_1 a✝) a [Meta.synthInstance.unusedArgs] ∀ (a : α), δ → IsSmooth fun g => f (g a) - has unused arguments, reduced type - ∀ (a : α), IsSmooth fun g => f (g a) - Transformer - fun redf a a_1 => redf a + has unused arguments, reduced type + ∀ (a : α), IsSmooth fun g => f (g a) + Transformer + fun redf a a_1 => redf a + [Meta.synthInstance] ❌ apply @const to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1 + [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a_1 => ?m a✝ a + [Meta.synthInstance] ❌ apply @identity to ∀ (a : α) (a_1 : δ), IsSmooth fun g => f (g a) a_1 + [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => f (g a✝) a ≟ IsSmooth fun a => a + [Meta.synthInstance] ❌ apply @diag to ∀ (a : α), IsSmooth fun g => f (g a) + [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => + f (g a) ≟ IsSmooth fun a_1 => ?m a (?m a a_1) (?m a a_1) + [Meta.synthInstance] ✅ apply @comp to ∀ (a : α), IsSmooth fun g => f (g a) + [Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => f (g a) ≟ IsSmooth fun a_1 => f (a_1 a) [Meta.synthInstance.unusedArgs] α → IsSmooth f - has unused arguments, reduced type - IsSmooth f - Transformer - fun redf a => redf + has unused arguments, reduced type + IsSmooth f + Transformer + fun redf a => redf + [Meta.synthInstance.resume] propagating α → + IsSmooth f to subgoal α → IsSmooth f of ∀ (a : α), IsSmooth fun g => f (g a) + [Meta.synthInstance.resume] size: 1 + [Meta.synthInstance] new goal ∀ (a : α), IsSmooth fun g => g a + [Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, inst✝] + [Meta.synthInstance] ❌ apply inst✝ to ∀ (a : α), IsSmooth fun g => g a + [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => g a ≟ IsSmooth f + [Meta.synthInstance] ❌ apply @diag to ∀ (a : α), IsSmooth fun g => g a + [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => + g a ≟ IsSmooth fun a_1 => ?m a (?m a a_1) (?m a a_1) + [Meta.synthInstance] ❌ apply @comp to ∀ (a : α), IsSmooth fun g => g a + [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => g a ≟ IsSmooth fun a_1 => ?m a (?m a a_1) + [Meta.synthInstance] ✅ apply @parm to ∀ (a : α), IsSmooth fun g => g a + [Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => g a ≟ IsSmooth fun a_1 => a_1 a [Meta.synthInstance.unusedArgs] α → IsSmooth fun g => g - has unused arguments, reduced type - IsSmooth fun g => g - Transformer - fun redf a => redf + has unused arguments, reduced type + IsSmooth fun g => g + Transformer + fun redf a => redf + [Meta.synthInstance] new goal IsSmooth fun g => g + [Meta.synthInstance.instances] #[@identity, @const, @parm, @comp, @diag, @swap, inst✝] + [Meta.synthInstance] ❌ apply inst✝ to IsSmooth fun g => g + [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => g ≟ IsSmooth f + [Meta.synthInstance] ✅ apply @swap to IsSmooth fun g => g + [Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => g ≟ IsSmooth fun b a => b a + [Meta.synthInstance] ❌ apply @diag to IsSmooth fun g => g + [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => g ≟ IsSmooth fun a => ?m (?m a) (?m a) + [Meta.synthInstance] ❌ apply @comp to IsSmooth fun g => g + [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => g ≟ IsSmooth fun a => ?m (?m a) + [Meta.synthInstance] ❌ apply @parm to IsSmooth fun g => g + [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => g ≟ IsSmooth fun a => ?m a ?m + [Meta.synthInstance] ❌ apply @const to IsSmooth fun g => g + [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => g ≟ IsSmooth fun a => ?m + [Meta.synthInstance] ✅ apply @identity to IsSmooth fun g => g + [Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => g ≟ IsSmooth fun a => a + [Meta.synthInstance.resume] propagating IsSmooth fun a => + a to subgoal IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a + [Meta.synthInstance.resume] size: 1 [Meta.synthInstance.unusedArgs] α → IsSmooth fun g => g - has unused arguments, reduced type - IsSmooth fun g => g - Transformer - fun redf a => redf + has unused arguments, reduced type + IsSmooth fun g => g + Transformer + fun redf a => redf + [Meta.synthInstance.resume] propagating ∀ (a : α), + IsSmooth fun a => a to subgoal α → IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a + [Meta.synthInstance.resume] size: 2 + [Meta.synthInstance.resume] propagating ∀ (a : α), + IsSmooth fun a_1 => a_1 a to subgoal ∀ (a : α), IsSmooth fun g => g a of IsSmooth fun g => g + [Meta.synthInstance.resume] size: 3 + [Meta.synthInstance.resume] propagating IsSmooth fun b a => + b a to subgoal IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a + [Meta.synthInstance.resume] size: 4 [Meta.synthInstance.unusedArgs] α → IsSmooth fun g => g - has unused arguments, reduced type - IsSmooth fun g => g - Transformer - fun redf a => redf + has unused arguments, reduced type + IsSmooth fun g => g + Transformer + fun redf a => redf + [Meta.synthInstance.resume] propagating ∀ (a : α), + IsSmooth fun b a => b a to subgoal α → IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a + [Meta.synthInstance.resume] size: 8 + [Meta.synthInstance.resume] propagating ∀ (a : α), + IsSmooth fun a => a to subgoal α → IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a + [Meta.synthInstance.resume] size: 5 + [Meta.synthInstance.resume] propagating ∀ (a : α), + IsSmooth fun a_1 => a_1 a to subgoal ∀ (a : α), IsSmooth fun g => g a of ∀ (a : α), IsSmooth fun g => f (g a) + [Meta.synthInstance.resume] size: 4 + [Meta.synthInstance.resume] propagating ∀ (a : α), + IsSmooth fun a_1 => + f (a_1 a) to subgoal ∀ (a : α), IsSmooth fun g => f (g a) of ∀ (a : α), IsSmooth fun g => f (g a) d + [Meta.synthInstance.resume] size: 5 + [Meta.synthInstance.resume] propagating ∀ (a : α), + IsSmooth fun a_1 => + f (a_1 a) d to subgoal ∀ (a : α), IsSmooth fun g => f (g a) d of IsSmooth fun g a => f (g a) d + [Meta.synthInstance.resume] size: 6 [Meta.synthInstance] result swap fun a g => f (g a) d diff --git a/tests/lean/973b.lean.expected.out b/tests/lean/973b.lean.expected.out index 4b5ec8419f6d0..42e17ddbc12a0 100644 --- a/tests/lean/973b.lean.expected.out +++ b/tests/lean/973b.lean.expected.out @@ -2,13 +2,12 @@ 973b.lean:9:8-9:11: warning: declaration uses 'sorry' [Meta.Tactic.simp.discharge] >> discharge?: ?p x [Meta.Tactic.simp.discharge] ex, failed to discharge hypotheses - ?p x + ?p x [Meta.Tactic.simp.discharge] >> discharge?: ?p (f x) [Meta.Tactic.simp.discharge] >> discharge?: ?p x [Meta.Tactic.simp.discharge] ex, failed to discharge hypotheses - ?p x + ?p x [Meta.Tactic.simp.discharge] >> discharge?: ?p x [Meta.Tactic.simp.discharge] ex, failed to discharge hypotheses - ?p x -[Meta.Tactic.simp.discharge] ex, failed to discharge hypotheses - ?p (f x) + ?p x +[Meta.Tactic.simp.discharge] ex, failed to discharge hypotheses ?p (f x) diff --git a/tests/lean/byCasesMetaM.lean.expected.out b/tests/lean/byCasesMetaM.lean.expected.out index d213534f3bc81..c52971f811421 100644 --- a/tests/lean/byCasesMetaM.lean.expected.out +++ b/tests/lean/byCasesMetaM.lean.expected.out @@ -1,14 +1,14 @@ [Meta.debug] p q : Prop -h : p ∧ q -⊢ q ∧ q + h : p ∧ q + ⊢ q ∧ q [Meta.debug] case inl -p q : Prop -h : p ∧ q -hAux : p -⊢ q ∧ q ------- -case inr -p q : Prop -h : p ∧ q -hAux : ¬p -⊢ q ∧ q + p q : Prop + h : p ∧ q + hAux : p + ⊢ q ∧ q + ------ + case inr + p q : Prop + h : p ∧ q + hAux : ¬p + ⊢ q ∧ q diff --git a/tests/lean/infoFromFailure.lean.expected.out b/tests/lean/infoFromFailure.lean.expected.out index c523330fa466b..04f965edf389f 100644 --- a/tests/lean/infoFromFailure.lean.expected.out +++ b/tests/lean/infoFromFailure.lean.expected.out @@ -1,13 +1,7 @@ B.foo "hello" : String × String -[Meta.synthInstance] preprocess: Add String ==> Add String - [Meta.synthInstance] - [Meta.synthInstance] main goal Add String - [Meta.synthInstance.newSubgoal] Add String - [Meta.synthInstance.globalInstances] Add String, [] - [Meta.synthInstance] failed -[Meta.synthInstance] preprocess: Add Bool ==> Add Bool - [Meta.synthInstance] - [Meta.synthInstance] main goal Add Bool - [Meta.synthInstance.newSubgoal] Add Bool - [Meta.synthInstance.globalInstances] Add Bool, [] - [Meta.synthInstance] failed +[Meta.synthInstance] ❌ Add String + [Meta.synthInstance] no instances for Add String + [Meta.synthInstance.instances] #[] +[Meta.synthInstance] ❌ Add Bool + [Meta.synthInstance] no instances for Add Bool + [Meta.synthInstance.instances] #[] diff --git a/tests/lean/ppNotationCode.lean.expected.out b/tests/lean/ppNotationCode.lean.expected.out index 5d4902cfc83ae..fba17d6f971c7 100644 --- a/tests/lean/ppNotationCode.lean.expected.out +++ b/tests/lean/ppNotationCode.lean.expected.out @@ -1,90 +1,90 @@ [Elab.definition.body] «term_+++_» : Lean.TrailingParserDescr := -Lean.ParserDescr.trailingNode `«term_+++_» 45 46 - (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "+++") (Lean.ParserDescr.cat `term 46)) + Lean.ParserDescr.trailingNode `«term_+++_» 45 46 + (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "+++") (Lean.ParserDescr.cat `term 46)) [Elab.definition.body] «_aux_ppNotationCode___macroRules_term_+++__1» : Lean.Macro := -fun x => - let discr := x; - if Lean.Syntax.isOfKind discr `«term_+++_» = true then - let discr_1 := Lean.Syntax.getArg discr 0; - let discr_2 := Lean.Syntax.getArg discr 1; - let discr := Lean.Syntax.getArg discr 2; - let rhs := { raw := discr }; - let lhs := { raw := discr_1 }; - do - let info ← Lean.MonadRef.mkInfoFromRefPos - let scp ← Lean.getCurrMacroScope - let mainModule ← Lean.getMainModule - pure - { raw := - Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app - #[Lean.Syntax.ident info (String.toSubstring "Nat.add") (Lean.addMacroScope mainModule `Nat.add scp) - [(`Nat.add, [])], - Lean.Syntax.node Lean.SourceInfo.none `null #[lhs.raw, rhs.raw]] }.raw - else - let discr := x; - throw Lean.Macro.Exception.unsupportedSyntax -[Elab.definition.body] _aux_ppNotationCode___unexpand_Nat_add_1 : Lean.PrettyPrinter.Unexpander := -fun x => - let discr := x; - if Lean.Syntax.isOfKind discr `Lean.Parser.Term.app = true then - let discr_1 := Lean.Syntax.getArg discr 0; - bif false || Lean.Syntax.isOfKind discr_1 `ident then - let discr_2 := Lean.Syntax.getArg discr 1; - if Lean.Syntax.matchesNull discr_2 2 = true then - let discr := Lean.Syntax.getArg discr_2 0; - let discr_3 := Lean.Syntax.getArg discr_2 1; - let rhs := { raw := discr_3 }; - let lhs := { raw := discr }; - let f := { raw := discr_1 }; - Lean.withRef f.raw do - let info ← Lean.MonadRef.mkInfoFromRefPos - let _ ← Lean.getCurrMacroScope - let _ ← Lean.getMainModule - pure - { raw := - Lean.Syntax.node Lean.SourceInfo.none `«term_+++_» - #[lhs.raw, Lean.Syntax.atom info "+++", rhs.raw] }.raw + fun x => + let discr := x; + if Lean.Syntax.isOfKind discr `«term_+++_» = true then + let discr_1 := Lean.Syntax.getArg discr 0; + let discr_2 := Lean.Syntax.getArg discr 1; + let discr := Lean.Syntax.getArg discr 2; + let rhs := { raw := discr }; + let lhs := { raw := discr_1 }; + do + let info ← Lean.MonadRef.mkInfoFromRefPos + let scp ← Lean.getCurrMacroScope + let mainModule ← Lean.getMainModule + pure + { raw := + Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app + #[Lean.Syntax.ident info (String.toSubstring "Nat.add") (Lean.addMacroScope mainModule `Nat.add scp) + [(`Nat.add, [])], + Lean.Syntax.node Lean.SourceInfo.none `null #[lhs.raw, rhs.raw]] }.raw else - let discr := Lean.Syntax.getArg discr 1; - throw () - else - let discr_2 := Lean.Syntax.getArg discr 0; - if Lean.Syntax.isOfKind discr_2 `Lean.Parser.Term.app = true then - let discr_3 := Lean.Syntax.getArg discr_2 0; - bif false || Lean.Syntax.isOfKind discr_3 `ident then - let discr_4 := Lean.Syntax.getArg discr_2 1; - if Lean.Syntax.matchesNull discr_4 2 = true then - let discr_5 := Lean.Syntax.getArg discr_4 0; - let discr_6 := Lean.Syntax.getArg discr_4 1; - let discr := Lean.Syntax.getArg discr 1; - let moreArgs := Lean.TSyntaxArray.mk (Lean.Syntax.getArgs discr); - let rhs := { raw := discr_6 }; - let lhs := { raw := discr_5 }; - let f := { raw := discr_3 }; + let discr := x; + throw Lean.Macro.Exception.unsupportedSyntax +[Elab.definition.body] _aux_ppNotationCode___unexpand_Nat_add_1 : Lean.PrettyPrinter.Unexpander := + fun x => + let discr := x; + if Lean.Syntax.isOfKind discr `Lean.Parser.Term.app = true then + let discr_1 := Lean.Syntax.getArg discr 0; + bif false || Lean.Syntax.isOfKind discr_1 `ident then + let discr_2 := Lean.Syntax.getArg discr 1; + if Lean.Syntax.matchesNull discr_2 2 = true then + let discr := Lean.Syntax.getArg discr_2 0; + let discr_3 := Lean.Syntax.getArg discr_2 1; + let rhs := { raw := discr_3 }; + let lhs := { raw := discr }; + let f := { raw := discr_1 }; Lean.withRef f.raw do let info ← Lean.MonadRef.mkInfoFromRefPos let _ ← Lean.getCurrMacroScope let _ ← Lean.getMainModule pure { raw := - Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app - #[Lean.Syntax.node Lean.SourceInfo.none `«term_+++_» - #[lhs.raw, Lean.Syntax.atom info "+++", rhs.raw], - Lean.Syntax.node Lean.SourceInfo.none `null - (Array.append #[] (Lean.TSyntaxArray.raw moreArgs))] }.raw + Lean.Syntax.node Lean.SourceInfo.none `«term_+++_» + #[lhs.raw, Lean.Syntax.atom info "+++", rhs.raw] }.raw else - let discr_5 := Lean.Syntax.getArg discr_2 1; let discr := Lean.Syntax.getArg discr 1; throw () else - let discr_4 := Lean.Syntax.getArg discr_2 0; - let discr_5 := Lean.Syntax.getArg discr_2 1; - let discr := Lean.Syntax.getArg discr 1; - throw () + let discr_2 := Lean.Syntax.getArg discr 0; + if Lean.Syntax.isOfKind discr_2 `Lean.Parser.Term.app = true then + let discr_3 := Lean.Syntax.getArg discr_2 0; + bif false || Lean.Syntax.isOfKind discr_3 `ident then + let discr_4 := Lean.Syntax.getArg discr_2 1; + if Lean.Syntax.matchesNull discr_4 2 = true then + let discr_5 := Lean.Syntax.getArg discr_4 0; + let discr_6 := Lean.Syntax.getArg discr_4 1; + let discr := Lean.Syntax.getArg discr 1; + let moreArgs := Lean.TSyntaxArray.mk (Lean.Syntax.getArgs discr); + let rhs := { raw := discr_6 }; + let lhs := { raw := discr_5 }; + let f := { raw := discr_3 }; + Lean.withRef f.raw do + let info ← Lean.MonadRef.mkInfoFromRefPos + let _ ← Lean.getCurrMacroScope + let _ ← Lean.getMainModule + pure + { raw := + Lean.Syntax.node Lean.SourceInfo.none `Lean.Parser.Term.app + #[Lean.Syntax.node Lean.SourceInfo.none `«term_+++_» + #[lhs.raw, Lean.Syntax.atom info "+++", rhs.raw], + Lean.Syntax.node Lean.SourceInfo.none `null + (Array.append #[] (Lean.TSyntaxArray.raw moreArgs))] }.raw + else + let discr_5 := Lean.Syntax.getArg discr_2 1; + let discr := Lean.Syntax.getArg discr 1; + throw () + else + let discr_4 := Lean.Syntax.getArg discr_2 0; + let discr_5 := Lean.Syntax.getArg discr_2 1; + let discr := Lean.Syntax.getArg discr 1; + throw () + else + let discr_3 := Lean.Syntax.getArg discr 0; + let discr := Lean.Syntax.getArg discr 1; + throw () else - let discr_3 := Lean.Syntax.getArg discr 0; - let discr := Lean.Syntax.getArg discr 1; + let discr := x; throw () - else - let discr := x; - throw () diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean index 580c151431b38..1aca9eba005aa 100644 --- a/tests/lean/run/meta2.lean +++ b/tests/lean/run/meta2.lean @@ -369,7 +369,7 @@ pure () #eval tst26 section -set_option trace.Meta.isDefEq.step true +set_option trace.Meta.isDefEq true set_option trace.Meta.isDefEq.delta true set_option trace.Meta.isDefEq.assign true @@ -572,7 +572,7 @@ checkM $ getAssignment m2 >>= fun v => pure $ v == nat; pure () set_option pp.all true -set_option trace.Meta.isDefEq.step true +set_option trace.Meta.isDefEq true set_option trace.Meta.isDefEq.delta true set_option trace.Meta.isDefEq.assign true @@ -658,7 +658,7 @@ check w; print w; pure () -set_option trace.Meta.isDefEq.step false +set_option trace.Meta.isDefEq false set_option trace.Meta.isDefEq.delta false set_option trace.Meta.isDefEq.assign false #eval tst41 diff --git a/tests/lean/run/termElab.lean b/tests/lean/run/termElab.lean index 7ad3f8e72e921..d41055556f2c8 100644 --- a/tests/lean/run/termElab.lean +++ b/tests/lean/run/termElab.lean @@ -10,7 +10,7 @@ let opt ← getOptions; let stx ← `(forall (a b : Nat), Nat); IO.println "message 1"; -- This message goes direct to stdio. It will be displayed before trace messages. let e ← elabTermAndSynthesize stx none; -logDbgTrace m!">>> {e}"; -- display message when `trace.Elab.debug` is true +trace[Elab.debug] m!">>> {e}"; -- display message when `trace.Elab.debug` is true IO.println "message 2" #eval tst1 @@ -21,7 +21,7 @@ let a := mkIdent `a; let b := mkIdent `b; let stx ← `((fun ($a : Type) (x : $a) => @id $a x) _ 1); let e ← elabTermAndSynthesize stx none; -logDbgTrace m!">>> {e}"; +trace[Elab.debug] m!">>> {e}"; throwErrorIfErrors #eval tst2 diff --git a/tests/lean/run/trace.lean b/tests/lean/run/trace.lean index e9fca4687131d..16c1701797e60 100644 --- a/tests/lean/run/trace.lean +++ b/tests/lean/run/trace.lean @@ -14,7 +14,7 @@ do trace[module] (m!"hello" ++ MessageData.nest 9 (m!"\n" ++ "world")); pure () def tst2 (b : Bool) : M Unit := -traceCtx `module $ do +withTraceNode `module (fun _ => return "message") do tst1; trace[bughunt] "at test2"; if b then throwError "error"; @@ -30,7 +30,7 @@ def slow (b : Bool) : Nat := ack 4 (cond b 0 1) def tst3 (b : Bool) : M Unit := -do traceCtx `module $ do { +do withTraceNode `module.slow (fun _ => return m!"slow: {slow b}") do { tst2 b; tst1 }; @@ -39,7 +39,7 @@ do traceCtx `module $ do { -- if `trace.slow is active. trace[slow] (m!"slow message: " ++ toString (slow b)) -- This is true even if it is a monad computation: - trace[slow] (m!"slow message: " ++ (toString (slow b))) + trace[slow] (m!"slow message: " ++ (← pure (toString (slow b)))) def run (x : M Unit) : M Unit := withReader diff --git a/tests/lean/sanitizeMacroScopes.lean.expected.out b/tests/lean/sanitizeMacroScopes.lean.expected.out index 878f678fd20b9..fb7ec6f25be8e 100644 --- a/tests/lean/sanitizeMacroScopes.lean.expected.out +++ b/tests/lean/sanitizeMacroScopes.lean.expected.out @@ -1,13 +1,19 @@ fun x x_1 => x : (x : ?m) → ?m x → ?m [Elab.step] expected type: , term -fun x => m x -[Elab.step] expected type: Sort ?u, term - _ - [Elab.step] expected type: , term - m x - [Elab.step] expected type: , term - fun x✝ => x - [Elab.step] expected type: Sort ?u, term + fun x => m x + [Elab.step] expected type: Sort ?u, term _ + [Elab.step.result] ?m + [Elab.step] expected type: , term + m x + [Elab.step] expected type: , term + fun x✝ => x + [Elab.step] expected type: Sort ?u, term + _ + [Elab.step.result] ?m [Elab.step] expected type: , term - x + x + [Elab.step.result] x + [Elab.step.result] fun x_1 => x + [Elab.step.result] fun x_1 => x + [Elab.step.result] fun x x_1 => x diff --git a/tests/lean/simpDisch.lean.expected.out b/tests/lean/simpDisch.lean.expected.out index e7b4bfc6e4d01..c6e58fe6a0582 100644 --- a/tests/lean/simpDisch.lean.expected.out +++ b/tests/lean/simpDisch.lean.expected.out @@ -8,12 +8,7 @@ h1 : x ≠ 0 h2 : y ≠ 0 h3 : x = y ⊢ x ≠ 0 -case simp.discharger -x y : Nat -h1 : x ≠ 0 -h2 : y ≠ 0 -h3 : x = y -⊢ y ≠ 0 +case simp.discharger x y : Nat h1 : x ≠ 0 h2 : y ≠ 0 h3 : x = y ⊢ y ≠ 0 x y : Nat h1 : x ≠ 0 h2 : y ≠ 0 diff --git a/tests/lean/smartUnfoldingMatch.lean.expected.out b/tests/lean/smartUnfoldingMatch.lean.expected.out index 84b4c40133ca1..3d995b176e3e8 100644 --- a/tests/lean/smartUnfoldingMatch.lean.expected.out +++ b/tests/lean/smartUnfoldingMatch.lean.expected.out @@ -1,4 +1,4 @@ 42 [Meta.debug] r: match x, 0 with - | some x, x_1 => x - | none, e => e + | some x, x_1 => x + | none, e => e diff --git a/tests/lean/syntaxInNamespacesAndPP.lean.expected.out b/tests/lean/syntaxInNamespacesAndPP.lean.expected.out index a42eda11a4503..47aa41c141159 100644 --- a/tests/lean/syntaxInNamespacesAndPP.lean.expected.out +++ b/tests/lean/syntaxInNamespacesAndPP.lean.expected.out @@ -1,27 +1,5 @@ -[Elab.command] #check foo true true : Bool -[Elab.step] expected type: , term -foo true -[Elab.step] expected type: , term - true - [Elab.app.args] explicit: false, ellipsis: false, true : Bool - [Elab.app.args] namedArgs: [] - [Elab.app.args] args: [] - [Elab.app.finalize] true - [Elab.app.finalize] after etaArgs, true : Bool -[Elab.command] end -[Elab.command] #check bla true true : Bool -[Elab.step] expected type: , term -bla true -[Elab.step] expected type: , term - true - [Elab.app.args] explicit: false, ellipsis: false, true : Bool - [Elab.app.args] namedArgs: [] - [Elab.app.args] args: [] - [Elab.app.finalize] true - [Elab.app.finalize] after etaArgs, true : Bool -[Elab.command] end def Bla.bla : Lean.ParserDescr := Lean.ParserDescr.node `Bla.bla 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "bla") (Lean.ParserDescr.cat `term 0)) diff --git a/tests/lean/syntaxPrec.lean.expected.out b/tests/lean/syntaxPrec.lean.expected.out index 3d1ad2db0e7ee..c1626128b656e 100644 --- a/tests/lean/syntaxPrec.lean.expected.out +++ b/tests/lean/syntaxPrec.lean.expected.out @@ -1,9 +1,9 @@ syntaxPrec.lean:1:18: error: expected ':' [Elab.command] syntax "foo"("*" <|> term,+) : term [Elab.command] @[termParser 1000] -def «termFoo*_» : Lean.ParserDescr✝ := - ParserDescr.node✝ `«termFoo*_» 1022 - (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "foo") - (ParserDescr.binary✝ `orelse (ParserDescr.symbol✝ "*") - ((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) (ParserDescr.cat✝ `term 0) "," (ParserDescr.symbol✝ ", ") - Bool.false✝))) + def «termFoo*_» : Lean.ParserDescr✝ := + ParserDescr.node✝ `«termFoo*_» 1022 + (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "foo") + (ParserDescr.binary✝ `orelse (ParserDescr.symbol✝ "*") + ((with_annotate_term"sepBy1(" @ParserDescr.sepBy1✝) (ParserDescr.cat✝ `term 0) "," + (ParserDescr.symbol✝ ", ") Bool.false✝))) diff --git a/tests/lean/traceTacticSteps.lean.expected.out b/tests/lean/traceTacticSteps.lean.expected.out index 0d4e1091e6854..3182ab4751d04 100644 --- a/tests/lean/traceTacticSteps.lean.expected.out +++ b/tests/lean/traceTacticSteps.lean.expected.out @@ -1,32 +1,34 @@ -[Elab.step] expected type: Sort ?u, term -True +[Elab.step] expected type: Prop, term + True + [Elab.step.result] True [Elab.step] expected type: True, term -by - skip - trivial + by + skip + trivial + [Elab.step.result] ?m +[Elab.step] skip [Elab.step] - skip - trivial + skip + trivial [Elab.step] - skip - trivial -[Elab.step] skip + skip + trivial [Elab.step] trivial [Elab.step] (apply And.intro✝) <;> trivial [Elab.step] focus - apply And.intro✝ - with_annotate_state"<;>" skip - all_goals - trivial + apply And.intro✝ + with_annotate_state"<;>" skip + all_goals + trivial [Elab.step] - apply And.intro✝ - with_annotate_state"<;>" skip - all_goals - trivial + apply And.intro✝ + with_annotate_state"<;>" skip + all_goals + trivial [Elab.step] - apply And.intro✝ - with_annotate_state"<;>" skip - all_goals - trivial + apply And.intro✝ + with_annotate_state"<;>" skip + all_goals + trivial [Elab.step] apply And.intro✝ [Elab.step] apply True.intro✝