diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index d0b705849e..a8b7ba215b 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -621,9 +621,6 @@ This is the same as `#eval show MetaM Unit from do discard doSeq`. -/ syntax (name := runMeta) "run_meta " doSeq : command -set_option linter.missingDocs false in -syntax guardMsgsFilterSeverity := &"info" <|> &"warning" <|> &"error" <|> &"all" - /-- `#reduce ` reduces the expression `` to its normal form. This involves applying reduction rules until no further reduction is possible. @@ -640,15 +637,27 @@ of expressions. -/ syntax (name := reduceCmd) "#reduce " (atomic("(" &"proofs" " := " &"true" ")"))? (atomic("(" &"types" " := " &"true" ")"))? term : command +set_option linter.missingDocs false in +syntax guardMsgsFilterAction := &"check" <|> &"drop" <|> &"pass" + +set_option linter.missingDocs false in +syntax guardMsgsFilterSeverity := &"trace" <|> &"info" <|> &"warning" <|> &"error" <|> &"all" + /-- A message filter specification for `#guard_msgs`. -- `info`, `warning`, `error`: capture messages with the given severity level. -- `all`: capture all messages (the default). -- `drop info`, `drop warning`, `drop error`: drop messages with the given severity level. -- `drop all`: drop every message. -These filters are processed in left-to-right order. +- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level. +- `trace`: captures trace messages +- `all`: capture all messages. + +The filters can be prefixed with +- `check` (the default): capture and check the message +- `drop`: drop the message +- `pass`: let the message pass through + +If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in +left-to-right order, with an implicit `pass all` at the end. -/ -syntax guardMsgsFilter := &"drop"? guardMsgsFilterSeverity +syntax guardMsgsFilter := guardMsgsFilterAction ? guardMsgsFilterSeverity set_option linter.missingDocs false in syntax guardMsgsWhitespaceArg := &"exact" <|> &"normalized" <|> &"lax" @@ -719,13 +728,20 @@ In general, `#guard_msgs` accepts a comma-separated list of configuration clause ``` #guard_msgs (configElt,*) in cmd ``` -By default, the configuration list is `(all, whitespace := normalized, ordering := exact)`. +By default, the configuration list is `(check all, whitespace := normalized, ordering := exact)`. -Message filters (processed in left-to-right order): -- `info`, `warning`, `error`: capture messages with the given severity level. -- `all`: capture all messages (the default). -- `drop info`, `drop warning`, `drop error`: drop messages with the given severity level. -- `drop all`: drop every message. +Message filters select messages by severity: +- `info`, `warning`, `error`: (non-trace) messages with the given severity level. +- `trace`: trace messages +- `all`: all messages. + +The filters can be prefixed with the action to take: +- `check` (the default): capture and check the message +- `drop`: drop the message +- `pass`: let the message pass through + +If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in +left-to-right order, with an implicit `pass all` at the end. Whitespace handling (after trimming leading and trailing whitespace): - `whitespace := exact` requires an exact whitespace match. diff --git a/src/Lean/Elab/GuardMsgs.lean b/src/Lean/Elab/GuardMsgs.lean index 846a4e0cdf..697f9fa8db 100644 --- a/src/Lean/Elab/GuardMsgs.lean +++ b/src/Lean/Elab/GuardMsgs.lean @@ -31,10 +31,13 @@ private def messageToStringWithoutPos (msg : Message) : BaseIO String := do unless msg.caption == "" do str := msg.caption ++ ":\n" ++ str if !("\n".isPrefixOf str) then str := " " ++ str - match msg.severity with - | MessageSeverity.information => str := "info:" ++ str - | MessageSeverity.warning => str := "warning:" ++ str - | MessageSeverity.error => str := "error:" ++ str + if msg.isTrace then + str := "trace:" ++ str + else + match msg.severity with + | MessageSeverity.information => str := "info:" ++ str + | MessageSeverity.warning => str := "warning:" ++ str + | MessageSeverity.error => str := "error:" ++ str if str.isEmpty || str.back != '\n' then str := str ++ "\n" return str @@ -46,7 +49,7 @@ inductive SpecResult /-- Drop the message and delete it. -/ | drop /-- Do not capture the message. -/ - | passthrough + | pass /-- The method to use when normalizing whitespace, after trimming. -/ inductive WhitespaceMode @@ -64,6 +67,25 @@ inductive MessageOrdering /-- Sort the produced messages. -/ | sorted +def parseGuardMsgsFilterAction (action? : Option (TSyntax ``guardMsgsFilterAction)) : + CommandElabM SpecResult := do + if let some action := action? then + match action with + | `(guardMsgsFilterAction| check) => pure .check + | `(guardMsgsFilterAction| drop) => pure .drop + | `(guardMsgsFilterAction| pass) => pure .pass + | _ => throwUnsupportedSyntax + else + pure .check + +def parseGuardMsgsFilterSeverity : TSyntax ``guardMsgsFilterSeverity → CommandElabM (Message → Bool) + | `(guardMsgsFilterSeverity| trace) => pure fun msg => msg.isTrace + | `(guardMsgsFilterSeverity| info) => pure fun msg => !msg.isTrace && msg.severity == .information + | `(guardMsgsFilterSeverity| warning) => pure fun msg => !msg.isTrace && msg.severity == .warning + | `(guardMsgsFilterSeverity| error) => pure fun msg => !msg.isTrace && msg.severity == .error + | `(guardMsgsFilterSeverity| all) => pure fun _ => true + | _ => throwUnsupportedSyntax + /-- Parses a `guardMsgsSpec`. - No specification: check everything. - With a specification: interpret the spec, and if nothing applies pass it through. -/ @@ -79,24 +101,23 @@ def parseGuardMsgsSpec (spec? : Option (TSyntax ``guardMsgsSpec)) : let mut whitespace : WhitespaceMode := .normalized let mut ordering : MessageOrdering := .exact let mut p? : Option (Message → SpecResult) := none - let pushP (s : MessageSeverity) (drop : Bool) (p? : Option (Message → SpecResult)) + let pushP (action : SpecResult) (msgP : Message → Bool) (p? : Option (Message → SpecResult)) (msg : Message) : SpecResult := - let p := p?.getD fun _ => .passthrough - if msg.severity == s then if drop then .drop else .check - else p msg + if msgP msg then + action + else + (p?.getD fun _ => .pass) msg for elt in elts.reverse do match elt with - | `(guardMsgsSpecElt| $[drop%$drop?]? info) => p? := pushP .information drop?.isSome p? - | `(guardMsgsSpecElt| $[drop%$drop?]? warning) => p? := pushP .warning drop?.isSome p? - | `(guardMsgsSpecElt| $[drop%$drop?]? error) => p? := pushP .error drop?.isSome p? - | `(guardMsgsSpecElt| $[drop%$drop?]? all) => p? := some fun _ => if drop?.isSome then .drop else .check + | `(guardMsgsSpecElt| $[$action?]? $sev) => p? := pushP (← parseGuardMsgsFilterAction action?) (← parseGuardMsgsFilterSeverity sev) p? | `(guardMsgsSpecElt| whitespace := exact) => whitespace := .exact | `(guardMsgsSpecElt| whitespace := normalized) => whitespace := .normalized | `(guardMsgsSpecElt| whitespace := lax) => whitespace := .lax | `(guardMsgsSpecElt| ordering := exact) => ordering := .exact | `(guardMsgsSpecElt| ordering := sorted) => ordering := .sorted | _ => throwUnsupportedSyntax - return (whitespace, ordering, p?.getD fun _ => .check) + let defaultP := fun _ => .check + return (whitespace, ordering, p?.getD defaultP) /-- An info tree node corresponding to a failed `#guard_msgs` invocation, used for code action support. -/ @@ -157,7 +178,7 @@ def MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List S match specFn msg with | .check => toCheck := toCheck.add msg | .drop => pure () - | .passthrough => toPassthrough := toPassthrough.add msg + | pass => toPassthrough := toPassthrough.add msg let strings ← toCheck.toList.mapM (messageToStringWithoutPos ·) let strings := ordering.apply strings let res := "---\n".intercalate strings |>.trim diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index 2008cbc5f1..47c52777ee 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -147,6 +147,13 @@ def kind : MessageData → Name | tagged n _ => n | _ => .anonymous +def isTrace : MessageData → Bool + | withContext _ msg => msg.isTrace + | withNamingContext _ msg => msg.isTrace + | tagged _ msg => msg.isTrace + | .trace _ _ _ => true + | _ => false + /-- An empty message. -/ def nil : MessageData := ofFormat Format.nil @@ -424,6 +431,9 @@ namespace Message @[inherit_doc MessageData.kind] abbrev kind (msg : Message) := msg.data.kind +def isTrace (msg : Message) : Bool := + msg.data.isTrace + /-- Serializes the message, converting its data into a string and saving its kind. -/ @[inline] def serialize (msg : Message) : BaseIO SerialMessage := do return {msg with kind := msg.kind, data := ← msg.data.toString} diff --git a/tests/lean/run/1234.lean b/tests/lean/run/1234.lean index a2a4581f68..59c63f092b 100644 --- a/tests/lean/run/1234.lean +++ b/tests/lean/run/1234.lean @@ -10,7 +10,7 @@ set_option Elab.async false -- for stable message ordering in #guard_msgs /-- warning: declaration uses 'sorry' --- -info: [Meta.Tactic.simp.rewrite] h₁:1000: +trace: [Meta.Tactic.simp.rewrite] h₁:1000: k ≤ v - 1 ==> True @@ -47,7 +47,7 @@ example (h₁: k ≤ v - 1) (h₂: 0 < v): /-- warning: declaration uses 'sorry' --- -info: [Meta.Tactic.simp.rewrite] h₁:1000: +trace: [Meta.Tactic.simp.rewrite] h₁:1000: k ≤ v - 1 ==> True @@ -82,7 +82,7 @@ example (h₁: k ≤ v - 1) (h₂: 0 < v): /-- warning: declaration uses 'sorry' --- -info: [Meta.Tactic.simp.rewrite] h₁:1000: +trace: [Meta.Tactic.simp.rewrite] h₁:1000: k ≤ v - 1 ==> True diff --git a/tests/lean/run/1380.lean b/tests/lean/run/1380.lean index 10d075fdee..d3896189d4 100644 --- a/tests/lean/run/1380.lean +++ b/tests/lean/run/1380.lean @@ -3,7 +3,7 @@ variable (n v₁ v₂) (hv₁: v₁ < n + 1) (hv₂: v₂ < n + 1) theorem foo (_: ¬ Fin.mk v₂ hv₂ = Fin.mk v₁ hv₁ ): True := trivial /-- -info: [Meta.Tactic.simp.unify] eq_self:1000, failed to unify +trace: [Meta.Tactic.simp.unify] eq_self:1000, failed to unify ?a = ?a with ⟨v₂, hv₂⟩ = ⟨v₁, hv₁⟩ diff --git a/tests/lean/run/1815.lean b/tests/lean/run/1815.lean index b68c651d18..3b33f5ed8f 100644 --- a/tests/lean/run/1815.lean +++ b/tests/lean/run/1815.lean @@ -7,7 +7,7 @@ theorem mul_comm (a b : α) : a * b = b * a := sorry set_option trace.Meta.Tactic.simp true /-- -info: [Meta.Tactic.simp.rewrite] mul_comm:1000:perm, perm rejected Left a ==> default * a +trace: [Meta.Tactic.simp.rewrite] mul_comm:1000:perm, perm rejected Left a ==> default * a [Meta.Tactic.simp.rewrite] mul_comm:1000:perm: Right a ==> diff --git a/tests/lean/run/1834.lean b/tests/lean/run/1834.lean index 4d5e6c2213..ec5344e9a2 100644 --- a/tests/lean/run/1834.lean +++ b/tests/lean/run/1834.lean @@ -94,7 +94,7 @@ end Rewrote forall, remains a forall, since domain is `Nat`. -/ /-- -info: P : Nat → Prop +trace: P : Nat → Prop q : Prop h : ∀ (n : Nat), P n = q hq : q @@ -111,7 +111,7 @@ example (P : Nat → Prop) (q : Prop) (h : ∀ n, P n = q) (hq : q) : When `pp.foralls` is false, uses non-dependent `→`. -/ /-- -info: P : Nat → Prop +trace: P : Nat → Prop q : Prop h : (n : Nat) → P n = q hq : q @@ -129,7 +129,7 @@ example (P : Nat → Prop) (q : Prop) (h : ∀ n, P n = q) (hq : q) : Rewrote forall, turns into an implication, since domain is a proposition. -/ /-- -info: p : Prop +trace: p : Prop P : p → Prop q : Prop h : ∀ (n : p), P n = q diff --git a/tests/lean/run/2042.lean b/tests/lean/run/2042.lean index 7e850b3dff..849e1eaf3e 100644 --- a/tests/lean/run/2042.lean +++ b/tests/lean/run/2042.lean @@ -2,7 +2,7 @@ 2 * a /-- -info: case h +trace: case h x : Nat ⊢ 2 * x = x + x -/ @@ -19,7 +19,7 @@ by | a => 2 * a /-- -info: case h +trace: case h x : Nat ⊢ 2 * x = x + x -/ diff --git a/tests/lean/run/2159.lean b/tests/lean/run/2159.lean index 4c51b3ada4..40e9d83f94 100644 --- a/tests/lean/run/2159.lean +++ b/tests/lean/run/2159.lean @@ -1,7 +1,7 @@ /-- -info: ⊢ 1.2 < 2 +trace: ⊢ 1.2 < 2 --- -info: ⊢ 1.2 < 2 +trace: ⊢ 1.2 < 2 --- warning: declaration uses 'sorry' -/ diff --git a/tests/lean/run/2389.lean b/tests/lean/run/2389.lean index e9ac815d0a..da9be3d02c 100644 --- a/tests/lean/run/2389.lean +++ b/tests/lean/run/2389.lean @@ -8,17 +8,17 @@ inductive Forall (P : α → Prop) : List α → Prop | nil : Forall P [] | cons : {x : α} → P x → Forall P l → Forall P (x::l) -inductive Tree : Type := +inductive Tree : Type where | leaf : Nat → Tree | node : List Tree → Tree set_option trace.Meta.IndPredBelow true in -/-- info: [Meta.IndPredBelow] Nested or not recursive -/ +/-- trace: [Meta.IndPredBelow] Nested or not recursive -/ #guard_msgs in /-- Despite not having `.below` and `.brecOn`, the type is still usable thanks to well-founded recursion. -/ -inductive OnlyZeros : Tree → Prop := +inductive OnlyZeros : Tree → Prop where | leaf : OnlyZeros (.leaf 0) | node (l : List Tree): Forall OnlyZeros l → OnlyZeros (.node l) diff --git a/tests/lean/run/2916.lean b/tests/lean/run/2916.lean index 45716a7faa..04c42093f5 100644 --- a/tests/lean/run/2916.lean +++ b/tests/lean/run/2916.lean @@ -1,7 +1,7 @@ set_option pp.coercions false -- Show `OfNat.ofNat` when present for clarity /-- -info: x : Nat +trace: x : Nat ⊢ OfNat.ofNat 2 = x --- warning: declaration uses 'sorry' @@ -13,7 +13,7 @@ example : nat_lit 2 = x := by sorry /-- -info: x : Nat +trace: x : Nat ⊢ OfNat.ofNat 2 = x --- warning: declaration uses 'sorry' @@ -25,7 +25,7 @@ example : nat_lit 2 = x := by sorry /-- -info: α : Nat → Type +trace: α : Nat → Type f : (n : Nat) → α n x : α (OfNat.ofNat 2) ⊢ f (OfNat.ofNat 2) = x @@ -39,12 +39,12 @@ example (α : Nat → Type) (f : (n : Nat) → α n) (x : α 2) : f (nat_lit 2) sorry /-- -info: x : Nat +trace: x : Nat f : Nat → Nat h : f (OfNat.ofNat 2) = x ⊢ f (OfNat.ofNat 2) = x --- -info: x : Nat +trace: x : Nat f : Nat → Nat h : f (OfNat.ofNat 2) = x ⊢ f 2 = x @@ -57,12 +57,12 @@ example (f : Nat → Nat) (h : f 2 = x) : f 2 = x := by assumption /-- -info: α : Nat → Type +trace: α : Nat → Type f : (n : Nat) → α n x : α (OfNat.ofNat 2) ⊢ f (OfNat.ofNat 2) = x --- -info: α : Nat → Type +trace: α : Nat → Type f : (n : Nat) → α n x : α (OfNat.ofNat 2) ⊢ f 2 = x diff --git a/tests/lean/run/2942.lean b/tests/lean/run/2942.lean index 8643f0e704..47af617383 100644 --- a/tests/lean/run/2942.lean +++ b/tests/lean/run/2942.lean @@ -6,7 +6,7 @@ The function `g` is "over-applied". Previously, conv-mode `congr` failed. -/ /-- -info: case a +trace: case a a b : Nat g : {α : Type} → α → α f : Nat → Nat @@ -40,19 +40,19 @@ While we are here, test `arg` too via `enter`. -/ /-- -info: a b : Nat +trace: a b : Nat g : {α : Type} → α → α f : Nat → Nat h : a = b | a --- -info: a b : Nat +trace: a b : Nat g : {α : Type} → α → α f : Nat → Nat h : a = b | f --- -info: a b : Nat +trace: a b : Nat g : {α : Type} → α → α f : Nat → Nat h : a = b diff --git a/tests/lean/run/3257.lean b/tests/lean/run/3257.lean index 9ade81163d..329c452aee 100644 --- a/tests/lean/run/3257.lean +++ b/tests/lean/run/3257.lean @@ -14,7 +14,7 @@ example : U := by simp [foo, T.mk] /-- -info: [Meta.Tactic.simp.discharge] bar discharge ✅️ +trace: [Meta.Tactic.simp.discharge] bar discharge ✅️ autoParam T _auto✝ [Meta.Tactic.simp.rewrite] T.mk:1000: T diff --git a/tests/lean/run/3467.lean b/tests/lean/run/3467.lean index d3df624172..d240bd4575 100644 --- a/tests/lean/run/3467.lean +++ b/tests/lean/run/3467.lean @@ -13,13 +13,13 @@ Basic diamond set_option structure.strictResolutionOrder true set_option trace.Elab.structure.resolutionOrder true -/-- info: [Elab.structure.resolutionOrder] computed resolution order: [A] -/ +/-- trace: [Elab.structure.resolutionOrder] computed resolution order: [A] -/ #guard_msgs in structure A -/-- info: [Elab.structure.resolutionOrder] computed resolution order: [B, A] -/ +/-- trace: [Elab.structure.resolutionOrder] computed resolution order: [B, A] -/ #guard_msgs in structure B extends A -/-- info: [Elab.structure.resolutionOrder] computed resolution order: [C, A] -/ +/-- trace: [Elab.structure.resolutionOrder] computed resolution order: [C, A] -/ #guard_msgs in structure C extends A -/-- info: [Elab.structure.resolutionOrder] computed resolution order: [D, B, C, A] -/ +/-- trace: [Elab.structure.resolutionOrder] computed resolution order: [D, B, C, A] -/ #guard_msgs in structure D extends B, C def A.x (a : A) : Bool := default @@ -55,7 +55,7 @@ Example resolution order failure warning: failed to compute strict resolution order: - parent 'B' must come after parent 'D' --- -info: [Elab.structure.resolutionOrder] computed resolution order: [D', B, D, C, A] +trace: [Elab.structure.resolutionOrder] computed resolution order: [D', B, D, C, A] -/ #guard_msgs in structure D' extends B, D @@ -67,17 +67,17 @@ Example from issue 3467. namespace Issue3467 -/-- info: [Elab.structure.resolutionOrder] computed resolution order: [Issue3467.X] -/ +/-- trace: [Elab.structure.resolutionOrder] computed resolution order: [Issue3467.X] -/ #guard_msgs in structure X where base : Nat -/-- info: [Elab.structure.resolutionOrder] computed resolution order: [Issue3467.A, Issue3467.X] -/ +/-- trace: [Elab.structure.resolutionOrder] computed resolution order: [Issue3467.A, Issue3467.X] -/ #guard_msgs in structure A extends X where countA : Nat -/-- info: [Elab.structure.resolutionOrder] computed resolution order: [Issue3467.B, Issue3467.X] -/ +/-- trace: [Elab.structure.resolutionOrder] computed resolution order: [Issue3467.B, Issue3467.X] -/ #guard_msgs in structure B extends X where countB : Nat @@ -95,7 +95,7 @@ def getTwiceCountB (b : B) := b.countB * 2 end B /-- -info: [Elab.structure.resolutionOrder] computed resolution order: [Issue3467.C, Issue3467.A, Issue3467.B, Issue3467.X] +trace: [Elab.structure.resolutionOrder] computed resolution order: [Issue3467.C, Issue3467.A, Issue3467.B, Issue3467.X] -/ #guard_msgs in structure C extends A, B @@ -112,20 +112,20 @@ end Issue3467 namespace Issue1881 -/-- info: [Elab.structure.resolutionOrder] computed resolution order: [Issue1881.Foo1] -/ +/-- trace: [Elab.structure.resolutionOrder] computed resolution order: [Issue1881.Foo1] -/ #guard_msgs in structure Foo1 where a : Nat b : Nat -/-- info: [Elab.structure.resolutionOrder] computed resolution order: [Issue1881.Foo2] -/ +/-- trace: [Elab.structure.resolutionOrder] computed resolution order: [Issue1881.Foo2] -/ #guard_msgs in structure Foo2 where a : Nat c : Nat /-- -info: [Elab.structure.resolutionOrder] computed resolution order: [Issue1881.Foo3, Issue1881.Foo1, Issue1881.Foo2] +trace: [Elab.structure.resolutionOrder] computed resolution order: [Issue1881.Foo3, Issue1881.Foo1, Issue1881.Foo2] -/ #guard_msgs in structure Foo3 extends Foo1, Foo2 where diff --git a/tests/lean/run/387.lean b/tests/lean/run/387.lean index 8934e4771a..2095597c7c 100644 --- a/tests/lean/run/387.lean +++ b/tests/lean/run/387.lean @@ -12,8 +12,8 @@ example : p 0 0 := by simp [foo 1] -- will not simplify simp [foo 0] -/-- info: ⊢ p 0 0 -/ -#guard_msgs in +/-- trace: ⊢ p 0 0 -/ +#guard_msgs (trace) in example : p 0 0 ∧ p 1 1 := by simp [foo 1] trace_state diff --git a/tests/lean/run/4171.lean b/tests/lean/run/4171.lean index 37c98842ad..a73c49603d 100644 --- a/tests/lean/run/4171.lean +++ b/tests/lean/run/4171.lean @@ -13,7 +13,7 @@ universe v u variable (α : Sort u) -structure Opposite := +structure Opposite where op :: unop : α @@ -714,7 +714,7 @@ example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where /-- -info: [simp] Diagnostics +trace: [simp] Diagnostics [simp] theorems with bad keys [simp] foo, key: @Quiver.Hom.unop _ _ _ _ (@Opposite.op (@Quiver.Hom _ _ _.1 _.1) _) use `set_option diagnostics.threshold ` to control threshold for reporting counters @@ -735,7 +735,7 @@ example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where attribute [simp] foo /-- -info: [simp] Diagnostics +trace: [simp] Diagnostics [simp] theorems with bad keys [simp] foo, key: @Quiver.Hom.unop _ _ _ _ (@Opposite.op (@Quiver.Hom _ _ _.1 _.1) _) use `set_option diagnostics.threshold ` to control threshold for reporting counters diff --git a/tests/lean/run/4339.lean b/tests/lean/run/4339.lean index bd829197f5..e0952caa24 100644 --- a/tests/lean/run/4339.lean +++ b/tests/lean/run/4339.lean @@ -7,7 +7,7 @@ structure HH (A B : Nat) where set_option pp.explicit true /-- -info: S T f : Nat +trace: S T f : Nat ⊢ @Eq (HH S T) (@HH.mk S T f trivial) (@id (HH S T) (@HH.mk S T f trivial)) -/ #guard_msgs in @@ -18,7 +18,7 @@ example {S T : Nat} (f : Nat) : rfl /-- -info: S T f : Nat +trace: S T f : Nat ⊢ @Eq (HH S T) (@HH.mk S T f trivial) (@id (HH S T) (@HH.mk S T f trivial)) -/ #guard_msgs in @@ -29,7 +29,7 @@ example {S T : Nat} (f : Nat) : rfl /-- -info: S T f : Nat +trace: S T f : Nat ⊢ @Eq (HH S T) (@HH.mk S T f trivial) (@id (HH S T) (@HH.mk S T f trivial)) -/ #guard_msgs in diff --git a/tests/lean/run/4381.lean b/tests/lean/run/4381.lean index 967e7360ab..0a6ed99d33 100644 --- a/tests/lean/run/4381.lean +++ b/tests/lean/run/4381.lean @@ -1,5 +1,5 @@ /-- -info: case h +trace: case h d g : Nat H1 : d = g ⊢ ?w = g diff --git a/tests/lean/run/4390.lean b/tests/lean/run/4390.lean index 5e10f4c31c..81153c3867 100644 --- a/tests/lean/run/4390.lean +++ b/tests/lean/run/4390.lean @@ -24,7 +24,7 @@ p : p = state --- -info: [split.failure] `split` tactic failed to generalize discriminant(s) at +trace: [split.failure] `split` tactic failed to generalize discriminant(s) at match h : step state with | none => [state] | some newState => state :: countdown newState diff --git a/tests/lean/run/5064.lean b/tests/lean/run/5064.lean index 6df9de8622..f6f47151df 100644 --- a/tests/lean/run/5064.lean +++ b/tests/lean/run/5064.lean @@ -13,7 +13,7 @@ def thingy : List (Nat ⊕ Nat) → List Bool | _ => [] termination_by l => l.length -/-- info: ⊢ [] = [] -/ +/-- trace: ⊢ [] = [] -/ #guard_msgs in theorem thingy_empty : thingy [] = [] := by unfold thingy diff --git a/tests/lean/run/790.lean b/tests/lean/run/790.lean index 85db1d6264..e0d88bbe31 100644 --- a/tests/lean/run/790.lean +++ b/tests/lean/run/790.lean @@ -16,7 +16,7 @@ instance : Vec' Nat := ⟨⟩ set_option trace.Meta.Tactic.simp true /-- -info: [Meta.Tactic.simp.rewrite] differential_of_linear:1000: +trace: [Meta.Tactic.simp.rewrite] differential_of_linear:1000: differential f x dx ==> f dx diff --git a/tests/lean/run/8049.lean b/tests/lean/run/8049.lean index d9c448f61f..1cae85f64e 100644 --- a/tests/lean/run/8049.lean +++ b/tests/lean/run/8049.lean @@ -25,13 +25,11 @@ elab "test" : tactic => do levelParams := [] } -/-- -info: [Elab.debug] traced --/ +/-- trace: [Elab.debug] traced -/ #guard_msgs in theorem f1 : True := by test; trivial -/-- info: [Elab.debug] traced -/ +/-- trace: [Elab.debug] traced -/ #guard_msgs in def f2 : True := by test; trivial diff --git a/tests/lean/run/CompilerCSE.lean b/tests/lean/run/CompilerCSE.lean index a7647c089f..dff84f3c81 100644 --- a/tests/lean/run/CompilerCSE.lean +++ b/tests/lean/run/CompilerCSE.lean @@ -15,7 +15,7 @@ def cseSizeTest : PassInstaller := set_option trace.Compiler.test true in /-- -info: [Compiler.test] Starting wrapper test cseSizeLeq for cse occurrence 0 +trace: [Compiler.test] Starting wrapper test cseSizeLeq for cse occurrence 0 [Compiler.test] Wrapper test cseSizeLeq for cse occurrence 0 successful [Compiler.test] Starting post condition test cseFix for cse occurrence 0 [Compiler.test] Post condition test cseFix for cse occurrence 0 successful diff --git a/tests/lean/run/CompilerFindJoinPoints.lean b/tests/lean/run/CompilerFindJoinPoints.lean index 75cd6cc079..2b60804f60 100644 --- a/tests/lean/run/CompilerFindJoinPoints.lean +++ b/tests/lean/run/CompilerFindJoinPoints.lean @@ -15,7 +15,7 @@ def cseSizeTest : PassInstaller := set_option trace.Compiler.test true in /-- -info: [Compiler.test] Starting wrapper test findJoinPointsSizeLeq for findJoinPoints occurrence 0 +trace: [Compiler.test] Starting wrapper test findJoinPointsSizeLeq for findJoinPoints occurrence 0 [Compiler.test] Wrapper test findJoinPointsSizeLeq for findJoinPoints occurrence 0 successful [Compiler.test] Starting post condition test findJoinPointsFix for findJoinPoints occurrence 0 [Compiler.test] Post condition test findJoinPointsFix for findJoinPoints occurrence 0 successful diff --git a/tests/lean/run/CompilerFloatLetIn.lean b/tests/lean/run/CompilerFloatLetIn.lean index 1b609b5c44..86f6f20220 100644 --- a/tests/lean/run/CompilerFloatLetIn.lean +++ b/tests/lean/run/CompilerFloatLetIn.lean @@ -16,7 +16,7 @@ def floatLetInSizeTest : PassInstaller := set_option trace.Compiler.test true in /-- -info: [Compiler.test] Starting wrapper test floatLetInSizeEq for floatLetIn occurrence 0 +trace: [Compiler.test] Starting wrapper test floatLetInSizeEq for floatLetIn occurrence 0 [Compiler.test] Wrapper test floatLetInSizeEq for floatLetIn occurrence 0 successful [Compiler.test] Starting wrapper test floatLetInSizeEq for floatLetIn occurrence 1 [Compiler.test] Wrapper test floatLetInSizeEq for floatLetIn occurrence 1 successful diff --git a/tests/lean/run/CompilerPullInstances.lean b/tests/lean/run/CompilerPullInstances.lean index f9d2de0e0e..0582ce3991 100644 --- a/tests/lean/run/CompilerPullInstances.lean +++ b/tests/lean/run/CompilerPullInstances.lean @@ -15,7 +15,7 @@ def pullInstancesSizeTest : PassInstaller := set_option trace.Compiler.test true in /-- -info: [Compiler.test] Starting wrapper test pullInstancesSizeEq for pullInstances occurrence 0 +trace: [Compiler.test] Starting wrapper test pullInstancesSizeEq for pullInstances occurrence 0 [Compiler.test] Wrapper test pullInstancesSizeEq for pullInstances occurrence 0 successful [Compiler.test] Starting post condition test pullInstancesFix for pullInstances occurrence 0 [Compiler.test] Post condition test pullInstancesFix for pullInstances occurrence 0 successful diff --git a/tests/lean/run/CompilerSimp.lean b/tests/lean/run/CompilerSimp.lean index 1f6099f000..bea661e184 100644 --- a/tests/lean/run/CompilerSimp.lean +++ b/tests/lean/run/CompilerSimp.lean @@ -15,7 +15,7 @@ def simpReaderTest : PassInstaller := set_option trace.Compiler.test true in /-- -info: [Compiler.test] Starting post condition test simpInlinesBinds for simp occurrence 0 +trace: [Compiler.test] Starting post condition test simpInlinesBinds for simp occurrence 0 [Compiler.test] Post condition test simpInlinesBinds for simp occurrence 0 successful [Compiler.test] Starting post condition test simpFix for simp occurrence 0 [Compiler.test] Post condition test simpFix for simp occurrence 0 successful diff --git a/tests/lean/run/ack.lean b/tests/lean/run/ack.lean index 021094014c..fdbfde718b 100644 --- a/tests/lean/run/ack.lean +++ b/tests/lean/run/ack.lean @@ -5,21 +5,21 @@ def ack : Nat → Nat → Nat termination_by a b => (a, b) /-- -info: [diag] Diagnostics +trace: [diag] Diagnostics [kernel] unfolded declarations (max: 147, num: 3): [kernel] OfNat.ofNat ↦ 147 [kernel] Add.add ↦ 61 [kernel] HAdd.hAdd ↦ 61 use `set_option diagnostics.threshold ` to control threshold for reporting counters --- -info: [simp] Diagnostics +trace: [simp] Diagnostics [simp] used theorems (max: 59, num: 1): [simp] ack.eq_3 ↦ 59 [simp] tried theorems (max: 59, num: 1): [simp] ack.eq_3 ↦ 59, succeeded: 59 use `set_option diagnostics.threshold ` to control threshold for reporting counters --- -info: [diag] Diagnostics +trace: [diag] Diagnostics [kernel] unfolded declarations (max: 147, num: 3): [kernel] OfNat.ofNat ↦ 147 [kernel] Add.add ↦ 61 diff --git a/tests/lean/run/allGoals.lean b/tests/lean/run/allGoals.lean index 5e0e82337d..e22071c184 100644 --- a/tests/lean/run/allGoals.lean +++ b/tests/lean/run/allGoals.lean @@ -12,7 +12,7 @@ open Lean Elab Tactic Tactics may assign other goals. There are three goals, but the tactic is run twice. -/ /-- -info: case a +trace: case a ⊢ 1 ≤ ?m case a @@ -21,7 +21,7 @@ case a case m ⊢ Nat --- -info: running tac +trace: running tac running tac -/ #guard_msgs in @@ -94,7 +94,7 @@ case refine_1 b : Bool ⊢ Unit --- -info: case refine_2.false +trace: case refine_2.false v : Unit := ?_ false ⊢ True @@ -149,7 +149,7 @@ error: Case tag 'true' not found. The only available case tag is 'refine_1'. --- -info: case refine_2.false +trace: case refine_2.false v : Unit := () this : () = v ⊢ True @@ -160,7 +160,7 @@ case refine_1 b : Bool ⊢ Unit --- -info: in true +trace: in true -/ #guard_msgs in example (b : Bool) : True := by @@ -200,7 +200,7 @@ This is the responsibility of `first`, but `all_goals` coordinates by being sure -/ /-- -info: rfl +trace: rfl rfl -/ #guard_msgs in @@ -311,7 +311,7 @@ theorem idEq (a : α) : id a = a := rfl /-- -info: case sunday +trace: case sunday ⊢ sunday.previous.next = id sunday case monday @@ -332,7 +332,7 @@ case friday case saturday ⊢ saturday.previous.next = id saturday --- -info: case sunday +trace: case sunday ⊢ sunday.previous.next = sunday case monday @@ -362,7 +362,7 @@ theorem Weekday.test (d : Weekday) : next (previous d) = id d := by all_goals rfl /-- -info: case sunday +trace: case sunday ⊢ sunday.previous.next = sunday case monday diff --git a/tests/lean/run/apply_tac.lean b/tests/lean/run/apply_tac.lean index 0ad662e6d8..0c2ab0bf9e 100644 --- a/tests/lean/run/apply_tac.lean +++ b/tests/lean/run/apply_tac.lean @@ -5,7 +5,7 @@ open Lean.Meta open Lean.Elab.Tactic /-- -info: a b c : Nat +trace: a b c : Nat h₁ : a = b h₂ : b = c ⊢ a = b @@ -17,7 +17,7 @@ example (a b c : Nat) (h₁ : a = b) (h₂ : b = c) : a = c := by exact h₁ /-- -info: case h +trace: case h a : Nat ⊢ ?w = a @@ -38,7 +38,7 @@ elab "eapply " e:term : tactic => evalApplyLikeTactic (MVarId.apply (cfg := {newGoals := ApplyNewGoals.nonDependentOnly})) e /-- -info: case h +trace: case h a : Nat ⊢ ?w = a -/ @@ -49,7 +49,7 @@ example (a : Nat) : ∃ x, x = a := by rfl /-- -info: case w +trace: case w a : Nat ⊢ Nat @@ -57,7 +57,7 @@ case h a : Nat ⊢ ?w = a --- -info: case h +trace: case h a : Nat ⊢ a = a -/ diff --git a/tests/lean/run/autoboundIssues.lean b/tests/lean/run/autoboundIssues.lean index afcd15a3cc..ae5a1e96ca 100644 --- a/tests/lean/run/autoboundIssues.lean +++ b/tests/lean/run/autoboundIssues.lean @@ -39,7 +39,7 @@ The auto-bound implicit creates a new variable `A✝`, which comes from the argu (This has been the case well before the creation of this test.) -/ /-- -info: A✝ : Sort u_1 +trace: A✝ : Sort u_1 a : A✝ _x : constUnit a ⊢ True @@ -66,7 +66,7 @@ The duplication was because `runTermElabM` wasn't resetting the local context. The poor variable name was due to using `mkForallFVars` instead of `mkForallFVars'`. -/ /-- -info: A✝ : Sort _ +trace: A✝ : Sort _ a : A✝ x : constUnit a ⊢ True @@ -82,7 +82,7 @@ Checking that `#check` also has the improvement. /-- info: 1 : Nat --- -info: A✝ : Sort _ +trace: A✝ : Sort _ a : A✝ x : constUnit a ⊢ ?_ diff --git a/tests/lean/run/binderNameHint.lean b/tests/lean/run/binderNameHint.lean index 084bb48469..cd4cbbe717 100644 --- a/tests/lean/run/binderNameHint.lean +++ b/tests/lean/run/binderNameHint.lean @@ -84,7 +84,7 @@ error: unsolved goals names : List String ⊢ (!names.any fun x => !"Waldo".isPrefixOf x) = true --- -info: names : List String +trace: names : List String ⊢ (!names.any fun x => binderNameHint x (fun name => "Waldo".isPrefixOf name) !"Waldo".isPrefixOf x) = true -/ #guard_msgs in diff --git a/tests/lean/run/binderNameHintSimp.lean b/tests/lean/run/binderNameHintSimp.lean index 137af94fc3..5aaa13178e 100644 --- a/tests/lean/run/binderNameHintSimp.lean +++ b/tests/lean/run/binderNameHintSimp.lean @@ -12,7 +12,7 @@ def z : Nat := 0 set_option trace.Meta.Tactic.simp.rewrite true /-- -info: [Meta.Tactic.simp.rewrite] ↓ binderNameHint.eq_1:1000: +trace: [Meta.Tactic.simp.rewrite] ↓ binderNameHint.eq_1:1000: binderNameHint x y z ==> z @@ -24,7 +24,7 @@ example : binderNameHint x y z = 0 := by simp [x, y, z] /-- -info: [Meta.Tactic.simp.rewrite] ↓ binderNameHint.eq_1:1000: +trace: [Meta.Tactic.simp.rewrite] ↓ binderNameHint.eq_1:1000: binderNameHint x y z ==> z diff --git a/tests/lean/run/canonM_exists_fun.lean b/tests/lean/run/canonM_exists_fun.lean index 3d9f1e0ec5..e1e45b0279 100644 --- a/tests/lean/run/canonM_exists_fun.lean +++ b/tests/lean/run/canonM_exists_fun.lean @@ -12,7 +12,7 @@ elab "foo" t:term : tactic => do #check (∃ f : Nat → Nat, ∀ x, f x = 0) -- works fine /-- -info: [debug] canonicalizing ∃ f, ∀ (x : Nat), f x = 0 +trace: [debug] canonicalizing ∃ f, ∀ (x : Nat), f x = 0 [debug] canonicalized it to ∃ f, ∀ (x : Nat), f x = 0 -/ #guard_msgs in diff --git a/tests/lean/run/cdotAtSimpArg.lean b/tests/lean/run/cdotAtSimpArg.lean index da00e88224..ca157f90be 100644 --- a/tests/lean/run/cdotAtSimpArg.lean +++ b/tests/lean/run/cdotAtSimpArg.lean @@ -6,7 +6,7 @@ example : ¬ true = false := by /-! Test `binop%` -/ /-- -info: y x : Nat +trace: y x : Nat h : y = 0 ⊢ Add.add x y = x -/ @@ -19,7 +19,7 @@ example (h : y = 0) : x + y = x := by done /-- -info: y x : Nat +trace: y x : Nat h : y = 0 ⊢ Add.add x y = x -/ diff --git a/tests/lean/run/change.lean b/tests/lean/run/change.lean index 4f5d9eb00e..375679db1d 100644 --- a/tests/lean/run/change.lean +++ b/tests/lean/run/change.lean @@ -85,7 +85,7 @@ is not definitionally equal to target `change` can create new metavariables and assign them -/ /-- -info: x y z : Nat +trace: x y z : Nat w : Nat := x + y ⊢ x + y = z -/ @@ -114,7 +114,7 @@ example : let x := 22; let y : Nat := x; let z : Fin (y + 1) := 0; z.1 < y + 1 : `change` reorders hypotheses if necessary -/ /-- -info: x y z w : Nat +trace: x y z w : Nat a : Nat := x + y h : a = z + w ⊢ True @@ -199,7 +199,7 @@ example (m n : Nat) : m + 2 = n := by conv `change` to create a metavariable -/ /-- -info: a b c d : Nat +trace: a b c d : Nat e : Nat := a + b ⊢ a + b + c = d -/ diff --git a/tests/lean/run/closure1.lean b/tests/lean/run/closure1.lean index 743f0d8db4..8396423e37 100644 --- a/tests/lean/run/closure1.lean +++ b/tests/lean/run/closure1.lean @@ -41,7 +41,7 @@ printDef `foo1 set_option pp.mvars false in /-- -info: [Meta.debug] foo1 α f b ?_ ?_ +trace: [Meta.debug] foo1 α f b ?_ ?_ [Meta.debug] fun α f b _x_1 _x_2 => _x_2 (f b) -/ #guard_msgs in @@ -63,7 +63,7 @@ printDef `foo2 set_option pp.mvars false in /-- -info: [Meta.debug] foo2 α v1 v2 p ?_ +trace: [Meta.debug] foo2 α v1 v2 p ?_ [Meta.debug] fun α v1 v2 p _x_1 => v1 = v2 ∧ (_x_1 v2 ∨ p) -/ #guard_msgs in diff --git a/tests/lean/run/coeAttrs.lean b/tests/lean/run/coeAttrs.lean index f2495cc81d..b3970f4558 100644 --- a/tests/lean/run/coeAttrs.lean +++ b/tests/lean/run/coeAttrs.lean @@ -4,7 +4,7 @@ -- With the option off (default) /-- -info: n : Nat +trace: n : Nat h : n = 0 ⊢ ↑n = 0 -/ @@ -15,7 +15,7 @@ example (n : Nat) (h : n = 0) : (↑n : Int) = 0 := by -- With the option on /-- -info: n : Nat +trace: n : Nat h : n = 0 ⊢ (↑n : Int) = 0 -/ diff --git a/tests/lean/run/conv1.lean b/tests/lean/run/conv1.lean index 86b1aa9626..81014aec1f 100644 --- a/tests/lean/run/conv1.lean +++ b/tests/lean/run/conv1.lean @@ -3,7 +3,7 @@ set_option pp.analyze false def p (x y : Nat) := x = y /-- -info: x y : Nat +trace: x y : Nat ⊢ x + y = y.add x -/ #guard_msgs in @@ -18,7 +18,7 @@ example (x y : Nat) : p (x + y) (y + x + 0) := by rfl /-- -info: x y : Nat +trace: x y : Nat ⊢ x + y = y.add x -/ #guard_msgs in @@ -32,7 +32,7 @@ example (x y : Nat) : p (x + y) (y + x + 0) := by rfl /-- -info: x y : Nat +trace: x y : Nat ⊢ x.add y = y.add x -/ #guard_msgs in @@ -48,7 +48,7 @@ example (x y : Nat) : p (x + y) (y + x + 0) := by apply Nat.add_comm x y /-- -info: x y : Nat +trace: x y : Nat | x + y -/ #guard_msgs in @@ -109,14 +109,14 @@ example (h₁ : f x = x + 1) (h₂ : x > 0) : f x = f x := by exact h₁ /-- -info: x y : Nat +trace: x y : Nat f : Nat → Nat → Nat g : Nat → Nat h₁ : ∀ (z : Nat), f z z = z h₂ : ∀ (x y : Nat), f (g x) (g y) = y ⊢ f (g (0 + y)) (f (g x) (g x)) = x --- -info: x y : Nat +trace: x y : Nat f : Nat → Nat → Nat g : Nat → Nat h₁ : ∀ (z : Nat), f z z = z @@ -133,7 +133,7 @@ example (x y : Nat) (f : Nat → Nat → Nat) (g : Nat → Nat) (h₁ : ∀ z, f set_option linter.unusedVariables false /-- -info: x y : Nat +trace: x y : Nat f : Nat → Nat → Nat g : Nat → Nat h₁ : ∀ (z : Nat), f z z = z @@ -141,7 +141,7 @@ h₂ : ∀ (x y : Nat), f (g x) (g y) = y h₃ : f (g x) (g x) = 0 ⊢ g x = 0 --- -info: x y : Nat +trace: x y : Nat f : Nat → Nat → Nat g : Nat → Nat h₁ : ∀ (z : Nat), f z z = z diff --git a/tests/lean/run/conv_arg.lean b/tests/lean/run/conv_arg.lean index 6e6cf576bb..bb38eeca29 100644 --- a/tests/lean/run/conv_arg.lean +++ b/tests/lean/run/conv_arg.lean @@ -30,10 +30,10 @@ example (p q₁ q₂ : Prop) (h : q₁ ↔ q₂) : (p → q₁) ↔ (p → q₂) -- Dependent implications /-- -info: i✝ : Nat +trace: i✝ : Nat | i✝ < 10 --- -info: a✝¹ : Nat +trace: a✝¹ : Nat a✝ : a✝¹ < 10 | ↑⟨a✝¹, ⋯⟩ = a✝¹ -/ diff --git a/tests/lean/run/core.lean b/tests/lean/run/core.lean index bf8fa849b3..6816706ee4 100644 --- a/tests/lean/run/core.lean +++ b/tests/lean/run/core.lean @@ -29,7 +29,7 @@ testing... --- info: 10 --- -info: [Elab] trace message +trace: [Elab] trace message -/ #guard_msgs in #eval f diff --git a/tests/lean/run/declareConfigElabBug.lean b/tests/lean/run/declareConfigElabBug.lean index 818f399dc0..b6d426d96b 100644 --- a/tests/lean/run/declareConfigElabBug.lean +++ b/tests/lean/run/declareConfigElabBug.lean @@ -1,6 +1,6 @@ set_option trace.Elab true /-- -info: α✝ : Sort u_1 +trace: α✝ : Sort u_1 a b : α✝ h : a = b ⊢ (fun x => x) a = b diff --git a/tests/lean/run/diagRec.lean b/tests/lean/run/diagRec.lean index f93bec0da0..ab58f07d87 100644 --- a/tests/lean/run/diagRec.lean +++ b/tests/lean/run/diagRec.lean @@ -8,7 +8,7 @@ termination_by n /-- info: 89 --- -info: [diag] Diagnostics +trace: [diag] Diagnostics [reduction] unfolded declarations (max: 407, num: 3): [reduction] Nat.rec ↦ 407 [reduction] Or.rec ↦ 144 diff --git a/tests/lean/run/diagnostics.lean b/tests/lean/run/diagnostics.lean index ccd158ee0c..4f88e00a3b 100644 --- a/tests/lean/run/diagnostics.lean +++ b/tests/lean/run/diagnostics.lean @@ -9,7 +9,7 @@ theorem f_eq : f (x + 1) = q (f x) := rfl set_option trace.Meta.debug true /-- -info: [diag] Diagnostics +trace: [diag] Diagnostics [reduction] unfolded declarations (max: 15, num: 6): [reduction] Nat.rec ↦ 15 [reduction] Add.add ↦ 10 @@ -30,7 +30,7 @@ example : f (x + 5) = q (q (q (q (q (f x))))) := rfl /-- -info: [diag] Diagnostics +trace: [diag] Diagnostics [reduction] unfolded declarations (max: 15, num: 6): [reduction] Nat.rec ↦ 15 [reduction] Add.add ↦ 10 diff --git a/tests/lean/run/dsimp1.lean b/tests/lean/run/dsimp1.lean index dbb54e3dad..1629e65b09 100644 --- a/tests/lean/run/dsimp1.lean +++ b/tests/lean/run/dsimp1.lean @@ -7,7 +7,7 @@ axiom P : Bool → Prop axiom P_false : P false /-- -info: x : Nat +trace: x : Nat ⊢ P (1 + x).isZero -/ #guard_msgs in diff --git a/tests/lean/run/dsimp_bv_simproc.lean b/tests/lean/run/dsimp_bv_simproc.lean index 90560ac72b..2108982343 100644 --- a/tests/lean/run/dsimp_bv_simproc.lean +++ b/tests/lean/run/dsimp_bv_simproc.lean @@ -10,7 +10,7 @@ theorem write_simplify_test_0 (a x y : BitVec 64) simp only [setWidth_eq, BitVec.cast_eq] /-- -info: write : (n : Nat) → BitVec 64 → BitVec (n * 8) → Type → Type +trace: write : (n : Nat) → BitVec 64 → BitVec (n * 8) → Type → Type s aux : Type a x y : BitVec 64 h : 128 = 128 diff --git a/tests/lean/run/elab_cmd.lean b/tests/lean/run/elab_cmd.lean index aa4030e69e..d9f408c135 100644 --- a/tests/lean/run/elab_cmd.lean +++ b/tests/lean/run/elab_cmd.lean @@ -26,7 +26,7 @@ elab "try" t:tactic : tactic => do set_option linter.unusedVariables false /-- -info: case h₁ +trace: case h₁ x y z : Nat h1 : y = z h2 : x = x @@ -47,7 +47,7 @@ h2 : x = x h3 : x = y ⊢ Nat --- -info: case h₂ +trace: case h₂ x y z : Nat h1 : y = z h2 : x = x diff --git a/tests/lean/run/emptyLcnf.lean b/tests/lean/run/emptyLcnf.lean index 80b7375022..2c5acd8dc1 100644 --- a/tests/lean/run/emptyLcnf.lean +++ b/tests/lean/run/emptyLcnf.lean @@ -7,7 +7,7 @@ def f (x : MyEmpty) : Nat := set_option trace.Compiler.result true /-- -info: [Compiler.result] size: 0 +trace: [Compiler.result] size: 0 def f x : Nat := ⊥ -/ diff --git a/tests/lean/run/eqnsAtSimp3.lean b/tests/lean/run/eqnsAtSimp3.lean index 6ea1b606f1..49075cb456 100644 --- a/tests/lean/run/eqnsAtSimp3.lean +++ b/tests/lean/run/eqnsAtSimp3.lean @@ -6,7 +6,7 @@ def f (x y : Nat) : Nat := | x+1, y => 2 * f x y /-- -info: x y : Nat +trace: x y : Nat h : y ≠ 5 ⊢ ∃ z, 2 * f x y = 2 * z -/ @@ -25,7 +25,7 @@ theorem ex1 (x : Nat) (y : Nat) (h : y ≠ 5) : ∃ z, f (x+1) y = 2 * z := by | x+1, y => 2 * g x y /-- -info: x y : Nat +trace: x y : Nat h : y ≠ 5 ⊢ ∃ z, 2 * g x y = 2 * z -/ @@ -37,7 +37,7 @@ theorem ex2 (x : Nat) (y : Nat) (h : y ≠ 5) : ∃ z, g (x+1) y = 2 * z := by rfl /-- -info: x y : Nat +trace: x y : Nat h : y = 5 → False ⊢ ∃ z, 2 * f x y = 2 * z -/ @@ -59,7 +59,7 @@ theorem ex3 (x : Nat) (y : Nat) (h : y = 5 → False) : ∃ z, f (x+1) y = 2 * z #check f2.eq_4 /-- -info: x y z : Nat +trace: x y z : Nat h : y = 5 → z = 6 → False ⊢ ∃ w, 2 * f2 x y z = 2 * w -/ diff --git a/tests/lean/run/erased.lean b/tests/lean/run/erased.lean index 642da1d034..3262dc0526 100644 --- a/tests/lean/run/erased.lean +++ b/tests/lean/run/erased.lean @@ -20,7 +20,7 @@ set_option pp.funBinderTypes true set_option pp.letVarTypes true set_option trace.Compiler.result true /-- -info: [Compiler.result] size: 1 +trace: [Compiler.result] size: 1 def Erased.mk (α : lcErased) (a : lcAny) : PSigma lcErased lcAny := let _x.1 : PSigma lcErased lcAny := PSigma.mk lcErased ◾ ◾ ◾; return _x.1 diff --git a/tests/lean/run/exposeNames.lean b/tests/lean/run/exposeNames.lean index 186ae3835a..c53da13fa2 100644 --- a/tests/lean/run/exposeNames.lean +++ b/tests/lean/run/exposeNames.lean @@ -1,5 +1,5 @@ /-- -info: α : Type u_1 +trace: α : Type u_1 inst : DecidableEq α inst_1 : Add α a_1 b_1 : α @@ -9,14 +9,14 @@ h_1 : b = a_2 a : α ⊢ a = b -/ -#guard_msgs (info) in +#guard_msgs (trace) in example [DecidableEq α] [Add α] (a b : α) (_ : a = b) (a : α) (b : α) (_ : b = a) (a : α) : a = b := by expose_names trace_state sorry /-- -info: α : Sort u_1 +trace: α : Sort u_1 a b : α h_1 : a = b h_2 : True @@ -24,14 +24,14 @@ h_3 : True ∨ False h : b = a ⊢ b = a -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (a b : α) (h : a = b) (_ : True) (_ : True ∨ False) (h : b = a) : b = a := by expose_names trace_state rw [h] /-- -info: α : Sort u_1 +trace: α : Sort u_1 a b : α h : a = b h_3 : True @@ -41,7 +41,7 @@ h_5 : True h_2 : b = a ⊢ b = a -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (a b : α) (h : a = b) (_ : True) (_ : False) (h_1 : True ∨ False) (_ : True) (h_2 : b = a) : b = a := by expose_names trace_state diff --git a/tests/lean/run/extract_lets.lean b/tests/lean/run/extract_lets.lean index 54df22882c..1a815edf9e 100644 --- a/tests/lean/run/extract_lets.lean +++ b/tests/lean/run/extract_lets.lean @@ -10,7 +10,7 @@ axiom test_sorry {α : Sort _} : α Extract a top-level let, no names given. -/ /-- -info: x✝ : Nat := 2 +trace: x✝ : Nat := 2 ⊢ x✝ = 2 -/ #guard_msgs in @@ -23,7 +23,7 @@ example : let x := 2; x = 2 := by Extract a top-level let, name given. -/ /-- -info: z : Nat := 2 +trace: z : Nat := 2 ⊢ z = 2 -/ #guard_msgs in @@ -36,7 +36,7 @@ example : let x := 2; x = 2 := by Extract a top-level let, placeholder name given. -/ /-- -info: x✝ : Nat := 2 +trace: x✝ : Nat := 2 ⊢ x✝ = 2 -/ #guard_msgs in @@ -49,7 +49,7 @@ example : let x := 2; x = 2 := by Extract an embedded let, name given. -/ /-- -info: z : Nat := 2 +trace: z : Nat := 2 ⊢ z = 2 -/ #guard_msgs in @@ -62,7 +62,7 @@ example : (let x := 2; x) = 2 := by Extract multiple embedded lets, no names given. -/ /-- -info: x✝ : Nat := 2 +trace: x✝ : Nat := 2 y✝ : Nat := 1 + 1 ⊢ x✝ = y✝ -/ @@ -76,7 +76,7 @@ example : (let x := 2; x) = (let y := 1 + 1; y) := by Names extracted lets in order, but keeps extracting even after list is exhausted. -/ /-- -info: z : Nat := 2 +trace: z : Nat := 2 y✝ : Nat := 1 + 1 ⊢ z = y✝ -/ @@ -93,7 +93,7 @@ Too many names, linter warning. warning: unused name note: this linter can be disabled with `set_option linter.tactic.unusedName false` --- -info: z : Nat := 2 +trace: z : Nat := 2 z' : Nat := 1 + 1 ⊢ z = z' -/ @@ -107,7 +107,7 @@ example : (let x := 2; x) = (let y := 1 + 1; y) := by Length of name list controls number of lets in `+onlyGivenNames` mode. -/ /-- -info: z : Nat := 2 +trace: z : Nat := 2 ⊢ z = let y := 1 + 1; y @@ -118,7 +118,7 @@ example : (let x := 2; x) = (let y := 1 + 1; y) := by trace_state rfl /-- -info: z : Nat := 2 +trace: z : Nat := 2 w : Nat := 1 + 1 ⊢ z = w -/ @@ -132,7 +132,7 @@ example : (let x := 2; x) = (let y := 1 + 1; y) := by Merging. -/ /-- -info: x✝ : Nat := 2 +trace: x✝ : Nat := 2 ⊢ x✝ = x✝ -/ #guard_msgs in @@ -145,7 +145,7 @@ example : (let x := 2; x) = (let y := 2; y) := by Merging, even if we run out of names. -/ /-- -info: z : Nat := 2 +trace: z : Nat := 2 ⊢ z = z -/ #guard_msgs in @@ -158,7 +158,7 @@ example : (let x := 2; x) = (let y := 2; y) := by Merging reuses pre-existing declarations -/ /-- -info: z : Nat := 2 +trace: z : Nat := 2 ⊢ z = z -/ #guard_msgs in @@ -172,7 +172,7 @@ example : (let x := 2; x) = (let y := 2; y) := by Merging doesn't reuse pre-existing declarations when `-useContext`. -/ /-- -info: z : Nat := 2 +trace: z : Nat := 2 x✝ : Nat := 2 ⊢ x✝ = x✝ -/ @@ -187,7 +187,7 @@ example : (let x := 2; x) = (let y := 2; y) := by Works with `have` (`let_fun`) -/ /-- -info: a✝ : Nat := 2 +trace: a✝ : Nat := 2 x✝ : Nat := a✝ y✝ : Nat := a✝ + 0 ⊢ x✝ = y✝ @@ -202,7 +202,7 @@ example : have a := 2; (have x := a; x) = (have y := a + 0; y) := by Extracts at both the type and the value of a local definition. -/ /-- -info: α✝ : Type := Nat +trace: α✝ : Type := Nat y✝ : Nat := 2 x : α✝ := 2 ⊢ x = x @@ -215,7 +215,7 @@ example : let x : (let α := Nat; α) := (let y := 2; 2); x = x := by rfl -- Essentially same state: /-- -info: α✝ : Type := Nat +trace: α✝ : Type := Nat y✝ : Nat := 2 x✝ : α✝ := 2 ⊢ x✝ = x✝ @@ -230,7 +230,7 @@ example : let x : (let α := Nat; α) := (let y := 2; 2); x = x := by Basic `descend := false` test. -/ /-- -info: x✝ : Nat := 2 +trace: x✝ : Nat := 2 ⊢ x✝ = 2 -/ #guard_msgs in @@ -243,7 +243,7 @@ example : let x := 2; x = 2 := by Make sure `descend := false` is not obstructed by metadata. -/ /-- -info: this : True +trace: this : True x✝ : Nat := 2 ⊢ x✝ = 2 -/ @@ -271,7 +271,7 @@ example : (let x := 2; x) = 2 := by In `-descend` mode, merges using pre-existing declarations. -/ /-- -info: w : Nat := 2 +trace: w : Nat := 2 y✝ : Nat := 3 ⊢ w = 2 + y✝ - y✝ -/ @@ -286,7 +286,7 @@ example : let x := 2; let y := 3; let z := 3; x = 2 + y - z := by `-descend` works with `have` (`let_fun`) -/ /-- -info: a✝ : Nat := 2 +trace: a✝ : Nat := 2 ⊢ (let_fun x := a✝; x) = let_fun y := a✝ + 0; @@ -302,7 +302,7 @@ example : have a := 2; (have x := a; x) = (have y := a + 0; y) := by Extracting at a hypothesis -/ /-- -info: x✝ : Nat := 1 +trace: x✝ : Nat := 1 h : x✝ = x✝ ⊢ True -/ @@ -317,7 +317,7 @@ example (h : let x := 1; x = x) : True := by Extracting at a hypothesis, with names -/ /-- -info: y : Nat := 1 +trace: y : Nat := 1 h : y = y ⊢ True -/ @@ -332,7 +332,7 @@ example (h : let x := 1; x = x) : True := by Extracting at a hypothesis, reorders hypotheses -/ /-- -info: h' : Nat +trace: h' : Nat y : Nat := 1 h : y = y ⊢ True @@ -348,7 +348,7 @@ example (h : let x := 1; x = x) (h' : Nat) : True := by Extracting at a hypothesis, not all top level. -/ /-- -info: x✝ : Nat := 1 +trace: x✝ : Nat := 1 y✝ : Nat := 2 h : x✝ + 1 = y✝ ⊢ True @@ -363,7 +363,7 @@ example (h : let x := 1; x + 1 = let y := 2; y) : True := by Extracting at a hypothesis, not all top level, in `-descend` mode. -/ /-- -info: x✝ : Nat := 1 +trace: x✝ : Nat := 1 h : x✝ + 1 = let y := 2; @@ -380,7 +380,7 @@ example (h : let x := 1; x + 1 = let y := 2; y) : True := by At multiple locations with `merge := true`. -/ /-- -info: _z✝ : Nat := 3 +trace: _z✝ : Nat := 3 x✝ : Nat := 1 h : x✝ + 2 = _z✝ ⊢ ∀ (x : Nat), True @@ -396,7 +396,7 @@ example (h : let x := 1; let y := 3; x + 2 = y) : let _z := 3; ∀ (_ : Nat), Tr At multiple locations with `merge := false`. -/ /-- -info: _z✝ : Nat := 3 +trace: _z✝ : Nat := 3 x✝ : Nat := 1 y✝ : Nat := 3 h : x✝ + 2 = y✝ @@ -413,7 +413,7 @@ example (h : let x := 1; let y := 3; x + 2 = y) : let _z := 3; ∀ (_ : Nat), Tr Merging can chain. This tests how extracted let declarations are recalled and can handle dependence. -/ /-- -info: x✝ : Nat := 2 +trace: x✝ : Nat := 2 y✝ : Nat := x✝ ⊢ y✝ = y✝ -/ @@ -427,7 +427,7 @@ example : (let x := 2; let y := x; y) = (let x' := 2; let y' := x'; y') := by Same merging example, but with `-merge`. -/ /-- -info: x✝ : Nat := 2 +trace: x✝ : Nat := 2 y✝ : Nat := x✝ x'✝ : Nat := 2 y'✝ : Nat := x'✝ @@ -445,21 +445,21 @@ Reported at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topi Unused lets are handled properly. -/ /-- -info: ok✝ : Prop := True +trace: ok✝ : Prop := True h : let _not_ok := False; ok✝ ⊢ let _also_ok := 3; True --- -info: ok✝ : Prop := True +trace: ok✝ : Prop := True h : let _not_ok := False; ok✝ _also_ok✝ : Nat := 3 ⊢ True --- -info: ok✝ : Prop := True +trace: ok✝ : Prop := True _also_ok✝ : Nat := 3 _not_ok✝ : Prop := False h : ok✝ @@ -479,12 +479,12 @@ example (h : let ok := True; let _not_ok := False; ok) : let _also_ok := 3; True Testing `+usedOnly` -/ /-- -info: ok✝ : Prop := True +trace: ok✝ : Prop := True h : ok✝ ⊢ let _also_ok := 3; True --- -info: ok✝ : Prop := True +trace: ok✝ : Prop := True h : ok✝ ⊢ True -/ @@ -500,12 +500,12 @@ example (h : let ok := True; let _not_ok := False; ok) : let _also_ok := 3; True Testing `+usedOnly` with `-descend` -/ /-- -info: ok✝ : Prop := True +trace: ok✝ : Prop := True h : ok✝ ⊢ let _also_ok := 3; True --- -info: ok✝ : Prop := True +trace: ok✝ : Prop := True h : ok✝ ⊢ True -/ @@ -521,7 +521,7 @@ example (h : let ok := True; let _not_ok := False; ok) : let _also_ok := 3; True `+proofs` -/ /-- -info: this✝ : (some true).isSome = true := of_eq_true (eq_self true) +trace: this✝ : (some true).isSome = true := of_eq_true (eq_self true) ⊢ (some true).get this✝ = true -/ #guard_msgs in @@ -535,7 +535,7 @@ example : Option.get (some true) (have := (by simp); this) = true := by `+implicits` -/ /-- -info: α✝ : Type := Nat +trace: α✝ : Type := Nat ⊢ id 2 = 2 -/ #guard_msgs in @@ -570,7 +570,7 @@ example : ∀ n : Nat, let x := n; x = x := by Can extract from underneath another `let`. -/ /-- -info: y✝ : Nat := 2 +trace: y✝ : Nat := 2 ⊢ ∀ (n : Nat), let x := n; x + y✝ = x + y✝ @@ -638,7 +638,7 @@ See also the `lift_lets.lean` test file. Lifts, does not make use of name generator. -/ /-- -info: ⊢ ∀ (n : Nat), +trace: ⊢ ∀ (n : Nat), let x := n; n = x -/ @@ -654,7 +654,7 @@ example : ∀ n : Nat, n = (let x := n; x) := by Same example, but testing `letFun`. -/ /-- -info: ⊢ ∀ (n : Nat), +trace: ⊢ ∀ (n : Nat), let_fun x := n; n = x -/ @@ -671,7 +671,7 @@ Merging of merely-lifted lets. Four cases to this test, depending on whether a ` and whether the second is a `have` or `let`. -/ /-- -info: ⊢ ∀ (n : Nat), +trace: ⊢ ∀ (n : Nat), let_fun x := n; x = x -/ @@ -683,7 +683,7 @@ example : ∀ n : Nat, (have x := n; x) = (have x' := n; x') := by intros rfl /-- -info: ⊢ ∀ (n : Nat), +trace: ⊢ ∀ (n : Nat), let x := n; x = x -/ @@ -695,7 +695,7 @@ example : ∀ n : Nat, (let x := n; x) = (have x' := n; x') := by intros rfl /-- -info: ⊢ ∀ (n : Nat), +trace: ⊢ ∀ (n : Nat), let x := n; x = x -/ @@ -707,7 +707,7 @@ example : ∀ n : Nat, (have x := n; x) = (let x' := n; x') := by intros rfl /-- -info: ⊢ ∀ (n : Nat), +trace: ⊢ ∀ (n : Nat), let x := n; x = x -/ @@ -723,7 +723,7 @@ example : ∀ n : Nat, (let x := n; x) = (let x' := n; x') := by Without merging -/ /-- -info: ⊢ ∀ (n : Nat), +trace: ⊢ ∀ (n : Nat), let_fun x := n; let_fun x' := n; x = x' @@ -748,7 +748,7 @@ example : ∀ n : Nat, let x := n; let y := x; y = n := by Extracting `let`s in proofs in `+proof` mode. -/ /-- -info: m : Nat +trace: m : Nat h : ∃ n, n + 1 = m x : Fin m y : Fin (h.choose + 1) @@ -771,10 +771,10 @@ example (m : Nat) (h : ∃ n, n + 1 = m) (x : Fin m) (y : Fin _) : Limitation: we can use `extract_lets` within `conv`, but the let bindings do not persist. -/ /-- -info: y : Type := Nat +trace: y : Type := Nat | y = Int --- -info: ⊢ Nat = Int +trace: ⊢ Nat = Int -/ #guard_msgs in example : let x := Nat; x = Int := by diff --git a/tests/lean/run/fixedParams.lean b/tests/lean/run/fixedParams.lean index 04317f95a2..d857e616ae 100644 --- a/tests/lean/run/fixedParams.lean +++ b/tests/lean/run/fixedParams.lean @@ -7,7 +7,7 @@ namespace Ex1 /-- error: well-founded recursion cannot be used, 'Ex1.foo' does not take any (non-fixed) arguments --- -info: [Elab.definition.fixedParams] getFixedParams: +trace: [Elab.definition.fixedParams] getFixedParams: • ⏎ • -/ @@ -25,7 +25,7 @@ namespace Ex2 /-- error: well-founded recursion cannot be used, 'Ex2.foo' does not take any (non-fixed) arguments --- -info: [Elab.definition.fixedParams] getFixedParams: +trace: [Elab.definition.fixedParams] getFixedParams: • [#1 #1] • [#1 #1] -/ @@ -41,7 +41,7 @@ namespace Ex3 /-- error: well-founded recursion cannot be used, 'Ex3.foo' does not take any (non-fixed) arguments --- -info: [Elab.definition.fixedParams] getFixedParams: +trace: [Elab.definition.fixedParams] getFixedParams: • [#1 #2] [#2 #1] • [#2 #1] [#1 #2] -/ @@ -56,7 +56,7 @@ end Ex3 namespace Ex4 /-- -info: [Elab.definition.fixedParams] getFixedParams: notFixed 0 3: +trace: [Elab.definition.fixedParams] getFixedParams: notFixed 0 3: In foo c n b m m not matched [Elab.definition.fixedParams] getFixedParams: • [#1 #3] ❌ [#3 #1] ❌ • [#3 #1] ❌ [#1 #3] ❌ @@ -73,7 +73,7 @@ end Ex4 namespace Append1 /-- -info: [Elab.definition.fixedParams] getFixedParams: notFixed 0 1: +trace: [Elab.definition.fixedParams] getFixedParams: notFixed 0 1: In app as bs x✝¹ =/= as [Elab.definition.fixedParams] getFixedParams: notFixed 0 2: @@ -81,18 +81,18 @@ info: [Elab.definition.fixedParams] getFixedParams: notFixed 0 1: x✝ =/= bs [Elab.definition.fixedParams] getFixedParams: • [#1] ❌ ❌ -/ -#guard_msgs(info) in +#guard_msgs(trace) in def app : List α → List α → List α | [], bs => bs | a::as, bs => a :: app as bs /-- -info: [Elab.definition.fixedParams] getFixedParams: notFixed 0 1: +trace: [Elab.definition.fixedParams] getFixedParams: notFixed 0 1: In app' as bs as✝ =/= as [Elab.definition.fixedParams] getFixedParams: • [#1] ❌ [#3] -/ -#guard_msgs(info) in +#guard_msgs(trace) in def app' (as : List α) (bs : List α) : List α := match as with | [] => bs diff --git a/tests/lean/run/frontend_meeting_2022_09_13.lean b/tests/lean/run/frontend_meeting_2022_09_13.lean index 784ab6ae03..02e540edc3 100644 --- a/tests/lean/run/frontend_meeting_2022_09_13.lean +++ b/tests/lean/run/frontend_meeting_2022_09_13.lean @@ -86,11 +86,11 @@ elab "seq" s:tacticSeq : tactic => do evalTactic tac /-- -info: x y : Nat +trace: x y : Nat h : x = y ⊢ 0 + x = y --- -info: x y : Nat +trace: x y : Nat h : x = y ⊢ 0 + y = y -/ @@ -100,11 +100,11 @@ example (h : x = y) : 0 + x = y := by done /-- -info: x y : Nat +trace: x y : Nat h : x = y ⊢ 0 + x = y --- -info: x y : Nat +trace: x y : Nat h : x = y ⊢ 0 + y = y -/ @@ -115,11 +115,11 @@ example (h : x = y) : 0 + x = y := by done /-- -info: x y : Nat +trace: x y : Nat h : x = y ⊢ 0 + x = y --- -info: x y : Nat +trace: x y : Nat h : x = y ⊢ 0 + y = y -/ diff --git a/tests/lean/run/generalizeMany.lean b/tests/lean/run/generalizeMany.lean index d830507429..a704ca4a0d 100644 --- a/tests/lean/run/generalizeMany.lean +++ b/tests/lean/run/generalizeMany.lean @@ -1,7 +1,7 @@ set_option pp.analyze false /-- -info: p : (n : Nat) → Fin n → Prop +trace: p : (n : Nat) → Fin n → Prop n : Nat v : Fin n n' : Nat diff --git a/tests/lean/run/generalizeTelescope.lean b/tests/lean/run/generalizeTelescope.lean index 22ca23bba8..f8aa7fc1d7 100644 --- a/tests/lean/run/generalizeTelescope.lean +++ b/tests/lean/run/generalizeTelescope.lean @@ -22,7 +22,7 @@ let t ← mkLambdaFVars ys ys.back! trace[Meta.debug] t pure () -/-- info: [Meta.debug] fun x x => x -/ +/-- trace: [Meta.debug] fun x x => x -/ #guard_msgs in #eval tst1 @@ -39,7 +39,7 @@ let t ← mkLambdaFVars ys ys.back! trace[Meta.debug] t pure () -/-- info: [Meta.debug] fun (x : Nat) (x_1 : Vec Nat x) (x : @Eq.{1} (Vec Nat x) x_1 x_1) => x -/ +/-- trace: [Meta.debug] fun (x : Nat) (x_1 : Vec Nat x) (x : @Eq.{1} (Vec Nat x) x_1 x_1) => x -/ #guard_msgs in #eval tst2 @@ -61,6 +61,6 @@ failIfSuccess do pure () trace[Meta.debug] "failed as expected" -/-- info: [Meta.debug] failed as expected -/ +/-- trace: [Meta.debug] failed as expected -/ #guard_msgs in #eval tst3 diff --git a/tests/lean/run/genindices.lean b/tests/lean/run/genindices.lean index cbde572865..99f11bc74e 100644 --- a/tests/lean/run/genindices.lean +++ b/tests/lean/run/genindices.lean @@ -25,7 +25,7 @@ pure () set_option trace.Elab true /-- -info: [Elab] ⊢ ∀ (α : Type u) (xs : List (List α)) (h : Pred (List α) xs), xs ≠ [] → xs = xs +trace: [Elab] ⊢ ∀ (α : Type u) (xs : List (List α)) (h : Pred (List α) xs), xs ≠ [] → xs = xs [Elab] α✝ : Type u xs✝ : List (List α✝) h✝ : Pred (List α✝) xs✝ diff --git a/tests/lean/run/grind_attrs.lean b/tests/lean/run/grind_attrs.lean index 5eb965cc8b..7c97e139fd 100644 --- a/tests/lean/run/grind_attrs.lean +++ b/tests/lean/run/grind_attrs.lean @@ -27,20 +27,20 @@ opaque Expr.eval : Expr → State → Nat axiom Expr.constProp : Expr → State → Expr -/-- info: [grind.ematch.pattern] eval_constProp_of_sub: [State.le #3 #2, constProp #1 #3] -/ -#guard_msgs (info) in +/-- trace: [grind.ematch.pattern] eval_constProp_of_sub: [State.le #3 #2, constProp #1 #3] -/ +#guard_msgs (trace) in set_option trace.grind.ematch.pattern true in @[grind =>] theorem Expr.eval_constProp_of_sub (e : Expr) (h : State.le σ' σ) : (e.constProp σ').eval σ = e.eval σ := sorry -/-- info: [grind.ematch.pattern] eval_constProp_of_eq_of_sub: [State.le #3 #2, constProp #1 #3] -/ -#guard_msgs (info) in +/-- trace: [grind.ematch.pattern] eval_constProp_of_eq_of_sub: [State.le #3 #2, constProp #1 #3] -/ +#guard_msgs (trace) in set_option trace.grind.ematch.pattern true in @[grind =>] theorem Expr.eval_constProp_of_eq_of_sub {e : Expr} (h₂ : State.le σ' σ) : (e.constProp σ').eval σ = e.eval σ := sorry -/-- info: [grind.ematch.pattern] update_le_update: [le #4 #3, update #4 #2 #1] -/ -#guard_msgs (info) in +/-- trace: [grind.ematch.pattern] update_le_update: [le #4 #3, update #4 #2 #1] -/ +#guard_msgs (trace) in set_option trace.grind.ematch.pattern true in @[grind =>] theorem State.update_le_update (h : State.le σ' σ) : State.le (σ'.update x v) (σ.update x v) := sorry diff --git a/tests/lean/run/grind_beta.lean b/tests/lean/run/grind_beta.lean index 6e24e05d22..248a9e3d4a 100644 --- a/tests/lean/run/grind_beta.lean +++ b/tests/lean/run/grind_beta.lean @@ -30,10 +30,10 @@ example (f : Nat → Nat → Nat) : f 2 3 ≠ 5 → f = (fun x y : Nat => x + y) opaque bla : Nat → Nat → Nat → Nat /-- -info: [grind.beta] f 2 3 = bla 2 3 2, using fun x y => bla x y x +trace: [grind.beta] f 2 3 = bla 2 3 2, using fun x y => bla x y x [grind.beta] f 2 3 = 2 + 3, using fun x y => x + y -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.beta true in example (g h f : Nat → Nat → Nat) : f 2 3 ≠ 5 → diff --git a/tests/lean/run/grind_canon_insts.lean b/tests/lean/run/grind_canon_insts.lean index 432122d4ff..602c1e791e 100644 --- a/tests/lean/run/grind_canon_insts.lean +++ b/tests/lean/run/grind_canon_insts.lean @@ -52,8 +52,8 @@ def fallback : Fallback := do set_option trace.Meta.debug true -/-- info: [Meta.debug] [a * (b * c), b * c, d * (b * c)] -/ -#guard_msgs (info) in +/-- trace: [Meta.debug] [a * (b * c), b * c, d * (b * c)] -/ +#guard_msgs (trace) in example (a b c d : Nat) : b * (a * c) = d * (b * c) → False := by rw [left_comm] -- Introduces a new (non-canonical) instance for `Mul Nat` grind on_failure fallback -- State should have only 3 `*`-applications @@ -62,14 +62,14 @@ example (a b c d : Nat) : b * (a * c) = d * (b * c) → False := by set_option pp.notation false in set_option pp.explicit true in /-- -info: [Meta.debug] [@HMul.hMul Int Int Int (@instHMul Int Int.instMul) (@NatCast.natCast Int instNatCastInt b) +trace: [Meta.debug] [@HMul.hMul Int Int Int (@instHMul Int Int.instMul) (@NatCast.natCast Int instNatCastInt b) (@NatCast.natCast Int instNatCastInt a), @HMul.hMul Int Int Int (@instHMul Int Int.instMul) (@NatCast.natCast Int instNatCastInt b) (@NatCast.natCast Int instNatCastInt d), @HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) b a, @HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) b d] -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (a b c d : Nat) : b * a = d * b → False := by rw [CommMonoid.mul_comm d b] -- Introduces a new (non-canonical) instance for `Mul Nat` -- See target here diff --git a/tests/lean/run/grind_canon_types.lean b/tests/lean/run/grind_canon_types.lean index 05fa1ee350..cf47bd5746 100644 --- a/tests/lean/run/grind_canon_types.lean +++ b/tests/lean/run/grind_canon_types.lean @@ -12,9 +12,9 @@ def fallback : Fallback := do set_option trace.Meta.debug true set_option pp.explicit true /-- -info: [Meta.debug] [@f Nat a, @f Nat b] +trace: [Meta.debug] [@f Nat a, @f Nat b] -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (a b c d : Nat) : @f Nat a = b → @f (g Nat) a = c → @f (g Nat) b = d → a = b → False := by -- State should have only two `f`-applications: `@f Nat a`, `@f Nat b` -- Note that `@f (g Nat) b` has been canonicalized to `@f Nat b`. diff --git a/tests/lean/run/grind_cases_tac.lean b/tests/lean/run/grind_cases_tac.lean index c63200ab14..26c075fdf0 100644 --- a/tests/lean/run/grind_cases_tac.lean +++ b/tests/lean/run/grind_cases_tac.lean @@ -15,28 +15,28 @@ def f (v : Vec α n) : Bool := | .cons .. => false /-- -info: n : Nat +trace: n : Nat v : Vec Nat n h : f v ≠ false ⊢ n + 1 = 0 → HEq (Vec.cons 10 v) Vec.nil → False --- -info: n : Nat +trace: n : Nat v : Vec Nat n h : f v ≠ false ⊢ ∀ {n_1 : Nat} (a : Nat) (a_1 : Vec Nat n_1), n + 1 = n_1 + 1 → HEq (Vec.cons 10 v) (Vec.cons a a_1) → False -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (v : Vec Nat n) (h : f v ≠ false) : False := by cases' (Vec.cons 10 v) next => trace_state; sorry next => trace_state; sorry /-- -info: ⊢ False → False +trace: ⊢ False → False --- -info: ⊢ True → False +trace: ⊢ True → False -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : False := by cases' (Or.inr (a := False) True.intro) next => trace_state; sorry diff --git a/tests/lean/run/grind_cat.lean b/tests/lean/run/grind_cat.lean index 446941614d..4ca15fa495 100644 --- a/tests/lean/run/grind_cat.lean +++ b/tests/lean/run/grind_cat.lean @@ -1,3 +1,5 @@ +set_option grind.warning false + universe v v₁ v₂ v₃ u u₁ u₂ u₃ namespace CategoryTheory diff --git a/tests/lean/run/grind_congr.lean b/tests/lean/run/grind_congr.lean index 8c13ab8b7d..d6684ecd42 100644 --- a/tests/lean/run/grind_congr.lean +++ b/tests/lean/run/grind_congr.lean @@ -16,29 +16,29 @@ set_option grind.debug true set_option grind.debug.proofs true /-- -info: [Meta.debug] [d, f b, c, f a] +trace: [Meta.debug] [d, f b, c, f a] -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (a b c d : Nat) : a = b → f a = c → f b = d → False := by grind on_failure fallback /-- -info: [Meta.debug] [d, f b, c, f a] +trace: [Meta.debug] [d, f b, c, f a] -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (a b c d : Nat) : f a = c → f b = d → a = b → False := by grind on_failure fallback /-- -info: [Meta.debug] [d, f (g b), c, f (g a)] +trace: [Meta.debug] [d, f (g b), c, f (g a)] -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (a b c d e : Nat) : f (g a) = c → f (g b) = d → a = e → b = e → False := by grind on_failure fallback /-- -info: [Meta.debug] [d, f (g b), c, f v] +trace: [Meta.debug] [d, f (g b), c, f v] -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (a b c d e v : Nat) : f v = c → f (g b) = d → a = e → b = e → v = g a → False := by grind on_failure fallback diff --git a/tests/lean/run/grind_cutsat_auto.lean b/tests/lean/run/grind_cutsat_auto.lean index e86ff399ac..e445e794f0 100644 --- a/tests/lean/run/grind_cutsat_auto.lean +++ b/tests/lean/run/grind_cutsat_auto.lean @@ -30,13 +30,13 @@ abbrev problem (x y z w v : Int) : Prop := (y ≥ -10) /-- -info: [grind.cutsat.model] x := 121 +trace: [grind.cutsat.model] x := 121 [grind.cutsat.model] y := -10 [grind.cutsat.model] z := -34 [grind.cutsat.model] w := 0 [grind.cutsat.model] v := 1 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.cutsat.model true in example (x y z w v : Int) : problem x y z w v → False := by fail_if_success grind diff --git a/tests/lean/run/grind_cutsat_cooper.lean b/tests/lean/run/grind_cutsat_cooper.lean index 3405f163a3..38dcd6dc4d 100644 --- a/tests/lean/run/grind_cutsat_cooper.lean +++ b/tests/lean/run/grind_cutsat_cooper.lean @@ -19,17 +19,17 @@ abbrev problem₁ [∀ n, OfNat α n] [Neg α] [Mul α] [Sub α] [Add α] [LE α 7*x - 9*y ≤ 4 /-- -info: [grind.cutsat.model] x := 241/154 +trace: [grind.cutsat.model] x := 241/154 [grind.cutsat.model] y := 1 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.cutsat.model true in example (x y : Int) : problem₁ x y → False := by fail_if_success grind +qlia -- Rational counterexamples allowed sorry /-- info: true -/ -#guard_msgs (info) in +#guard_msgs in open Std.Internal in #eval problem₁ (241/154 : Rat) (1 : Rat) diff --git a/tests/lean/run/grind_cutsat_diseq_1.lean b/tests/lean/run/grind_cutsat_diseq_1.lean index 0539ed88b2..56da6c5620 100644 --- a/tests/lean/run/grind_cutsat_diseq_1.lean +++ b/tests/lean/run/grind_cutsat_diseq_1.lean @@ -5,80 +5,80 @@ open Int.Linear set_option trace.grind.cutsat.assert true /-- -info: [grind.cutsat.assert] a + b + 1 ≤ 0 +trace: [grind.cutsat.assert] a + b + 1 ≤ 0 [grind.cutsat.assert] a + -1*b ≠ 0 -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (a b : Int) : a + b < 0 → a ≠ b → False := by (fail_if_success grind); sorry -#guard_msgs (info) in -- `a` and `b` are not relevant to cutsat in the following example +#guard_msgs (trace) in -- `a` and `b` are not relevant to cutsat in the following example example (a b : Int) : a ≠ b → False := by (fail_if_success grind); sorry /-- -info: [grind.cutsat.assert] a + -1*b ≠ 0 +trace: [grind.cutsat.assert] a + -1*b ≠ 0 [grind.cutsat.assert] a + b + 1 ≤ 0 -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (a b : Int) : a ≠ b → a + b < 0 → False := by (fail_if_success grind); sorry /-- -info: [grind.cutsat.assert] a + -1*b ≠ 0 +trace: [grind.cutsat.assert] a + -1*b ≠ 0 [grind.cutsat.assert] a + b + 1 ≤ 0 -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (a b c : Int) : a ≠ c → c = b → a + b < 0 → False := by (fail_if_success grind); sorry /-- -info: [grind.cutsat.assert] a + -1*b ≠ 0 +trace: [grind.cutsat.assert] a + -1*b ≠ 0 [grind.cutsat.assert] a + b + 1 ≤ 0 -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (a b c d : Int) : d ≠ c → c = b → a = d → a + b < 0 → False := by (fail_if_success grind); sorry /-- -info: [grind.cutsat.assert] a + b + 1 ≤ 0 +trace: [grind.cutsat.assert] a + b + 1 ≤ 0 [grind.cutsat.assert] a + -1*b ≠ 0 -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (a b c d : Int) : d ≠ c → a = d → a + b < 0 → c = b → False := by (fail_if_success grind); sorry /-- -info: [grind.cutsat.assert] a + b + 1 ≤ 0 +trace: [grind.cutsat.assert] a + b + 1 ≤ 0 [grind.cutsat.assert] a + -1*b ≠ 0 [grind.cutsat.assert] e + -1*b = 0 [grind.cutsat.assert] -1*e + 1 ≤ 0 -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (a b c d e : Int) : d ≠ c → a = d → a + b < 0 → c = b → c = e → e > 0 → False := by (fail_if_success grind); sorry /-- -info: [grind.cutsat.assert] -1*e + 1 ≤ 0 +trace: [grind.cutsat.assert] -1*e + 1 ≤ 0 [grind.cutsat.assert] b + -1*e = 0 [grind.cutsat.assert] a + -1*e ≠ 0 [grind.cutsat.assert] a + b + 1 ≤ 0 -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (a b c d e : Int) : d ≠ c → a = d → c = b → c = e → e > 0 → a + b < 0 → False := by (fail_if_success grind); sorry /-- -info: [grind.cutsat.assert] -1*e + 1 ≤ 0 +trace: [grind.cutsat.assert] -1*e + 1 ≤ 0 [grind.cutsat.assert] b + -1*e = 0 [grind.cutsat.assert] a + b + 1 ≤ 0 [grind.cutsat.assert] a + -1*e ≠ 0 -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (a b c d e : Int) : a = d → c = b → c = e → e > 0 → a + b < 0 → d ≠ c → False := by (fail_if_success grind); sorry -#guard_msgs (info) in -- no propagation to cutsat +#guard_msgs (trace) in -- no propagation to cutsat example (a b c d e : Int) : a = d → c = b → c = e → a = 1 → d ≠ c → False := by (fail_if_success grind); sorry diff --git a/tests/lean/run/grind_cutsat_diseq_2.lean b/tests/lean/run/grind_cutsat_diseq_2.lean index e5a24cc04a..747c8bb184 100644 --- a/tests/lean/run/grind_cutsat_diseq_2.lean +++ b/tests/lean/run/grind_cutsat_diseq_2.lean @@ -12,14 +12,14 @@ theorem ex₃ (a b c : Int) : a + b + c = 0 → a = c → b = 4 → c = -2 := by grind /-- -info: [grind.cutsat.assert] -1*「a + -2 * b + -2 * c」 + a + -2*b + -2*c = 0 +trace: [grind.cutsat.assert] -1*「a + -2 * b + -2 * c」 + a + -2*b + -2*c = 0 [grind.cutsat.assert] 「a + -2 * b + -2 * c」 = 0 [grind.cutsat.assert] -1*「a + -2 * b + -2 * d」 + a + -2*b + -2*d = 0 [grind.cutsat.assert] 「a + -2 * b + -2 * d」 ≠ 0 [grind.cutsat.assert] -1*d + c = 0 [grind.cutsat.assert] 0 ≠ 0 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.cutsat.assert true in theorem ex₄ (a b c d : Int) : a = 2*b + 2*c → a - 2*b - 2*d ≠ 0 → c ≠ d := by grind diff --git a/tests/lean/run/grind_cutsat_div_1.lean b/tests/lean/run/grind_cutsat_div_1.lean index b8eb2a7f26..00eafeae4b 100644 --- a/tests/lean/run/grind_cutsat_div_1.lean +++ b/tests/lean/run/grind_cutsat_div_1.lean @@ -21,22 +21,22 @@ theorem ex₄ (f : Int → Int) (a b : Int) (_ : 2 ∣ f (f a) + 1) (h₁ : 3 #print ex₄ /-- -info: [grind.debug.cutsat.search.assign] a := 1 +trace: [grind.debug.cutsat.search.assign] a := 1 [grind.debug.cutsat.search.assign] b := 0 -/ -#guard_msgs (info) in -- finds the model without any backtracking +#guard_msgs (trace) in -- finds the model without any backtracking set_option trace.grind.debug.cutsat.search.assign true in example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + b - 4) : False := by fail_if_success grind sorry /-- -info: [grind.cutsat.assert] 2 ∣ a + 3 +trace: [grind.cutsat.assert] 2 ∣ a + 3 [grind.cutsat.assert] 3 ∣ a + 3*b + -4 [grind.debug.cutsat.search.assign] a := 1 [grind.debug.cutsat.search.assign] b := 0 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.cutsat.assert true in set_option trace.grind.debug.cutsat.search.assign true in example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + 3*b - 4) : False := by @@ -44,30 +44,30 @@ example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + 3*b - 4) : False := by sorry /-- -info: [grind.debug.cutsat.search.assign] a := 1 +trace: [grind.debug.cutsat.search.assign] a := 1 [grind.debug.cutsat.search.assign] b := 15 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.debug.cutsat.search.assign true in example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + b - 4) (_ : b < 18): False := by fail_if_success grind sorry /-- -info: [grind.debug.cutsat.search.assign] a := 1 +trace: [grind.debug.cutsat.search.assign] a := 1 [grind.debug.cutsat.search.assign] b := 12 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.debug.cutsat.search.assign true in example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + b - 4) (_ : b ≥ 11): False := by fail_if_success grind sorry /-- -info: [grind.debug.cutsat.search.assign] f 0 := 11 +trace: [grind.debug.cutsat.search.assign] f 0 := 11 [grind.debug.cutsat.search.assign] f 1 := 2 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.debug.cutsat.search.assign true in example (f : Int → Int) (_ : 2 ∣ f 0 + 3) (_ : 3 ∣ f 0 + f 1 - 4) (_ : f 0 ≥ 11): False := by fail_if_success grind diff --git a/tests/lean/run/grind_cutsat_div_mod.lean b/tests/lean/run/grind_cutsat_div_mod.lean index 393773e841..e2477a8b61 100644 --- a/tests/lean/run/grind_cutsat_div_mod.lean +++ b/tests/lean/run/grind_cutsat_div_mod.lean @@ -13,10 +13,10 @@ example (x y : Int) : x % 2 + y = 3 → x = 5 → y = 2 := by grind /-- -info: [grind.cutsat.model] x := 5 +trace: [grind.cutsat.model] x := 5 [grind.cutsat.model] y := 2 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.cutsat.model true in example (x y : Int) : x % 2 + y = 3 → x ≤ 5 → x > 4 → y = 1 := by fail_if_success grind diff --git a/tests/lean/run/grind_cutsat_eq_1.lean b/tests/lean/run/grind_cutsat_eq_1.lean index 5dd337768b..ff71a9630c 100644 --- a/tests/lean/run/grind_cutsat_eq_1.lean +++ b/tests/lean/run/grind_cutsat_eq_1.lean @@ -3,10 +3,10 @@ set_option grind.debug true open Int.Linear /-- -info: [grind.cutsat.assert] -1*「b + f a + 1」 + b + f a + 1 = 0 +trace: [grind.cutsat.assert] -1*「b + f a + 1」 + b + f a + 1 = 0 [grind.cutsat.assert] 「b + f a + 1」 = 0 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.cutsat.assert true in example (a b : Int) (f : Int → Int) (h₁ : f a + b + 3 = 2) : False := by fail_if_success grind diff --git a/tests/lean/run/grind_cutsat_le_1.lean b/tests/lean/run/grind_cutsat_le_1.lean index e6993c84a8..63f9c790fb 100644 --- a/tests/lean/run/grind_cutsat_le_1.lean +++ b/tests/lean/run/grind_cutsat_le_1.lean @@ -2,10 +2,10 @@ set_option grind.warning false set_option grind.debug true /-- -info: [grind.debug.cutsat.search.assign] b := -1 +trace: [grind.debug.cutsat.search.assign] b := -1 [grind.debug.cutsat.search.assign] a := 3 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.debug.cutsat.search.assign true in example (a b : Int) (h₁ : a ≤ 3) (h₂ : a > 2) (h₃ : a + b < 3) : False := by fail_if_success grind diff --git a/tests/lean/run/grind_cutsat_le_2.lean b/tests/lean/run/grind_cutsat_le_2.lean index 87b0e0e26d..7da35a0789 100644 --- a/tests/lean/run/grind_cutsat_le_2.lean +++ b/tests/lean/run/grind_cutsat_le_2.lean @@ -11,12 +11,12 @@ example (a b c d e : Int) : set_option trace.grind.cutsat.model true /-- -info: [grind.cutsat.model] a := 7 +trace: [grind.cutsat.model] a := 7 [grind.cutsat.model] b := 0 [grind.cutsat.model] c := 3 [grind.cutsat.model] d := 2 -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (a b c d e : Int) : a + b ≥ 0 → a = 2*c + 1 → @@ -25,11 +25,11 @@ example (a b c d e : Int) : (fail_if_success grind); sorry /-- -info: [grind.cutsat.model] a := 17 +trace: [grind.cutsat.model] a := 17 [grind.cutsat.model] b := -9 [grind.cutsat.model] c := -9 -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (a b c : Int) : 2*a + 3*b = 7 → 4*a + 7*c = 5 → diff --git a/tests/lean/run/grind_cutsat_nat_eq.lean b/tests/lean/run/grind_cutsat_nat_eq.lean index d5c4f8dc51..89beaf0d60 100644 --- a/tests/lean/run/grind_cutsat_nat_eq.lean +++ b/tests/lean/run/grind_cutsat_nat_eq.lean @@ -70,21 +70,21 @@ example (a b : Int) : (a - b).toNat = 0 ↔ a ≤ b := by grind /-- -info: [grind.cutsat.model] x := 3 +trace: [grind.cutsat.model] x := 3 [grind.cutsat.model] y := 1 [grind.cutsat.model] z := 4 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.cutsat.model true in example (x y z : Nat) : x ≥ 3 → x ≠ z → x > y → z ≤ 6 → x + y = z → False := by fail_if_success grind sorry /-- -info: [grind.cutsat.model] x := 13 +trace: [grind.cutsat.model] x := 13 [grind.cutsat.model] y := 9 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.cutsat.model true in example (x y : Nat) : x > 8 → y > 8 → x ≠ y → (x - y) % 4 = 1 := by fail_if_success grind @@ -115,10 +115,10 @@ example (x y : Nat) : x ^ 0 + y = 0 → False := by grind /-- -info: [grind.cutsat.model] x := 4 +trace: [grind.cutsat.model] x := 4 [grind.cutsat.model] y := 1 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.cutsat.model true in example (x y : Nat) : x = y + 3 → y > 0 → False := by fail_if_success grind diff --git a/tests/lean/run/grind_cutsat_nat_le.lean b/tests/lean/run/grind_cutsat_nat_le.lean index 5c9f8d717b..56a28c4b74 100644 --- a/tests/lean/run/grind_cutsat_nat_le.lean +++ b/tests/lean/run/grind_cutsat_nat_le.lean @@ -29,7 +29,7 @@ example (a b : Int) : a + b = Int.ofNat 2 → a - 2 = -b := by grind /-- -info: [grind.cutsat.assert] -1*「↑a * ↑b」 ≤ 0 +trace: [grind.cutsat.assert] -1*「↑a * ↑b」 ≤ 0 [grind.cutsat.assert] -1*↑c ≤ 0 [grind.cutsat.assert] -1*↑c + 「↑a * ↑b」 + 1 ≤ 0 [grind.cutsat.assert] ↑c = 0 @@ -37,7 +37,7 @@ info: [grind.cutsat.assert] -1*「↑a * ↑b」 ≤ 0 [grind.cutsat.assert] 「↑a * ↑b」 + 1 ≤ 0 [grind.cutsat.assert] 1 ≤ 0 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.cutsat.assert true in example (a b c : Nat) : c > a * b → c >= 1 := by grind diff --git a/tests/lean/run/grind_cutsat_tests.lean b/tests/lean/run/grind_cutsat_tests.lean index 73af9b014b..058154e5a0 100644 --- a/tests/lean/run/grind_cutsat_tests.lean +++ b/tests/lean/run/grind_cutsat_tests.lean @@ -15,13 +15,13 @@ abbrev test1 (a b c d e : Int) := a ≤ 100 /-- -info: [grind.cutsat.model] a := 101 +trace: [grind.cutsat.model] a := 101 [grind.cutsat.model] b := 0 [grind.cutsat.model] c := 5335 [grind.cutsat.model] d := 0 [grind.cutsat.model] e := 0 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.cutsat.model true in example (a b c d e : Int) : test1 a b c d e := by (fail_if_success grind); sorry diff --git a/tests/lean/run/grind_cutsat_upper_bug.lean b/tests/lean/run/grind_cutsat_upper_bug.lean index 7816edb355..98c9c46c5a 100644 --- a/tests/lean/run/grind_cutsat_upper_bug.lean +++ b/tests/lean/run/grind_cutsat_upper_bug.lean @@ -1,5 +1,5 @@ -/-- info: [grind.cutsat.model] a := 2 -/ -#guard_msgs (info) in +/-- trace: [grind.cutsat.model] a := 2 -/ +#guard_msgs (trace) in set_option trace.grind.cutsat.model true in example (a b : Int) : a ≤ 5 → a ≠ 4 → 2 ∣ a → False := by (fail_if_success grind); sorry diff --git a/tests/lean/run/grind_diseq_api.lean b/tests/lean/run/grind_diseq_api.lean index 7429dae319..a7bc7a52f7 100644 --- a/tests/lean/run/grind_diseq_api.lean +++ b/tests/lean/run/grind_diseq_api.lean @@ -23,58 +23,58 @@ def fallback : Fallback := do set_option trace.Meta.debug true /-- -info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h_2 (Lean.Grind.ne_of_ne_of_eq_left h (Ne.symm h_1)) : a ≠ b +trace: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h_2 (Lean.Grind.ne_of_ne_of_eq_left h (Ne.symm h_1)) : a ≠ b -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (x y : Nat) : a = x → y ≠ x → b = y → False := by grind on_failure fallback /-- -info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h_2 (Lean.Grind.ne_of_ne_of_eq_left h h_1) : a ≠ b +trace: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h_2 (Lean.Grind.ne_of_ne_of_eq_left h h_1) : a ≠ b -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (x y : Nat) : a = x → x ≠ y → b = y → False := by grind on_failure fallback /-- -info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h_3 (Lean.Grind.ne_of_ne_of_eq_left (Eq.trans h (Eq.symm h_1)) h_2) : a ≠ b +trace: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h_3 (Lean.Grind.ne_of_ne_of_eq_left (Eq.trans h (Eq.symm h_1)) h_2) : a ≠ b -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (x y z : Nat) : a = x → z = x → z ≠ y → b = y → False := by grind on_failure fallback -/-- info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_left h (Ne.symm h_1) : a ≠ b -/ -#guard_msgs (info) in +/-- trace: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_left h (Ne.symm h_1) : a ≠ b -/ +#guard_msgs (trace) in example (x : Nat) : a = x → b ≠ x → False := by grind on_failure fallback -/-- info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_left h h_1 : a ≠ b -/ -#guard_msgs (info) in +/-- trace: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_left h h_1 : a ≠ b -/ +#guard_msgs (trace) in example (x : Nat) : a = x → x ≠ b → False := by grind on_failure fallback -/-- info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h h_1 : a ≠ b -/ -#guard_msgs (info) in +/-- trace: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h h_1 : a ≠ b -/ +#guard_msgs (trace) in example (x : Nat) : b = x → a ≠ x → False := by grind on_failure fallback -/-- info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h (Ne.symm h_1) : a ≠ b -/ -#guard_msgs (info) in +/-- trace: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h (Ne.symm h_1) : a ≠ b -/ +#guard_msgs (trace) in example (x : Nat) : b = x → x ≠ a → False := by grind on_failure fallback -/-- info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_left h (Ne.symm h_1) : a ≠ b -/ -#guard_msgs (info) in +/-- trace: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_left h (Ne.symm h_1) : a ≠ b -/ +#guard_msgs (trace) in example (x : Nat) : a = x → b ≠ x → False := by grind on_failure fallback -/-- info: [Meta.debug] h : ¬a = b -/ -#guard_msgs (info) in +/-- trace: [Meta.debug] h : ¬a = b -/ +#guard_msgs (trace) in example : a ≠ b → False := by grind on_failure fallback -/-- info: [Meta.debug] Ne.symm h : a ≠ b -/ -#guard_msgs (info) in +/-- trace: [Meta.debug] Ne.symm h : a ≠ b -/ +#guard_msgs (trace) in example : b ≠ a → False := by grind on_failure fallback diff --git a/tests/lean/run/grind_ematch1.lean b/tests/lean/run/grind_ematch1.lean index 907015c794..330ae1c13d 100644 --- a/tests/lean/run/grind_ematch1.lean +++ b/tests/lean/run/grind_ematch1.lean @@ -27,10 +27,10 @@ set_option trace.grind.ematch.instance true attribute [grind =] Array.getElem_set_ne /-- -info: [grind.ematch.instance] Array.size_set: (as.set i v ⋯).size = as.size +trace: [grind.ematch.instance] Array.size_set: (as.set i v ⋯).size = as.size [grind.ematch.instance] Array.getElem_set_ne: ∀ (pj : j < as.size), i ≠ j → (as.set i v ⋯)[j] = as[j] -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (as bs cs : Array α) (v : α) (i : Nat) (h₁ : i < as.size) @@ -49,15 +49,15 @@ theorem Rtrans (a b c : Nat) : R a b → R b c → R a c := sorry grind_pattern Rtrans => R a b, R b c /-- -info: [grind.ematch.instance] Rtrans: R a b → R b c → R a c +trace: [grind.ematch.instance] Rtrans: R a b → R b c → R a c -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : R a b → R b c → R a c := by grind /-- -info: [grind.ematch.instance] Rtrans: R a d → R d e → R a e +trace: [grind.ematch.instance] Rtrans: R a d → R d e → R a e [grind.ematch.instance] Rtrans: R c d → R d e → R c e [grind.ematch.instance] Rtrans: R b c → R c d → R b d [grind.ematch.instance] Rtrans: R a b → R b c → R a c @@ -67,7 +67,7 @@ info: [grind.ematch.instance] Rtrans: R a d → R d e → R a e [grind.ematch.instance] Rtrans: R a b → R b d → R a d [grind.ematch.instance] Rtrans: R b c → R c e → R b e -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : R a b → R b c → R c d → R d e → R a d := by grind @@ -85,7 +85,7 @@ error: `@[grind →] theorem using_grind_fwd.StransBad` failed to find patterns set_option trace.grind.debug.ematch.pattern true in /-- -info: [grind.debug.ematch.pattern] place: S a b ∨ R a b +trace: [grind.debug.ematch.pattern] place: S a b ∨ R a b [grind.debug.ematch.pattern] collect: S a b ∨ R a b [grind.debug.ematch.pattern] arg: S a b, support: false [grind.debug.ematch.pattern] collect: S a b @@ -104,13 +104,13 @@ info: [grind.debug.ematch.pattern] place: S a b ∨ R a b [grind.debug.ematch.pattern] found full coverage [grind.ematch.pattern] Strans: [S #4 #3, S #3 #2] -/ -#guard_msgs (info) in +#guard_msgs (trace) in @[grind→] theorem Strans (a b c : Nat) : S a b ∨ R a b → S b c → S a c := sorry /-- -info: [grind.ematch.instance] Strans: S a b ∨ R a b → S b c → S a c +trace: [grind.ematch.instance] Strans: S a b ∨ R a b → S b c → S a c -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : S a b → S b c → S a c := by grind @@ -122,14 +122,14 @@ opaque P : Nat → Prop opaque Q : Nat → Prop opaque f : Nat → Nat → Nat -/-- info: [grind.ematch.pattern] pqf: [f #2 #1] -/ -#guard_msgs (info) in +/-- trace: [grind.ematch.pattern] pqf: [f #2 #1] -/ +#guard_msgs (trace) in @[grind←] theorem pqf : Q x → P (f x y) := sorry /-- -info: [grind.ematch.instance] pqf: Q a → P (f a b) +trace: [grind.ematch.instance] pqf: Q a → P (f a b) -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : Q 0 → Q 1 → Q 2 → Q 3 → ¬ P (f a b) → a = 1 → False := by grind @@ -148,18 +148,18 @@ error: `@[grind →] theorem using_grind_fwd2.pqfBad` failed to find patterns in @[grind→] theorem pqfBad : Q x → P (f x y) := sorry /-- -info: [grind.ematch.pattern] pqf: [Q #1] +trace: [grind.ematch.pattern] pqf: [Q #1] -/ -#guard_msgs (info) in +#guard_msgs (trace) in @[grind→] theorem pqf : Q x → P (f x x) := sorry /-- -info: [grind.ematch.instance] pqf: Q 3 → P (f 3 3) +trace: [grind.ematch.instance] pqf: Q 3 → P (f 3 3) [grind.ematch.instance] pqf: Q 2 → P (f 2 2) [grind.ematch.instance] pqf: Q 1 → P (f 1 1) [grind.ematch.instance] pqf: Q 0 → P (f 0 0) -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : Q 0 → Q 1 → Q 2 → Q 3 → ¬ P (f a a) → a = 1 → False := by grind @@ -184,9 +184,9 @@ error: `@[grind ←] theorem using_grind_mixed.pqBad2` failed to find patterns i /-- -info: [grind.ematch.pattern] pqBad: [Q #3 #1, P #3 #2] +trace: [grind.ematch.pattern] pqBad: [Q #3 #1, P #3 #2] -/ -#guard_msgs (info) in +#guard_msgs (trace) in @[grind] theorem pqBad : P x y → Q x z := sorry example : P a b → Q a c := by @@ -201,9 +201,9 @@ opaque f : Nat → Nat opaque g : Nat → Nat → Nat /-- -info: [grind.ematch.pattern] fq: [g #0 (f #0)] +trace: [grind.ematch.pattern] fq: [g #0 (f #0)] -/ -#guard_msgs (info) in +#guard_msgs (trace) in @[grind =_] theorem fq : f x = g x (f x) := sorry @@ -215,10 +215,10 @@ opaque f : Nat → Nat opaque g : Nat → Nat → Nat /-- -info: [grind.ematch.pattern] fq: [f #0] +trace: [grind.ematch.pattern] fq: [f #0] [grind.ematch.pattern] fq: [g #0 (g #0 #0)] -/ -#guard_msgs (info) in +#guard_msgs (trace) in @[grind _=_] theorem fq : f x = g x (g x x) := sorry diff --git a/tests/lean/run/grind_ematch2.lean b/tests/lean/run/grind_ematch2.lean index 140e0d62ce..097ce62a43 100644 --- a/tests/lean/run/grind_ematch2.lean +++ b/tests/lean/run/grind_ematch2.lean @@ -43,14 +43,14 @@ example (as bs cs : Array α) (v₁ v₂ : α) grind /-- -info: [grind.ematch.instance] Array.size_set: (cs.set i₃ v₃ ⋯).size = cs.size +trace: [grind.ematch.instance] Array.size_set: (cs.set i₃ v₃ ⋯).size = cs.size [grind.ematch.instance] Array.size_set: (bs.set i₂ v₂ ⋯).size = bs.size [grind.ematch.instance] Array.size_set: (as.set i₁ v₁ ⋯).size = as.size [grind.ematch.instance] Array.getElem_set_ne: ∀ (pj : j < cs.size), i₃ ≠ j → (cs.set i₃ v₃ ⋯)[j] = cs[j] [grind.ematch.instance] Array.getElem_set_ne: ∀ (pj : j < bs.size), i₂ ≠ j → (bs.set i₂ v₂ ⋯)[j] = bs[j] [grind.ematch.instance] Array.getElem_set_ne: ∀ (pj : j < as.size), i₁ ≠ j → (as.set i₁ v₁ ⋯)[j] = as[j] -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (as bs cs ds : Array α) (v₁ v₂ v₃ : α) (i₁ i₂ i₃ j : Nat) (h₁ : i₁ < as.size) @@ -69,8 +69,8 @@ opaque f (a b : α) : α := a @[grind =] theorem fx : f x (f x x) = x := sorry /-- -info: [grind.ematch.instance] fx: f a (f a a) = a +trace: [grind.ematch.instance] fx: f a (f a a) = a -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : a = b₁ → c = f b₁ b₂ → f a c ≠ a → a = b₂ → False := by grind diff --git a/tests/lean/run/grind_ematch_patterns.lean b/tests/lean/run/grind_ematch_patterns.lean index bbbaef764f..0cb8b319bf 100644 --- a/tests/lean/run/grind_ematch_patterns.lean +++ b/tests/lean/run/grind_ematch_patterns.lean @@ -3,10 +3,10 @@ def replicate : (n : Nat) → (a : α) → List α | n+1, a => a :: replicate n a /-- -info: [grind.ematch.pattern] replicate.eq_1: [@replicate #1 `[0] #0] +trace: [grind.ematch.pattern] replicate.eq_1: [@replicate #1 `[0] #0] [grind.ematch.pattern] replicate.eq_2: [@replicate #2 (#0 + 1) #1] -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.ematch.pattern true in attribute [grind] replicate diff --git a/tests/lean/run/grind_eq.lean b/tests/lean/run/grind_eq.lean index 28ba3f95ed..c3163306c4 100644 --- a/tests/lean/run/grind_eq.lean +++ b/tests/lean/run/grind_eq.lean @@ -14,12 +14,12 @@ set_option trace.grind.ematch.instance true set_option trace.grind.assert true /-- -info: [grind.assert] f (y + 1) = a +trace: [grind.assert] f (y + 1) = a [grind.assert] ¬a = g (f y) [grind.ematch.instance] f.eq_2: f y.succ = g (f y) [grind.assert] f (y + 1) = g (f y) -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : f (y + 1) = a → a = g (f y):= by grind @@ -29,7 +29,7 @@ example : f (y + 1) = a → a = g (f y):= by | x::xs => x :: app xs ys /-- -info: [grind.assert] app [1, 2] ys = xs +trace: [grind.assert] app [1, 2] ys = xs [grind.assert] ¬xs = 1 :: 2 :: ys [grind.ematch.instance] app.eq_2: app [1, 2] ys = 1 :: app [2] ys [grind.assert] app [1, 2] ys = 1 :: app [2] ys @@ -38,7 +38,7 @@ info: [grind.assert] app [1, 2] ys = xs [grind.ematch.instance] app.eq_1: app [] ys = ys [grind.assert] app [] ys = ys -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : app [1, 2] ys = xs → xs = 1::2::ys := by grind @@ -48,12 +48,12 @@ opaque q : Nat → Prop @[grind =] theorem pq : p x x ↔ q x := by sorry /-- -info: [grind.assert] p a a +trace: [grind.assert] p a a [grind.assert] ¬q a [grind.ematch.instance] pq: p a a ↔ q a [grind.assert] p a a = q a -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : p a a → q a := by grind @@ -65,7 +65,7 @@ theorem appV_assoc (a : Vector α n) (b : Vector α m) (c : Vector α n') : HEq (appV a (appV b c)) (appV (appV a b) c) := sorry /-- -info: [grind.assert] x1 = appV a_2 b +trace: [grind.assert] x1 = appV a_2 b [grind.assert] x2 = appV x1 c [grind.assert] x3 = appV b c [grind.assert] x4 = appV a_2 x3 @@ -73,6 +73,6 @@ info: [grind.assert] x1 = appV a_2 b [grind.ematch.instance] appV_assoc: HEq (appV a_2 (appV b c)) (appV (appV a_2 b) c) [grind.assert] HEq (appV a_2 (appV b c)) (appV (appV a_2 b) c) -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : x1 = appV a b → x2 = appV x1 c → x3 = appV b c → x4 = appV a x3 → HEq x2 x4 := by grind diff --git a/tests/lean/run/grind_eq_bwd.lean b/tests/lean/run/grind_eq_bwd.lean index 46b3f3db10..fc88bc13db 100644 --- a/tests/lean/run/grind_eq_bwd.lean +++ b/tests/lean/run/grind_eq_bwd.lean @@ -1,3 +1,5 @@ +set_option grind.warning false + theorem dummy (x : Nat) : x = x := rfl @@ -17,7 +19,7 @@ def one : α := sorry theorem inv_eq {a b : α} (w : mul a b = one) : inv a = b := sorry /-- -info: [grind.ematch.pattern] inv_eq: [@Lean.Grind.eqBwdPattern `[α] (inv #2) #1] +trace: [grind.ematch.pattern] inv_eq: [@Lean.Grind.eqBwdPattern `[α] (inv #2) #1] -/ #guard_msgs in set_option trace.grind.ematch.pattern true in @@ -52,10 +54,10 @@ example (s : S) : a ≠ s.f false → a = inv (s.f true) → False := by grind /-- -info: [grind.ematch.instance] inv_eq: mul (s.f true) (s.f false) = one → inv (s.f true) = s.f false +trace: [grind.ematch.instance] inv_eq: mul (s.f true) (s.f false) = one → inv (s.f true) = s.f false [grind.ematch.instance] S.h: mul (s.f true) (s.f false) = one -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.ematch.instance true in example (s : S) : inv (s.f true) = s.f false := by grind diff --git a/tests/lean/run/grind_eq_pattern.lean b/tests/lean/run/grind_eq_pattern.lean index 9921bd99d9..f4da2c60a0 100644 --- a/tests/lean/run/grind_eq_pattern.lean +++ b/tests/lean/run/grind_eq_pattern.lean @@ -1,32 +1,32 @@ reset_grind_attrs% /-- -info: [grind.ematch.pattern] List.append_ne_nil_of_left_ne_nil: [@HAppend.hAppend (List #3) (List _) (List _) _ #2 #0] +trace: [grind.ematch.pattern] List.append_ne_nil_of_left_ne_nil: [@HAppend.hAppend (List #3) (List _) (List _) _ #2 #0] -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.ematch.pattern true in attribute [grind] List.append_ne_nil_of_left_ne_nil /-- -info: [grind.ematch.pattern] List.append_ne_nil_of_right_ne_nil: [@HAppend.hAppend (List #3) (List _) (List _) _ #1 #2] +trace: [grind.ematch.pattern] List.append_ne_nil_of_right_ne_nil: [@HAppend.hAppend (List #3) (List _) (List _) _ #1 #2] -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.ematch.pattern true in attribute [grind] List.append_ne_nil_of_right_ne_nil -/-- info: [grind.ematch.pattern] List.getLast?_eq_some_iff: [@List.getLast? #2 #1, @some _ #0] -/ -#guard_msgs (info) in +/-- trace: [grind.ematch.pattern] List.getLast?_eq_some_iff: [@List.getLast? #2 #1, @some _ #0] -/ +#guard_msgs (trace) in set_option trace.grind.ematch.pattern true in attribute [grind =] List.getLast?_eq_some_iff /-- -info: [grind.assert] xs.getLast? = b? +trace: [grind.assert] xs.getLast? = b? [grind.assert] b? = some 10 [grind.assert] xs = [] [grind.assert] (xs.getLast? = some 10) = ∃ ys, xs = ys ++ [10] [grind.assert] xs = w ++ [10] [grind.assert] ¬w ++ [10] = [] -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.assert true in example (xs : List Nat) : xs.getLast? = b? → b? = some 10 → xs ≠ [] := by grind diff --git a/tests/lean/run/grind_erase_attr.lean b/tests/lean/run/grind_erase_attr.lean index 94e2b914ac..13d03834e4 100644 --- a/tests/lean/run/grind_erase_attr.lean +++ b/tests/lean/run/grind_erase_attr.lean @@ -13,10 +13,10 @@ attribute [-grind] fthm' set_option trace.grind.assert true /-- -info: [grind.assert] ¬f (f (f a)) = f a +trace: [grind.assert] ¬f (f (f a)) = f a [grind.assert] f (f a) = f a -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : f (f (f a)) = f a := by grind @@ -27,9 +27,9 @@ error: unsolved goals a : Nat ⊢ f (f (f a)) = f a --- -info: [grind.assert] ¬f (f (f a)) = f a +trace: [grind.assert] ¬f (f (f a)) = f a -/ -#guard_msgs (info, error) in +#guard_msgs (trace, error) in example : f (f (f a)) = f a := by fail_if_success grind @@ -61,11 +61,11 @@ error: unsolved goals a b : Nat ⊢ g a = b → a = 0 → b = 1 --- -info: [grind.assert] g a = b +trace: [grind.assert] g a = b [grind.assert] a = 0 [grind.assert] ¬b = 1 -/ -#guard_msgs (info, error) in +#guard_msgs (trace, error) in example : g a = b → a = 0 → b = 1 := by fail_if_success grind diff --git a/tests/lean/run/grind_implies.lean b/tests/lean/run/grind_implies.lean index 30007828b4..ca350f73f3 100644 --- a/tests/lean/run/grind_implies.lean +++ b/tests/lean/run/grind_implies.lean @@ -2,7 +2,7 @@ set_option trace.grind.eqc true set_option trace.grind.internalize true /-- -info: [grind.internalize] p → q +trace: [grind.internalize] p → q [grind.internalize] p [grind.internalize] q [grind.eqc] (p → q) = True @@ -10,12 +10,12 @@ info: [grind.internalize] p → q [grind.eqc] (p → q) = q [grind.eqc] q = False -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (p q : Prop) : (p → q) → p → q := by grind /-- -info: [grind.internalize] p → q +trace: [grind.internalize] p → q [grind.internalize] p [grind.internalize] q [grind.eqc] (p → q) = True @@ -23,12 +23,12 @@ info: [grind.internalize] p → q [grind.eqc] p = False [grind.eqc] p = True -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (p q : Prop) : (p → q) → ¬q → ¬p := by grind /-- -info: [grind.internalize] (p → q) = r +trace: [grind.internalize] (p → q) = r [grind.internalize] Prop [grind.internalize] p → q [grind.internalize] p @@ -40,13 +40,13 @@ info: [grind.internalize] (p → q) = r [grind.eqc] (p → q) = True [grind.eqc] r = False -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (p q : Prop) : (p → q) = r → ¬p → r := by grind /-- -info: [grind.internalize] (p → q) = r +trace: [grind.internalize] (p → q) = r [grind.internalize] Prop [grind.internalize] p → q [grind.internalize] p @@ -58,12 +58,12 @@ info: [grind.internalize] (p → q) = r [grind.eqc] (p → q) = True [grind.eqc] r = False -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (p q : Prop) : (p → q) = r → q → r := by grind /-- -info: [grind.internalize] (p → q) = r +trace: [grind.internalize] (p → q) = r [grind.internalize] Prop [grind.internalize] p → q [grind.internalize] p @@ -76,12 +76,12 @@ info: [grind.internalize] (p → q) = r [grind.eqc] p = False [grind.eqc] p = True -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (p q : Prop) : (p → q) = r → ¬q → r → ¬p := by grind /-- -info: [grind.internalize] (p → q) = r +trace: [grind.internalize] (p → q) = r [grind.internalize] Prop [grind.internalize] p → q [grind.internalize] p @@ -94,6 +94,6 @@ info: [grind.internalize] (p → q) = r [grind.eqc] p = True [grind.eqc] p = False -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (p q : Prop) : (p → q) = r → ¬q → ¬r → p := by grind diff --git a/tests/lean/run/grind_lazy_ite.lean b/tests/lean/run/grind_lazy_ite.lean index 7aafb0df92..d25eea3da8 100644 --- a/tests/lean/run/grind_lazy_ite.lean +++ b/tests/lean/run/grind_lazy_ite.lean @@ -5,16 +5,16 @@ def f (n : Nat) (m : Nat) := n /-- -info: [grind.ematch.instance] f.eq_def: f 5 m = if 5 < m then f (5 + 1) m + 5 else 5 +trace: [grind.ematch.instance] f.eq_def: f 5 m = if 5 < m then f (5 + 1) m + 5 else 5 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.ematch.instance true in example : f 5 m > 0 := by fail_if_success grind (splits := 0) [f.eq_def] sorry -/-- info: [grind.ematch.instance] f.eq_def: f 5 m = if 5 < m then f (5 + 1) m + 5 else 5 -/ -#guard_msgs (info) in +/-- trace: [grind.ematch.instance] f.eq_def: f 5 m = if 5 < m then f (5 + 1) m + 5 else 5 -/ +#guard_msgs (trace) in set_option trace.grind.ematch.instance true in example : f 5 m > 0 := by grind (splits := 1) [f.eq_def] diff --git a/tests/lean/run/grind_match1.lean b/tests/lean/run/grind_match1.lean index b507381a85..6a72871ade 100644 --- a/tests/lean/run/grind_match1.lean +++ b/tests/lean/run/grind_match1.lean @@ -11,7 +11,7 @@ set_option trace.grind.split.candidate true set_option trace.grind.split.resolved true /-- -info: [grind.assert] (match as, bs with +trace: [grind.assert] (match as, bs with | [], x => bs | head :: head_1 :: tail, [] => [] | x :: xs, ys => x :: g xs ys) = @@ -34,7 +34,7 @@ info: [grind.assert] (match as, bs with | head :: head_1 :: tail, [] => [] | x :: xs, ys => x :: g xs ys -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (f : Nat → List Nat) : g as bs = d → bs = [] → a₁ :: f 0 = as → f 0 = a₂ :: f 1 → d = [] := by unfold g grind diff --git a/tests/lean/run/grind_match2.lean b/tests/lean/run/grind_match2.lean index d54abd8276..108c4fa0c2 100644 --- a/tests/lean/run/grind_match2.lean +++ b/tests/lean/run/grind_match2.lean @@ -17,11 +17,11 @@ def h (as : List Nat) := | _::_::_ => 3 /-- -info: [grind] closed `grind.1` +trace: [grind] closed `grind.1` [grind] closed `grind.2` [grind] closed `grind.3` -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind true in example : h as ≠ 0 := by grind [h.eq_def] diff --git a/tests/lean/run/grind_mbtc_1.lean b/tests/lean/run/grind_mbtc_1.lean index 7a466b7a00..ce5b32f940 100644 --- a/tests/lean/run/grind_mbtc_1.lean +++ b/tests/lean/run/grind_mbtc_1.lean @@ -9,11 +9,11 @@ example (f : Int → Int) (x : Int) -- and we have an invalid counterexample where `x := 1`, -- but `f x` and `f 1` have different assignments. /-- -info: [grind.cutsat.model] x := 1 +trace: [grind.cutsat.model] x := 1 [grind.cutsat.model] f x := 2 [grind.cutsat.model] f 1 := 5 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.cutsat.model true in example (f : Int → Int) (x : Int) : 0 ≤ x → x ≠ 0 → x ≤ 1 → f x = 2 → f 1 = 2 := by @@ -21,11 +21,11 @@ example (f : Int → Int) (x : Int) sorry /-- -info: [grind.cutsat.model] x := 2 +trace: [grind.cutsat.model] x := 2 [grind.cutsat.model] f x := 2 [grind.cutsat.model] f 1 := 5 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.cutsat.model true in example (f : Int → Int) (x : Int) : 0 ≤ x → x ≠ 0 → x ≤ 3 → f x = 2 → f 1 = 2 := by @@ -46,21 +46,21 @@ example (f : Nat → Nat → Nat) (x y : Nat) -- `b` must not be `2`. Otherwise, `f (b+1)` and `f 3` must be equal. -/-- info: [grind.cutsat.model] b := 3 -/ -#guard_msgs (info) in +/-- trace: [grind.cutsat.model] b := 3 -/ +#guard_msgs (trace) in set_option trace.grind.cutsat.model true in example (f : Int → α) (a b : Int) : b > 1 → f (b + 1) = x → f 3 = y → x = y := by (fail_if_success grind); sorry -- `b` must not be `2`. Otherwise, `f (b+1)` and `f 3` must be equal. /-- -info: [grind.cutsat.model] x := 7 +trace: [grind.cutsat.model] x := 7 [grind.cutsat.model] y := 8 [grind.cutsat.model] b := 3 [grind.cutsat.model] f 3 := 8 [grind.cutsat.model] f (b + 1) := 7 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.cutsat.model true in example (f : Int → Int) (a b : Int) : b > 1 → f (b + 1) = x → f 3 = y → x = y := by (fail_if_success grind); sorry diff --git a/tests/lean/run/grind_mvar.lean b/tests/lean/run/grind_mvar.lean index d8fd669659..e6972526a8 100644 --- a/tests/lean/run/grind_mvar.lean +++ b/tests/lean/run/grind_mvar.lean @@ -5,7 +5,7 @@ set_option grind.warning false attribute [grind →] Array.eq_empty_of_append_eq_empty eq_nil_of_length_eq_zero attribute [grind] Vector.getElem?_append getElem?_dropLast -#guard_msgs (info) in -- should not report any issues +#guard_msgs (trace) in -- should not report any issues set_option trace.grind.issues true theorem dropLast_concat : dropLast (l₁ ++ [b]) = l₁ := by fail_if_success grind (gen := 6) diff --git a/tests/lean/run/grind_nested_proofs.lean b/tests/lean/run/grind_nested_proofs.lean index a42f9781b2..9cd4396399 100644 --- a/tests/lean/run/grind_nested_proofs.lean +++ b/tests/lean/run/grind_nested_proofs.lean @@ -22,17 +22,17 @@ detect equalities between array access terms. -/ /-- -info: [Meta.debug] [‹i < a.toList.length›, ‹j < a.toList.length›, ‹j < b.toList.length›] +trace: [Meta.debug] [‹i < a.toList.length›, ‹j < a.toList.length›, ‹j < b.toList.length›] [Meta.debug] [a[i], b[j], a[j]] -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (i j : Nat) (a b : Array Nat) (h1 : j < a.size) (h : j < b.size) (h2 : i ≤ j) : a[i] < a[j] + b[j] → i = j → a = b → False := by grind -mbtc on_failure fallback /-- -info: [Meta.debug] [‹i < a.toList.length›, ‹j < a.toList.length›, ‹j < b.toList.length›] +trace: [Meta.debug] [‹i < a.toList.length›, ‹j < a.toList.length›, ‹j < b.toList.length›] [Meta.debug] [a[i], a[j]] -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (i j : Nat) (a b : Array Nat) (h1 : j < a.size) (h : j < b.size) (h2 : i ≤ j) : a[i] < a[j] + b[j] → i = j → False := by grind -mbtc on_failure fallback diff --git a/tests/lean/run/grind_norm_levels.lean b/tests/lean/run/grind_norm_levels.lean index 73f86e08fb..f692c87b68 100644 --- a/tests/lean/run/grind_norm_levels.lean +++ b/tests/lean/run/grind_norm_levels.lean @@ -11,8 +11,8 @@ def fallback : Fallback := do -- `grind` final state must contain only two `g`-applications set_option trace.Meta.debug true in /-- -info: [Meta.debug] [g (a, b), g (g (a, b))] +trace: [Meta.debug] [g (a, b), g (g (a, b))] -/ -#guard_msgs (info) in +#guard_msgs (trace) in example {β : Type v} {α : Type u} (a c : α) (b d : β) : g.{max u v + 1} (a, b) = (c, d) → g (g.{max (u+1) (v+1)} (a, b)) = (c, d) → False := by grind on_failure fallback diff --git a/tests/lean/run/grind_offset.lean b/tests/lean/run/grind_offset.lean index 1de16dc996..d8226fa895 100644 --- a/tests/lean/run/grind_offset.lean +++ b/tests/lean/run/grind_offset.lean @@ -9,52 +9,52 @@ set_option trace.grind.ematch.pattern true set_option trace.grind.ematch.instance true set_option trace.grind.assert true -/-- info: [grind.ematch.pattern] f.eq_2: [f (#0 + 1)] -/ +/-- trace: [grind.ematch.pattern] f.eq_2: [f (#0 + 1)] -/ #guard_msgs in grind_pattern f.eq_2 => f (x + 1) /-- -info: [grind.assert] f (y + 1) = a +trace: [grind.assert] f (y + 1) = a [grind.assert] ¬a = g (f y) [grind.ematch.instance] f.eq_2: f y.succ = g (f y) [grind.assert] f (y + 1) = g (f y) -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : f (y + 1) = a → a = g (f y) := by grind /-- -info: [grind.assert] f 1 = a +trace: [grind.assert] f 1 = a [grind.assert] ¬a = g (f 0) [grind.ematch.instance] f.eq_2: f (Nat.succ 0) = g (f 0) [grind.assert] f 1 = g (f 0) -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : f 1 = a → a = g (f 0) := by grind /-- -info: [grind.assert] f 10 = a +trace: [grind.assert] f 10 = a [grind.assert] ¬a = g (f 9) [grind.ematch.instance] f.eq_2: f (Nat.succ 8) = g (f 8) [grind.ematch.instance] f.eq_2: f (Nat.succ 9) = g (f 9) [grind.assert] f 9 = g (f 8) [grind.assert] f 10 = g (f 9) -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : f 10 = a → a = g (f 9) := by grind /-- -info: [grind.assert] f (c + 2) = a +trace: [grind.assert] f (c + 2) = a [grind.assert] ¬a = g (g (f c)) [grind.ematch.instance] f.eq_2: f (c + 1).succ = g (f (c + 1)) [grind.assert] f (c + 2) = g (f (c + 1)) [grind.ematch.instance] f.eq_2: f c.succ = g (f c) [grind.assert] f (c + 1) = g (f c) -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : f (c + 2) = a → a = g (g (f c)) := by grind @@ -64,86 +64,86 @@ example : f (c + 2) = a → a = g (g (f c)) := by | 1 => 10 | a+2 => g (foo a) -/-- info: [grind.ematch.pattern] foo.eq_3: [foo (#0 + 2)] -/ +/-- trace: [grind.ematch.pattern] foo.eq_3: [foo (#0 + 2)] -/ #guard_msgs in grind_pattern foo.eq_3 => foo (a_2 + 2) -- The instance is correctly found in the following example. -- TODO: to complete the proof, we need linear arithmetic support to prove that `b + 2 = c + 1`. /-- -info: [grind.assert] foo (c + 1) = a +trace: [grind.assert] foo (c + 1) = a [grind.assert] c = b + 1 [grind.assert] ¬a = g (foo b) [grind.ematch.instance] foo.eq_3: foo b.succ.succ = g (foo b) [grind.assert] foo (b + 2) = g (foo b) -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : foo (c + 1) = a → c = b + 1 → a = g (foo b) := by grind set_option trace.grind.assert false /-- -info: [grind.ematch.instance] f.eq_2: f (x + 99).succ = g (f (x + 99)) +trace: [grind.ematch.instance] f.eq_2: f (x + 99).succ = g (f (x + 99)) [grind.ematch.instance] f.eq_2: f (x + 98).succ = g (f (x + 98)) -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : f (x + 100) = a → a = b := by fail_if_success grind (ematch := 2) sorry /-- -info: [grind.ematch.instance] f.eq_2: f (x + 99).succ = g (f (x + 99)) +trace: [grind.ematch.instance] f.eq_2: f (x + 99).succ = g (f (x + 99)) [grind.ematch.instance] f.eq_2: f (x + 98).succ = g (f (x + 98)) [grind.ematch.instance] f.eq_2: f (x + 97).succ = g (f (x + 97)) [grind.ematch.instance] f.eq_2: f (x + 96).succ = g (f (x + 96)) [grind.ematch.instance] f.eq_2: f (x + 95).succ = g (f (x + 95)) -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : f (x + 100) = a → a = b := by fail_if_success grind (ematch := 5) sorry /-- -info: [grind.ematch.instance] f.eq_2: f (x + 99).succ = g (f (x + 99)) +trace: [grind.ematch.instance] f.eq_2: f (x + 99).succ = g (f (x + 99)) [grind.ematch.instance] f.eq_2: f (x + 98).succ = g (f (x + 98)) [grind.ematch.instance] f.eq_2: f (x + 97).succ = g (f (x + 97)) [grind.ematch.instance] f.eq_2: f (x + 96).succ = g (f (x + 96)) -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : f (x + 100) = a → a = b := by fail_if_success grind (ematch := 100) (instances := 4) sorry /-- -info: [grind.ematch.instance] f.eq_2: f (y + 9).succ = g (f (y + 9)) +trace: [grind.ematch.instance] f.eq_2: f (y + 9).succ = g (f (y + 9)) [grind.ematch.instance] f.eq_2: f (x + 99).succ = g (f (x + 99)) [grind.ematch.instance] f.eq_2: f (x + 98).succ = g (f (x + 98)) [grind.ematch.instance] f.eq_2: f (y + 8).succ = g (f (y + 8)) [grind.ematch.instance] f.eq_2: f (y + 7).succ = g (f (y + 7)) -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : f (x + 100) = a → f (y + 10) = c → a = b := by fail_if_success grind (ematch := 100) (instances := 5) sorry /-- -info: [grind.ematch.instance] f.eq_2: f (x + 99).succ = g (f (x + 99)) +trace: [grind.ematch.instance] f.eq_2: f (x + 99).succ = g (f (x + 99)) [grind.ematch.instance] f.eq_2: f (x + 98).succ = g (f (x + 98)) -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : f (x + 100) = a → a = b := by fail_if_success grind (gen := 2) sorry /-- -info: [grind.ematch.instance] f.eq_2: f (x + 99).succ = g (f (x + 99)) +trace: [grind.ematch.instance] f.eq_2: f (x + 99).succ = g (f (x + 99)) [grind.ematch.instance] f.eq_2: f (x + 98).succ = g (f (x + 98)) [grind.ematch.instance] f.eq_2: f (x + 97).succ = g (f (x + 97)) [grind.ematch.instance] f.eq_2: f (x + 96).succ = g (f (x + 96)) [grind.ematch.instance] f.eq_2: f (x + 95).succ = g (f (x + 95)) -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : f (x + 100) = a → a = b := by fail_if_success grind (gen := 5) sorry diff --git a/tests/lean/run/grind_offset_cnstr.lean b/tests/lean/run/grind_offset_cnstr.lean index f9cd7d3e32..c90d554bf5 100644 --- a/tests/lean/run/grind_offset_cnstr.lean +++ b/tests/lean/run/grind_offset_cnstr.lean @@ -1,7 +1,8 @@ +set_option grind.warning false set_option grind.debug true /-- -info: [grind.offset.internalize.term] a1 ↦ #0 +trace: [grind.offset.internalize.term] a1 ↦ #0 [grind.offset.internalize.term] a2 ↦ #1 [grind.offset.internalize] a1 + 1 ≤ a2 ↦ #0 + 1 ≤ #1 [grind.offset.internalize.term] a3 ↦ #2 @@ -9,7 +10,7 @@ info: [grind.offset.internalize.term] a1 ↦ #0 [grind.offset.internalize.term] a4 ↦ #3 [grind.offset.internalize] a3 ≤ a4 ↦ #2 ≤ #3 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.offset.internalize true in example (a1 a2 a3) : a1 + 1 ≤ a2 → a2 ≤ a3 + 2 → a3 ≤ a4 → False := by @@ -17,14 +18,14 @@ example (a1 a2 a3) : sorry /-- -info: [grind.offset.internalize.term] a1 ↦ #0 +trace: [grind.offset.internalize.term] a1 ↦ #0 [grind.offset.internalize.term] a2 ↦ #1 [grind.offset.dist] #0 + 1 ≤ #1 [grind.offset.internalize.term] a3 ↦ #2 [grind.offset.dist] #1 ≤ #2 [grind.offset.dist] #0 + 1 ≤ #2 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.offset.internalize.term true in set_option trace.grind.offset.dist true in example (a1 a2 a3 : Nat) : @@ -34,14 +35,14 @@ example (a1 a2 a3 : Nat) : /-- -info: [grind.offset.internalize.term] a1 ↦ #0 +trace: [grind.offset.internalize.term] a1 ↦ #0 [grind.offset.internalize.term] a2 ↦ #1 [grind.offset.dist] #0 + 1 ≤ #1 [grind.offset.internalize.term] a3 ↦ #2 [grind.offset.dist] #1 + 2 ≤ #2 [grind.offset.dist] #0 + 3 ≤ #2 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.offset.internalize.term true in set_option trace.grind.offset.dist true in example (a1 a2 a3 : Nat) : @@ -50,14 +51,14 @@ example (a1 a2 a3 : Nat) : sorry /-- -info: [grind.offset.internalize.term] a1 ↦ #0 +trace: [grind.offset.internalize.term] a1 ↦ #0 [grind.offset.internalize.term] a2 ↦ #1 [grind.offset.dist] #0 + 1 ≤ #1 [grind.offset.internalize.term] a3 ↦ #2 [grind.offset.dist] #1 ≤ #2 + 2 [grind.offset.dist] #0 ≤ #2 + 1 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.offset.internalize.term true in set_option trace.grind.offset.dist true in example (a1 a2 a3 : Nat) : @@ -66,14 +67,14 @@ example (a1 a2 a3 : Nat) : sorry /-- -info: [grind.offset.internalize.term] a1 ↦ #0 +trace: [grind.offset.internalize.term] a1 ↦ #0 [grind.offset.internalize.term] a2 ↦ #1 [grind.offset.dist] #0 ≤ #1 [grind.offset.internalize.term] a3 ↦ #2 [grind.offset.dist] #1 ≤ #2 [grind.offset.dist] #0 ≤ #2 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.offset.internalize.term true in set_option trace.grind.offset.dist true in example (a1 a2 a3 : Nat) : @@ -82,14 +83,14 @@ example (a1 a2 a3 : Nat) : sorry /-- -info: [grind.offset.internalize.term] a1 ↦ #0 +trace: [grind.offset.internalize.term] a1 ↦ #0 [grind.offset.internalize.term] a2 ↦ #1 [grind.offset.dist] #0 ≤ #1 [grind.offset.internalize.term] a3 ↦ #2 [grind.offset.dist] #1 + 2 ≤ #2 [grind.offset.dist] #0 + 2 ≤ #2 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.offset.internalize.term true in set_option trace.grind.offset.dist true in example (a1 a2 a3 : Nat) : @@ -98,14 +99,14 @@ example (a1 a2 a3 : Nat) : sorry /-- -info: [grind.offset.internalize.term] a1 ↦ #0 +trace: [grind.offset.internalize.term] a1 ↦ #0 [grind.offset.internalize.term] a2 ↦ #1 [grind.offset.dist] #0 ≤ #1 [grind.offset.internalize.term] a3 ↦ #2 [grind.offset.dist] #1 ≤ #2 + 5 [grind.offset.dist] #0 ≤ #2 + 5 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.offset.internalize.term true in set_option trace.grind.offset.dist true in example (a1 a2 a3 : Nat) : @@ -114,14 +115,14 @@ example (a1 a2 a3 : Nat) : sorry /-- -info: [grind.offset.internalize.term] a1 ↦ #0 +trace: [grind.offset.internalize.term] a1 ↦ #0 [grind.offset.internalize.term] a2 ↦ #1 [grind.offset.dist] #0 ≤ #1 + 5 [grind.offset.internalize.term] a3 ↦ #2 [grind.offset.dist] #1 ≤ #2 [grind.offset.dist] #0 ≤ #2 + 5 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.offset.internalize.term true in set_option trace.grind.offset.dist true in example (a1 a2 a3 : Nat) : @@ -130,14 +131,14 @@ example (a1 a2 a3 : Nat) : sorry /-- -info: [grind.offset.internalize.term] a1 ↦ #0 +trace: [grind.offset.internalize.term] a1 ↦ #0 [grind.offset.internalize.term] a2 ↦ #1 [grind.offset.dist] #0 ≤ #1 + 5 [grind.offset.internalize.term] a3 ↦ #2 [grind.offset.dist] #1 + 2 ≤ #2 [grind.offset.dist] #0 ≤ #2 + 3 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.offset.internalize.term true in set_option trace.grind.offset.dist true in example (a1 a2 a3 : Nat) : @@ -146,14 +147,14 @@ example (a1 a2 a3 : Nat) : sorry /-- -info: [grind.offset.internalize.term] a1 ↦ #0 +trace: [grind.offset.internalize.term] a1 ↦ #0 [grind.offset.internalize.term] a2 ↦ #1 [grind.offset.dist] #0 ≤ #1 + 5 [grind.offset.internalize.term] a3 ↦ #2 [grind.offset.dist] #1 ≤ #2 + 2 [grind.offset.dist] #0 ≤ #2 + 7 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.offset.internalize.term true in set_option trace.grind.offset.dist true in example (a1 a2 a3 : Nat) : @@ -169,14 +170,14 @@ example (a1 a2 a3 : Nat) : sorry /-- -info: [grind.offset.internalize.term] a1 ↦ #0 +trace: [grind.offset.internalize.term] a1 ↦ #0 [grind.offset.internalize.term] a2 ↦ #1 [grind.offset.dist] #0 ≤ #1 + 2 [grind.offset.internalize.term] a3 ↦ #2 [grind.offset.dist] #1 + 3 ≤ #2 [grind.offset.dist] #0 + 1 ≤ #2 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.offset.internalize.term true in set_option trace.grind.offset.dist true in example (a1 a2 a3 : Nat) : a1 ≤ a2 + 2 → a2 + 3 ≤ a3 → False := by @@ -184,14 +185,14 @@ example (a1 a2 a3 : Nat) : a1 ≤ a2 + 2 → a2 + 3 ≤ a3 → False := by sorry /-- -info: [grind.offset.internalize.term] a2 ↦ #0 +trace: [grind.offset.internalize.term] a2 ↦ #0 [grind.offset.internalize.term] a1 ↦ #1 [grind.offset.dist] #1 + 3 ≤ #0 [grind.offset.internalize.term] a3 ↦ #2 [grind.offset.dist] #0 + 3 ≤ #2 [grind.offset.dist] #1 + 6 ≤ #2 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.offset.internalize.term true in set_option trace.grind.offset.dist true in example (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 ≤ a1 + 2) → ¬p → a2 + 3 ≤ a3 → False := by @@ -199,14 +200,14 @@ example (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 ≤ a1 + 2) → ¬p → a2 + 3 sorry /-- -info: [grind.offset.internalize.term] a2 ↦ #0 +trace: [grind.offset.internalize.term] a2 ↦ #0 [grind.offset.internalize.term] a1 ↦ #1 [grind.offset.dist] #1 ≤ #0 + 1 [grind.offset.internalize.term] a3 ↦ #2 [grind.offset.dist] #0 + 3 ≤ #2 [grind.offset.dist] #1 + 2 ≤ #2 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.offset.internalize.term true in set_option trace.grind.offset.dist true in example (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 + 2 ≤ a1) → ¬p → a2 + 3 ≤ a3 → False := by @@ -214,14 +215,14 @@ example (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 + 2 ≤ a1) → ¬p → a2 + 3 sorry /-- -info: [grind.offset.internalize.term] a2 ↦ #0 +trace: [grind.offset.internalize.term] a2 ↦ #0 [grind.offset.internalize.term] a1 ↦ #1 [grind.offset.dist] #1 + 1 ≤ #0 [grind.offset.internalize.term] a3 ↦ #2 [grind.offset.dist] #0 + 3 ≤ #2 [grind.offset.dist] #1 + 4 ≤ #2 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.offset.internalize.term true in set_option trace.grind.offset.dist true in example (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 ≤ a1) → ¬p → a2 + 3 ≤ a3 → False := by @@ -229,14 +230,14 @@ example (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 ≤ a1) → ¬p → a2 + 3 ≤ a sorry /-- -info: [grind.offset.internalize.term] a2 ↦ #0 +trace: [grind.offset.internalize.term] a2 ↦ #0 [grind.offset.internalize.term] a1 ↦ #1 [grind.offset.dist] #1 ≤ #0 [grind.offset.internalize.term] a3 ↦ #2 [grind.offset.dist] #0 + 3 ≤ #2 [grind.offset.dist] #1 + 3 ≤ #2 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.offset.internalize.term true in set_option trace.grind.offset.dist true in example (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 + 1 ≤ a1) → ¬p → a2 + 3 ≤ a3 → False := by @@ -275,45 +276,45 @@ fun {a4} p a1 a2 a3 => (Nat.lo_lo a2 a3 a4 3 3 h_2 (Nat.of_ro_eq_false a4 a3 2 (Eq.trans (Eq.symm h_3) (eq_false h_1))))))) True.intro) -/ -#guard_msgs (info) in +#guard_msgs in open Lean Grind in #print ex1._proof_1 /-! Propagate `cnstr = False` tests -/ -- The following example is solved by `grind` using constraint propagation and 0 case-splits. -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.split true in example (p q r s : Prop) (a b : Nat) : a ≤ b → b + 2 ≤ c → (a + 1 ≤ c ↔ p) → (a + 2 ≤ c ↔ s) → (a ≤ c ↔ q) → (a ≤ c + 4 ↔ r) → p ∧ q ∧ r ∧ s := by grind (splits := 0) -- The following example is solved by `grind` using constraint propagation and 0 case-splits. -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.split true in example (p q : Prop) (a b : Nat) : a ≤ b → b ≤ c → (a ≤ c ↔ p) → (a ≤ c + 1 ↔ q) → p ∧ q := by grind (splits := 0) -- The following example is solved by `grind` using constraint propagation and 0 case-splits. -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.split true in example (p q : Prop) (a b : Nat) : a ≤ b → b ≤ c + 1 → (a ≤ c + 1 ↔ p) → (a ≤ c + 2 ↔ q) → p ∧ q := by grind (splits := 0) -- The following example is solved by `grind` using constraint propagation and 0 case-splits. -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.split true in example (p r s : Prop) (a b : Nat) : a ≤ b → b + 2 ≤ c → (c ≤ a ↔ p) → (c ≤ a + 1 ↔ s) → (c + 1 ≤ a ↔ r) → ¬p ∧ ¬r ∧ ¬s := by grind (splits := 0) -- The following example is solved by `grind` using constraint propagation and 0 case-splits. -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.split true in example (p r : Prop) (a b : Nat) : a ≤ b → b ≤ c → (c + 1 ≤ a ↔ p) → (c + 2 ≤ a + 1 ↔ r) → ¬p ∧ ¬r := by grind (splits := 0) -- The following example is solved by `grind` using constraint propagation and 0 case-splits. -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.split true in example (p r : Prop) (a b : Nat) : a ≤ b → b ≤ c + 3 → (c + 5 ≤ a ↔ p) → (c + 4 ≤ a ↔ r) → ¬p ∧ ¬r := by grind (splits := 0) @@ -321,37 +322,37 @@ example (p r : Prop) (a b : Nat) : a ≤ b → b ≤ c + 3 → (c + 5 ≤ a ↔ /-! Propagate `cnstr = False` tests, but with different internalization order -/ -- The following example is solved by `grind` using constraint propagation and 0 case-splits. -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.split true in example (p q r s : Prop) (a b : Nat) : (a + 1 ≤ c ↔ p) → (a + 2 ≤ c ↔ s) → (a ≤ c ↔ q) → (a ≤ c + 4 ↔ r) → a ≤ b → b + 2 ≤ c → p ∧ q ∧ r ∧ s := by grind (splits := 0) -- The following example is solved by `grind` using constraint propagation and 0 case-splits. -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.split true in example (p q : Prop) (a b : Nat) : (a ≤ c ↔ p) → (a ≤ c + 1 ↔ q) → a ≤ b → b ≤ c → p ∧ q := by grind (splits := 0) -- The following example is solved by `grind` using constraint propagation and 0 case-splits. -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.split true in example (p q : Prop) (a b : Nat) : (a ≤ c + 1 ↔ p) → (a ≤ c + 2 ↔ q) → a ≤ b → b ≤ c + 1 → p ∧ q := by grind (splits := 0) -- The following example is solved by `grind` using constraint propagation and 0 case-splits. -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.split true in example (p r s : Prop) (a b : Nat) : (c ≤ a ↔ p) → (c ≤ a + 1 ↔ s) → (c + 1 ≤ a ↔ r) → a ≤ b → b + 2 ≤ c → ¬p ∧ ¬r ∧ ¬s := by grind (splits := 0) -- The following example is solved by `grind` using constraint propagation and 0 case-splits. -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.split true in example (p r : Prop) (a b : Nat) : (c + 1 ≤ a ↔ p) → (c + 2 ≤ a + 1 ↔ r) → a ≤ b → b ≤ c → ¬p ∧ ¬r := by grind (splits := 0) -- The following example is solved by `grind` using constraint propagation and 0 case-splits. -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.split true in example (p r : Prop) (a b : Nat) : (c + 5 ≤ a ↔ p) → (c + 4 ≤ a ↔ r) → a ≤ b → b ≤ c + 3 → ¬p ∧ ¬r := by grind (splits := 0) @@ -398,7 +399,7 @@ example (a : Nat) : a < 2 → a = 5 → False := by example (a : Nat) : a < 2 → a = b → b = c → c = 5 → False := by grind -#guard_msgs (info) in -- none of the numerals should be internalized by the offset module +#guard_msgs (trace) in -- none of the numerals should be internalized by the offset module set_option trace.grind.offset.internalize true in example (a b c d e : Nat) : a = 1 → b = 2 → c = 3 → d = 4 → e = 5 → a ≠ e := by grind diff --git a/tests/lean/run/grind_offset_model.lean b/tests/lean/run/grind_offset_model.lean index 923500c419..f9bd77a500 100644 --- a/tests/lean/run/grind_offset_model.lean +++ b/tests/lean/run/grind_offset_model.lean @@ -5,54 +5,54 @@ set_option grind.debug.proofs true set_option trace.grind.offset.model true /-- -info: [grind.offset.model] i := 1 +trace: [grind.offset.model] i := 1 [grind.offset.model] j := 0 [grind.offset.model] 「0」 := 0 [grind.offset.model] 「i + 1」 := 2 -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (i j : Nat) (h : i + 1 > j + 1) : g (i+1) j = i + 1 := by fail_if_success grind sorry /-- -info: [grind.offset.model] i := 101 +trace: [grind.offset.model] i := 101 [grind.offset.model] 「0」 := 0 -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (i : Nat) : i ≤ 100 := by fail_if_success grind sorry /-- -info: [grind.offset.model] i := 99 +trace: [grind.offset.model] i := 99 [grind.offset.model] 「0」 := 0 -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (i : Nat) : 100 ≤ i := by fail_if_success grind sorry /-- -info: [grind.offset.model] n := 0 +trace: [grind.offset.model] n := 0 [grind.offset.model] j := 0 [grind.offset.model] i := 99 [grind.offset.model] 「0」 := 0 [grind.offset.model] 「n + 1」 := 1 -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (i : Nat) : g (n + 1) m = a → 100 + j ≤ i := by fail_if_success grind sorry /-- -info: [grind.offset.model] n := 0 +trace: [grind.offset.model] n := 0 [grind.offset.model] j := 101 [grind.offset.model] i := 0 [grind.offset.model] 「0」 := 0 [grind.offset.model] 「n + 1」 := 1 -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (i : Nat) : g (n + 1) m = a → j ≤ i + 100 := by fail_if_success grind sorry diff --git a/tests/lean/run/grind_pattern1.lean b/tests/lean/run/grind_pattern1.lean index 3f51edf302..3f3ba3efbe 100644 --- a/tests/lean/run/grind_pattern1.lean +++ b/tests/lean/run/grind_pattern1.lean @@ -1,20 +1,20 @@ set_option trace.grind.ematch.pattern true /-- -info: [grind.ematch.pattern] Array.getElem_push_lt: [@getElem (Array #4) `[Nat] _ _ _ (@Array.push _ #3 #2) #1 _] +trace: [grind.ematch.pattern] Array.getElem_push_lt: [@getElem (Array #4) `[Nat] _ _ _ (@Array.push _ #3 #2) #1 _] -/ #guard_msgs in grind_pattern Array.getElem_push_lt => (xs.push x)[i] /-- -info: [grind.ematch.pattern] List.getElem_attach: [@getElem (List (@Subtype #3 _)) `[Nat] (@Subtype _ _) _ _ (@List.attach _ #2) #1 _] +trace: [grind.ematch.pattern] List.getElem_attach: [@getElem (List (@Subtype #3 _)) `[Nat] (@Subtype _ _) _ _ (@List.attach _ #2) #1 _] -/ #guard_msgs in grind_pattern List.getElem_attach => xs.attach[i] /-- -info: [grind.ematch.pattern] List.mem_concat_self: [@Membership.mem #2 (List _) _ (@HAppend.hAppend (List _) (List _) (List _) _ #1 (@List.cons _ #0 (@List.nil _))) #0] +trace: [grind.ematch.pattern] List.mem_concat_self: [@Membership.mem #2 (List _) _ (@HAppend.hAppend (List _) (List _) (List _) _ #1 (@List.cons _ #0 (@List.nil _))) #0] -/ #guard_msgs in grind_pattern List.mem_concat_self => a ∈ xs ++ [a] @@ -32,7 +32,7 @@ the following theorem parameters cannot be instantiated: i : Nat h : i < xs.size --- -info: [grind.ematch.pattern] Array.getElem_push_lt: [@Array.push #4 #3 #2] +trace: [grind.ematch.pattern] Array.getElem_push_lt: [@Array.push #4 #3 #2] -/ #guard_msgs in grind_pattern Array.getElem_push_lt => (xs.push x) @@ -54,13 +54,13 @@ instance [Boo α β] : Boo (List α) (Array β) where theorem fEq [Foo α β] [Boo α β] (a : List α) : (f a).1 = a := rfl -/-- info: [grind.ematch.pattern] fEq: [@f (List #4) (Array #3) _ _ #0] -/ +/-- trace: [grind.ematch.pattern] fEq: [@f (List #4) (Array #3) _ _ #0] -/ #guard_msgs in grind_pattern fEq => f a theorem fEq2 [Foo α β] [Boo α β] (a : List α) (_h : a.length > 5) : (f a).1 = a := rfl -/-- info: [grind.ematch.pattern] fEq2: [@f (List #5) (Array #4) _ _ #1] -/ +/-- trace: [grind.ematch.pattern] fEq2: [@f (List #5) (Array #4) _ _ #1] -/ #guard_msgs in grind_pattern fEq2 => f a @@ -76,7 +76,7 @@ the following theorem parameters cannot be instantiated: β : Type inst✝ : Boo α β --- -info: [grind.ematch.pattern] gEq: [@g (List #3) _ _ #0] +trace: [grind.ematch.pattern] gEq: [@g (List #3) _ _ #0] -/ #guard_msgs in grind_pattern gEq => g a @@ -92,7 +92,7 @@ error: invalid pattern(s) for `hThm1` the following theorem parameters cannot be instantiated: c : Nat --- -info: [grind.ematch.pattern] hThm1: [plus #2 #3] +trace: [grind.ematch.pattern] hThm1: [plus #2 #3] -/ #guard_msgs in grind_pattern hThm1 => plus a b @@ -104,12 +104,12 @@ the following theorem parameters cannot be instantiated: b : Nat h : b > 10 --- -info: [grind.ematch.pattern] hThm1: [plus #2 #1] +trace: [grind.ematch.pattern] hThm1: [plus #2 #1] -/ #guard_msgs in grind_pattern hThm1 => plus a c -/-- info: [grind.ematch.pattern] hThm1: [plus #2 #1, plus #2 #3] -/ +/-- trace: [grind.ematch.pattern] hThm1: [plus #2 #1, plus #2 #3] -/ #guard_msgs in grind_pattern hThm1 => plus a c, plus a b diff --git a/tests/lean/run/grind_pattern2.lean b/tests/lean/run/grind_pattern2.lean index 8ff7817c7a..72eb4dbd60 100644 --- a/tests/lean/run/grind_pattern2.lean +++ b/tests/lean/run/grind_pattern2.lean @@ -16,14 +16,14 @@ grind_pattern contains_insert => contains (insertElem s a) a set_option trace.grind.ematch true set_option trace.grind.ematch.pattern true -/-- info: [grind.ematch] activated `contains_insert`, [@contains #3 (@insertElem _ #2 #1 #0) #0] -/ -#guard_msgs (info) in +/-- trace: [grind.ematch] activated `contains_insert`, [@contains #3 (@insertElem _ #2 #1 #0) #0] -/ +#guard_msgs (trace) in example [DecidableEq α] (s₁ s₂ : Set α) (a₁ a₂ : α) : s₂ = insertElem s₁ a₁ → a₁ = a₂ → contains s₂ a₂ := by grind -/-- info: [grind.ematch] activated `contains_insert`, [@contains #3 (@insertElem _ #2 #1 #0) #0] -/ -#guard_msgs (info) in +/-- trace: [grind.ematch] activated `contains_insert`, [@contains #3 (@insertElem _ #2 #1 #0) #0] -/ +#guard_msgs (trace) in example [DecidableEq α] (s₁ s₂ : Set α) (a₁ a₂ : α) : ¬ contains s₂ a₂ → s₂ = insertElem s₁ a₁ → a₁ = a₂ → False := by grind @@ -34,13 +34,13 @@ def foo (x : List Nat) (y : List Nat) := x ++ y ++ x theorem fooThm : foo x [a, b] = x ++ [a, b] ++ x := rfl -/-- info: [grind.ematch.pattern] fooThm: [foo #0 `[[a, b]]] -/ +/-- trace: [grind.ematch.pattern] fooThm: [foo #0 `[[a, b]]] -/ #guard_msgs in grind_pattern fooThm => foo x [a, b] /-- -info: [grind.internalize] foo x y +trace: [grind.internalize] foo x y [grind.internalize] [a, b] [grind.internalize] Nat [grind.internalize] a @@ -52,7 +52,7 @@ info: [grind.internalize] foo x y [grind.internalize] y [grind.internalize] z -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.internalize true in example : foo x y = z → False := by fail_if_success grind @@ -62,7 +62,7 @@ theorem arrEx [Add α] (as : Array α) (h₁ : i < as.size) (h₂ : i = j) : as[ /-- -info: [grind.ematch.pattern] arrEx: [@HAdd.hAdd #6 _ _ _ (@getElem (Array _) `[Nat] _ _ _ #2 #5 _) (@getElem (Array _) `[Nat] _ _ _ #2 #4 _)] +trace: [grind.ematch.pattern] arrEx: [@HAdd.hAdd #6 _ _ _ (@getElem (Array _) `[Nat] _ _ _ #2 #5 _) (@getElem (Array _) `[Nat] _ _ _ #2 #4 _)] -/ #guard_msgs in grind_pattern arrEx => as[i]+as[j]'(h₂▸h₁) diff --git a/tests/lean/run/grind_pattern_proj.lean b/tests/lean/run/grind_pattern_proj.lean index 96fae6ceed..d98fab52db 100644 --- a/tests/lean/run/grind_pattern_proj.lean +++ b/tests/lean/run/grind_pattern_proj.lean @@ -35,13 +35,13 @@ structure Functor (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category. set_option trace.grind.ematch.pattern true /-- -info: [grind.ematch.pattern] Functor.map_id: [@Prefunctor.map #5 _ #3 _ (@Functor.toPrefunctor _ #4 _ #2 #1) #0 #0 (@CategoryStruct.id _ _ #0)] +trace: [grind.ematch.pattern] Functor.map_id: [@Prefunctor.map #5 _ #3 _ (@Functor.toPrefunctor _ #4 _ #2 #1) #0 #0 (@CategoryStruct.id _ _ #0)] -/ #guard_msgs in grind_pattern Functor.map_id => self.map (𝟙 X) /-- -info: [grind.ematch.pattern] Functor.map_comp: [@Prefunctor.map #9 _ #7 _ (@Functor.toPrefunctor _ #8 _ #6 #5) #4 #2 (@CategoryStruct.comp _ _ #4 #3 #2 #1 #0)] +trace: [grind.ematch.pattern] Functor.map_comp: [@Prefunctor.map #9 _ #7 _ (@Functor.toPrefunctor _ #8 _ #6 #5) #4 #2 (@CategoryStruct.comp _ _ #4 #3 #2 #1 #0)] -/ #guard_msgs in grind_pattern Functor.map_comp => self.map (f ≫ g) diff --git a/tests/lean/run/grind_pre.lean b/tests/lean/run/grind_pre.lean index 418d7b55ca..58ab526ca0 100644 --- a/tests/lean/run/grind_pre.lean +++ b/tests/lean/run/grind_pre.lean @@ -79,14 +79,14 @@ end def g (i : Nat) (j : Nat) (_ : i > j := by omega) := i + j /-- -info: [grind.offset.model] i := 1 +trace: [grind.offset.model] i := 1 [grind.offset.model] j := 0 [grind.offset.model] 「0」 := 0 [grind.offset.model] 「i + j」 := 0 [grind.offset.model] 「i + 1」 := 2 [grind.offset.model] 「i + j + 1」 := 1 -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.offset.model true in example (i j : Nat) (h : i + 1 > j + 1) : g (i+1) j = f ((fun x => x) i) + f j + 1 := by fail_if_success grind @@ -173,13 +173,13 @@ example (a : α) (p q r : Prop) : (h₁ : HEq p a) → (h₂ : HEq q a) → (h grind /-- -info: [grind.issues] found congruence between +trace: [grind.issues] found congruence between g b and f a but functions have different types -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.issues true in set_option trace.grind.debug.proof false in example (f : Nat → Bool) (g : Int → Bool) (a : Nat) (b : Int) : HEq f g → HEq a b → f a = g b := by diff --git a/tests/lean/run/grind_propagate_connectives.lean b/tests/lean/run/grind_propagate_connectives.lean index c7f7178b95..87ceeaa5fd 100644 --- a/tests/lean/run/grind_propagate_connectives.lean +++ b/tests/lean/run/grind_propagate_connectives.lean @@ -18,78 +18,78 @@ set_option grind.debug true set_option grind.debug.proofs true /-- -info: [Meta.debug] true: [q, w] +trace: [Meta.debug] true: [q, w] [Meta.debug] false: [p, r] -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : (p ∨ (q ∧ ¬r ∧ w)) → ¬p → False := by grind on_failure fallback /-- -info: [Meta.debug] true: [r] +trace: [Meta.debug] true: [r] [Meta.debug] false: [p, q] -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : (p ∨ q ∨ r) → (p ∨ ¬q) → ¬p → False := by grind on_failure fallback /-- -info: [Meta.debug] true: [r] +trace: [Meta.debug] true: [r] [Meta.debug] false: [p₁, q] -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : ((p₁ ∧ p₂) ∨ q ∨ r) → (p₁ ∨ ¬q) → p₁ = False → False := by grind on_failure fallback /-- -info: [Meta.debug] true: [r] +trace: [Meta.debug] true: [r] [Meta.debug] false: [p₂, q] -/ -#guard_msgs (info) in +#guard_msgs (trace) in example : ((p₁ ∧ p₂) ∨ q ∨ r) → ((p₂ ∧ p₁) ∨ ¬q) → p₂ = False → False := by grind on_failure fallback /-- -info: [Meta.debug] true: [q, r] +trace: [Meta.debug] true: [q, r] [Meta.debug] false: [p] -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (p q r : Prop) : p ∨ (q ↔ r) → p = False → q → False := by grind on_failure fallback /-- -info: [Meta.debug] true: [r] +trace: [Meta.debug] true: [r] [Meta.debug] false: [p, s] -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (p q r : Prop) : p ∨ ¬(s ∨ (p ↔ r)) → p = False → False := by grind on_failure fallback /-- -info: [Meta.debug] true: [p] +trace: [Meta.debug] true: [p] [Meta.debug] false: [] [Meta.debug] [a, b] -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (p : Prop) (a : Vector Nat 5) (b : Vector Nat 6) : (p → HEq a b) → p → False := by grind on_failure fallback /-- -info: [Meta.debug] true: [p, q] +trace: [Meta.debug] true: [p, q] [Meta.debug] false: [r] -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (p q r : Prop) : p ∨ (q ↔ r) → q → ¬r → False := by grind on_failure fallback /-- -info: [Meta.debug] hello world +trace: [Meta.debug] hello world [Meta.debug] true: [p, q] [Meta.debug] false: [r] -/ -#guard_msgs (info) in +#guard_msgs (trace) in example (p q r : Prop) : p ∨ (q ↔ r) → ¬r → q → False := by grind on_failure do trace[Meta.debug] "hello world" diff --git a/tests/lean/run/grind_ring_1.lean b/tests/lean/run/grind_ring_1.lean index a213f6ad6a..39cd45e4d2 100644 --- a/tests/lean/run/grind_ring_1.lean +++ b/tests/lean/run/grind_ring_1.lean @@ -16,11 +16,11 @@ example (x : UInt8) : (x + 16)*(x - 16) = x^2 := by grind +ring /-- -info: [grind.ring] new ring: Int +trace: [grind.ring] new ring: Int [grind.ring] characteristic: 0 [grind.ring] NoNatZeroDivisors available: true -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.ring true in example (x : Int) : (x + 1)^2 - 1 = x^2 + 2*x := by grind +ring @@ -29,11 +29,11 @@ example (x : BitVec 8) : (x + 16)*(x - 16) = x^2 := by grind +ring /-- -info: [grind.ring] new ring: BitVec 8 +trace: [grind.ring] new ring: BitVec 8 [grind.ring] characteristic: 256 [grind.ring] NoNatZeroDivisors available: false -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.ring true in example (x : BitVec 8) : (x + 1)^2 - 1 = x^2 + 2*x := by grind +ring @@ -60,8 +60,8 @@ example [CommRing α] [IsCharP α 0] (x : α) : (x + 1)*(x - 1) = x^2 → False example [CommRing α] [IsCharP α 8] (x : α) : (x + 1)*(x - 1) = x^2 → False := by grind +ring -/-- info: [grind.ring.assert.queue] -7 * x ^ 2 + 16 * y ^ 2 + x = 0 -/ -#guard_msgs (info) in +/-- trace: [grind.ring.assert.queue] -7 * x ^ 2 + 16 * y ^ 2 + x = 0 -/ +#guard_msgs (trace) in set_option trace.grind.ring.assert.queue true in example (x y : Int) : x + 16*y^2 - 7*x^2 = 0 → False := by fail_if_success grind +ring diff --git a/tests/lean/run/grind_ring_2.lean b/tests/lean/run/grind_ring_2.lean index 75ae1fcb28..617fefb67b 100644 --- a/tests/lean/run/grind_ring_2.lean +++ b/tests/lean/run/grind_ring_2.lean @@ -73,11 +73,11 @@ example [CommRing α] (a b c : α) grind +ring /-- -info: [grind.ring.assert.basis] a + b + c + -3 = 0 +trace: [grind.ring.assert.basis] a + b + c + -3 = 0 [grind.ring.assert.basis] 2 * b ^ 2 + 2 * (b * c) + 2 * c ^ 2 + -6 * b + -6 * c + 4 = 0 [grind.ring.assert.basis] 6 * c ^ 3 + -18 * c ^ 2 + 12 * c + 4 = 0 -/ -#guard_msgs (info) in +#guard_msgs (trace) in example [CommRing α] (a b c : α) : a + b + c = 3 → a^2 + b^2 + c^2 = 5 → @@ -87,11 +87,11 @@ example [CommRing α] (a b c : α) grind +ring /-- -info: [grind.ring.assert.basis] a + b + c + -3 = 0 +trace: [grind.ring.assert.basis] a + b + c + -3 = 0 [grind.ring.assert.basis] b ^ 2 + b * c + c ^ 2 + -3 * b + -3 * c + 2 = 0 [grind.ring.assert.basis] 3 * c ^ 3 + -9 * c ^ 2 + 6 * c + 2 = 0 -/ -#guard_msgs (info) in +#guard_msgs (trace) in example [CommRing α] [NoNatZeroDivisors α] (a b c : α) : a + b + c = 3 → a^2 + b^2 + c^2 = 5 → @@ -112,8 +112,8 @@ example (a b c : BitVec 8) (f : BitVec 8 → Nat) : c = 255 → - a + b - 1 = c example (a b c : BitVec 8) (f : BitVec 8 → Nat) : c = 255 → - a + b - 1 = c → f (2*a) = f (b + a) := by grind +ring -/-- info: [grind.ring.impEq] skip: b = a, k: 2, noZeroDivisors: false -/ -#guard_msgs (info) in +/-- trace: [grind.ring.impEq] skip: b = a, k: 2, noZeroDivisors: false -/ +#guard_msgs (trace) in example (a b c : BitVec 8) (f : BitVec 8 → Nat) : 2*a = 1 → 2*b = 1 → f (a) = f (b) := by set_option trace.grind.ring.impEq true in fail_if_success grind +ring diff --git a/tests/lean/run/grind_split.lean b/tests/lean/run/grind_split.lean index a159dd95eb..56accbc822 100644 --- a/tests/lean/run/grind_split.lean +++ b/tests/lean/run/grind_split.lean @@ -6,7 +6,7 @@ example (p q : Prop) : p ∨ q → p ∨ ¬q → ¬p ∨ q → ¬p ∨ ¬q → F opaque R : Nat → Prop /-- -info: [grind] working on goal `grind` +trace: [grind] working on goal `grind` [grind.eqc] (if p then a else b) = c [grind.eqc] R a = True [grind.eqc] R b = True @@ -23,7 +23,7 @@ info: [grind] working on goal `grind` [grind.eqc] R b = R c [grind] closed `grind.2` -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind true in example (p : Prop) [Decidable p] (a b c : Nat) : (if p then a else b) = c → R a → R b → R c := by grind diff --git a/tests/lean/run/grind_t1.lean b/tests/lean/run/grind_t1.lean index 98332bb6dd..689b73963f 100644 --- a/tests/lean/run/grind_t1.lean +++ b/tests/lean/run/grind_t1.lean @@ -79,9 +79,9 @@ example (a b c : Nat) (f : Nat → Nat) : p.1 ≠ f a → p = { a := f b, c, b : grind /-- -info: [grind.debug.proj] { a := b, b := v₁, c := v₂ }.a +trace: [grind.debug.proj] { a := b, b := v₁, c := v₂ }.a -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.debug.proj true in example (a b d e : Nat) (x y z : Boo Nat) (f : Nat → Boo Nat) : (f d).1 ≠ a → f d = ⟨b, v₁, v₂⟩ → x.1 = e → y.1 = e → z.1 = e → f d = x → f d = y → f d = z → b = a → False := by grind @@ -115,30 +115,30 @@ example (foo : Nat → Nat) end dite_propagator_test /-- -info: [grind.eqc] x = 2 * a +trace: [grind.eqc] x = 2 * a [grind.eqc] y = x [grind.eqc] (y = 2 * a) = False -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.eqc true in example (a : Nat) : let x := a + a; y = x → y = a + a := by grind -zetaDelta /-- -info: [grind.eqc] x = 2 * a +trace: [grind.eqc] x = 2 * a [grind.eqc] y = x [grind.eqc] (y = 2 * a) = False -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.eqc true in example (a : Nat) : let_fun x := a + a; y = x → y = a + a := by grind -zetaDelta /-- -info: [grind.eqc] y = 2 * a +trace: [grind.eqc] y = 2 * a [grind.eqc] (y = 2 * a) = False -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.eqc true in example (a : Nat) : let_fun x := a + a; y = x → y = a + a := by grind @@ -184,7 +184,7 @@ example (α : Type) (β : Type) (a₁ a₂ : α) (b₁ b₂ : β) grind /-- -info: [grind.assert] ∀ (a : α), a ∈ b → p a +trace: [grind.assert] ∀ (a : α), a ∈ b → p a [grind.ematch.pattern] h₁: [@Membership.mem `[α] `[List α] `[List.instMembership] `[b] #1] [grind.ematch.pattern] h₁: [p #1] [grind.assert] w ∈ b @@ -193,7 +193,7 @@ info: [grind.assert] ∀ (a : α), a ∈ b → p a [grind.ematch.instance] List.length_pos_of_mem: w ∈ b → 0 < b.length [grind.assert] w ∈ b → p w -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.ematch.pattern true in set_option trace.grind.ematch.instance true in set_option trace.grind.assert true in @@ -201,7 +201,7 @@ example (b : List α) (p : α → Prop) (h₁ : ∀ a ∈ b, p a) (h₂ : ∃ a grind /-- -info: [grind.assert] ∀ (x : α), Q x → P x +trace: [grind.assert] ∀ (x : α), Q x → P x [grind.ematch.pattern] h₁: [Q #1] [grind.ematch.pattern] h₁: [P #1] [grind.assert] ∀ (x : α), R x → False = P x @@ -214,7 +214,7 @@ info: [grind.assert] ∀ (x : α), Q x → P x [grind.assert] Q a → P a [grind.assert] R a → False = P a -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.ematch.pattern true in set_option trace.grind.ematch.instance true in set_option trace.grind.assert true in @@ -379,7 +379,7 @@ example (b : Bool) : (if b then 10 else 20) = a → b = true → False := by grind -- Should not generate a trace message about canonicalization issues -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.issues true in example : (if n + 2 < m then a else b) = (if n + 1 < m then c else d) := by fail_if_success grind (splits := 0) diff --git a/tests/lean/run/grind_trace.lean b/tests/lean/run/grind_trace.lean index c3caadda37..1c4e67ccfa 100644 --- a/tests/lean/run/grind_trace.lean +++ b/tests/lean/run/grind_trace.lean @@ -1,5 +1,7 @@ reset_grind_attrs% +set_option grind.warning false + attribute [grind =] List.length_cons attribute [grind →] List.getElem?_eq_getElem attribute [grind =] List.length_replicate diff --git a/tests/lean/run/grind_usr.lean b/tests/lean/run/grind_usr.lean index e1fcf65c87..13d3b736ce 100644 --- a/tests/lean/run/grind_usr.lean +++ b/tests/lean/run/grind_usr.lean @@ -7,27 +7,27 @@ error: the modifier `usr` is only relevant in parameters for `grind only` @[grind usr] theorem fthm : f (f x) = f x := sorry -/-- info: [grind.ematch.pattern] fthm: [f #0] -/ -#guard_msgs (info) in +/-- trace: [grind.ematch.pattern] fthm: [f #0] -/ +#guard_msgs (trace) in set_option trace.grind.ematch.pattern true in example : f (f (f x)) = f x := by grind only [fthm] /-- -info: [grind.ematch.instance] fthm: f (f x) = f x +trace: [grind.ematch.instance] fthm: f (f x) = f x [grind.ematch.instance] fthm: f (f (f x)) = f (f x) [grind.ematch.instance] fthm: f (f (f (f x))) = f (f (f x)) -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.ematch.instance true in example : f (f (f x)) = f x := by grind only [fthm] /-- -info: [grind.ematch.instance] fthm: f (f x) = f x +trace: [grind.ematch.instance] fthm: f (f x) = f x [grind.ematch.instance] fthm: f (f (f x)) = f (f x) -/ -#guard_msgs (info) in +#guard_msgs (trace) in -- should not instantiate anything using pattern `f (f #0)` set_option trace.grind.ematch.instance true in example : f x = x := by @@ -53,7 +53,7 @@ grind_pattern fthm => f (f x) example : f (f (f x)) = f x := by grind only [usr fthm] -#guard_msgs (info) in +#guard_msgs (trace) in -- should not instantiate anything using pattern `f (f #0)` set_option trace.grind.ematch.instance true in example : f x = x := by @@ -61,10 +61,10 @@ example : f x = x := by sorry /-- -info: [grind.ematch.instance] fthm: f (f x) = f x +trace: [grind.ematch.instance] fthm: f (f x) = f x [grind.ematch.instance] fthm: f (f (f x)) = f (f x) -/ -#guard_msgs (info) in +#guard_msgs (trace) in set_option trace.grind.ematch.instance true in example : f x = x := by fail_if_success grind only [fthm] diff --git a/tests/lean/run/guard_msgs.lean b/tests/lean/run/guard_msgs.lean index 156e6414cf..98626c6290 100644 --- a/tests/lean/run/guard_msgs.lean +++ b/tests/lean/run/guard_msgs.lean @@ -309,3 +309,36 @@ info: Tree.branch -/ #guard_msgs in #eval Tree.build 8 3 + + +section Trace + +/-! check that guard_msgs by defaults passes trace messages -/ + +set_option trace.debug true + +/-- trace: [debug] a trace -/ +#guard_msgs(all) in +#guard_msgs(info) in +run_meta trace[debug] "a trace" + +#guard_msgs(all) in +/-- trace: [debug] a trace -/ +#guard_msgs(trace) in +run_meta trace[debug] "a trace" + +#guard_msgs(all) in +#guard_msgs(drop trace) in +run_meta trace[debug] "a trace" + +#guard_msgs(all) in +/-- trace: [debug] a trace -/ +#guard_msgs in +run_meta trace[debug] "a trace" + +#guard_msgs(all) in +/-- trace: [debug] a trace -/ +#guard_msgs in +run_meta trace[debug] "a trace" + +end Trace diff --git a/tests/lean/run/haveTactic.lean b/tests/lean/run/haveTactic.lean index 54edb02fb6..821b35d66c 100644 --- a/tests/lean/run/haveTactic.lean +++ b/tests/lean/run/haveTactic.lean @@ -13,7 +13,7 @@ has type but is expected to have type True : Prop --- -info: h : True +trace: h : True ⊢ True -/ #guard_msgs in diff --git a/tests/lean/run/induction1.lean b/tests/lean/run/induction1.lean index 46b07aad70..d898cc618f 100644 --- a/tests/lean/run/induction1.lean +++ b/tests/lean/run/induction1.lean @@ -84,7 +84,7 @@ inductive Vec (α : Type) : Nat → Type | cons : (a : α) → {n : Nat} → (as : Vec α n) → Vec α (n+1) /-- -info: case cons.cons.fst +trace: case cons.cons.fst α β : Type n : Nat a✝¹ : α @@ -129,7 +129,7 @@ theorem ex1 (n m o : Nat) : n = m + 0 → m = o → m = o := by Test of named generalization, of an expression that does not appear in the goal. -/ /-- -info: case succ +trace: case succ α : Type ys zs : List α n : Nat @@ -157,7 +157,7 @@ example {α : Type} (xs ys zs : List α) : (xs ++ ys) ++ zs = xs ++ (ys ++ zs) : Test of named generalization, of an expression that appears in the goal. -/ /-- -info: case cons +trace: case cons α : Type zs : List α w : α @@ -195,7 +195,7 @@ Test of hole for named generalization. Yields a fresh hygienic name. -/ /-- -info: case zero +trace: case zero n : Nat h✝ : n + 1 = 0 ⊢ 0 = 1 + n @@ -217,7 +217,7 @@ example (n : Nat) : n + 1 = 1 + n := by Having no `=>` clause is short for `=> ?_`. -/ /-- -info: case mk +trace: case mk p1 p2 : Nat ⊢ (p1, p2).fst = (p1, p2).fst -/ @@ -238,7 +238,7 @@ induction n with | zero => ?_ | succ n ih => ?_ ``` -/ /-- -info: case zero +trace: case zero ⊢ 0 + 1 = 1 + 0 case succ diff --git a/tests/lean/run/infoFromFailure.lean b/tests/lean/run/infoFromFailure.lean index 8ef4ae6e90..d425b4e8d3 100644 --- a/tests/lean/run/infoFromFailure.lean +++ b/tests/lean/run/infoFromFailure.lean @@ -14,7 +14,7 @@ set_option trace.Meta.synthInstance true /-- info: B.foo "hello" : String × String --- -info: [Meta.synthInstance] ❌️ Add String +trace: [Meta.synthInstance] ❌️ Add String [Meta.synthInstance] new goal Add String [Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toAdd] [Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toAdd to Add String @@ -29,7 +29,7 @@ info: [Meta.synthInstance] ❌️ Add String #check foo "hello" /-- -info: [Meta.synthInstance] ❌️ Add Bool +trace: [Meta.synthInstance] ❌️ Add Bool [Meta.synthInstance] new goal Add Bool [Meta.synthInstance.instances] #[@Lean.Grind.CommRing.toAdd] [Meta.synthInstance] ✅️ apply @Lean.Grind.CommRing.toAdd to Add Bool diff --git a/tests/lean/run/issue7318.lean b/tests/lean/run/issue7318.lean index c93a087ef6..dabd95d33b 100644 --- a/tests/lean/run/issue7318.lean +++ b/tests/lean/run/issue7318.lean @@ -55,7 +55,7 @@ theorem bar_decide_4 (t : Three) : Q := by -- Check if messages from dischargers still appear /-- -info: case simp.discharger +trace: case simp.discharger ⊢ 1 + 1 = 2 -/ #guard_msgs in diff --git a/tests/lean/run/lazyListRotateUnfoldProof.lean b/tests/lean/run/lazyListRotateUnfoldProof.lean index 2a7e4d0c93..d442011811 100644 --- a/tests/lean/run/lazyListRotateUnfoldProof.lean +++ b/tests/lean/run/lazyListRotateUnfoldProof.lean @@ -42,7 +42,7 @@ def LazyList.ind {α : Type u} {motive : LazyList α → Sort v} -- Remark: Lean used well-founded recursion behind the scenes to define LazyList.ind /-- -info: case cons +trace: case cons τ : Type u_1 nil : LazyList τ R : List τ @@ -52,7 +52,7 @@ ih : ∀ (h : t.length + 1 = R.length), (rotate t R nil h).length = t.length + R ⊢ ∀ (h_1 : (LazyList.cons h t).length + 1 = R.length), (rotate (LazyList.cons h t) R nil h_1).length = (LazyList.cons h t).length + R.length --- -info: case delayed +trace: case delayed τ : Type u_1 nil : LazyList τ R : List τ diff --git a/tests/lean/run/letDeclSimp.lean b/tests/lean/run/letDeclSimp.lean index d226461323..2f545102d3 100644 --- a/tests/lean/run/letDeclSimp.lean +++ b/tests/lean/run/letDeclSimp.lean @@ -6,12 +6,12 @@ example (a : Nat) : let n := 0; n + a = a := by simp (config := { zeta := false }) [n] /-- -info: a b : Nat +trace: a b : Nat h : a = b n : Nat := 0 ⊢ n + a = b --- -info: a b : Nat +trace: a b : Nat h : a = b n : Nat := 0 ⊢ a = b diff --git a/tests/lean/run/lift_lets.lean b/tests/lean/run/lift_lets.lean index e8142a9829..00849d10b1 100644 --- a/tests/lean/run/lift_lets.lean +++ b/tests/lean/run/lift_lets.lean @@ -9,7 +9,7 @@ axiom test_sorry {α : Sort _} : α Basic test of let in expression. -/ /-- -info: ⊢ let x := 1; +trace: ⊢ let x := 1; x = 1 -/ #guard_msgs in @@ -23,7 +23,7 @@ example : (let x := 1; x) = 1 := by Merging -/ /-- -info: ⊢ let x := 1; +trace: ⊢ let x := 1; x = x -/ #guard_msgs in @@ -37,7 +37,7 @@ example : (let x := 1; x) = (let y := 1; y) := by Merging off. -/ /-- -info: ⊢ let x := 1; +trace: ⊢ let x := 1; let y := 1; x = y -/ @@ -52,7 +52,7 @@ example : (let x := 1; x) = (let y := 1; y) := by Not mergable, since they must match syntactically. -/ /-- -info: ⊢ let x := 2; +trace: ⊢ let x := 2; let y := 1 + 1; x = y -/ @@ -66,7 +66,7 @@ example : (let x := 2; x) = (let y := 1 + 1; y) := by Merging with local context. -/ /-- -info: y : Nat := 1 +trace: y : Nat := 1 ⊢ y = 1 -/ #guard_msgs in @@ -80,7 +80,7 @@ example : (let x := 1; x) = 1 := by Merging with local context, for top-level. -/ /-- -info: y : Nat := 1 +trace: y : Nat := 1 ⊢ y = 1 -/ #guard_msgs in @@ -94,7 +94,7 @@ example : let x := 1; x = 1 := by Recursive lifting -/ /-- -info: ⊢ let y := 1; +trace: ⊢ let y := 1; let x := y + 1; x + 1 = 3 -/ @@ -109,7 +109,7 @@ example : (let x := (let y := 1; y + 1); x + 1) = 3 := by Lifting under a binder, dependency. -/ /-- -info: ⊢ ∀ (n : Nat), +trace: ⊢ ∀ (n : Nat), let x := n; n = x -/ @@ -124,7 +124,7 @@ example : ∀ n : Nat, n = (let x := n; x) := by Lifting under a binder, no dependency. -/ /-- -info: ⊢ let x := 0; +trace: ⊢ let x := 0; ∀ (n : Nat), n = n + x -/ #guard_msgs in @@ -138,7 +138,7 @@ example : ∀ n : Nat, n = (let x := 0; n + x) := by Lifting `letFun` under a binder, dependency. -/ /-- -info: ⊢ ∀ (n : Nat), +trace: ⊢ ∀ (n : Nat), let_fun x := n; n = x -/ @@ -153,7 +153,7 @@ example : ∀ n : Nat, n = (have x := n; x) := by Lifting `letFun` under a binder, no dependency. -/ /-- -info: ⊢ let_fun x := 0; +trace: ⊢ let_fun x := 0; ∀ (n : Nat), n = n + x -/ #guard_msgs in @@ -167,7 +167,7 @@ example : ∀ n : Nat, n = (have x := 0; n + x) := by Recursive lifting, one of the internal lets can leave the binder. -/ /-- -info: ⊢ let y := 1; +trace: ⊢ let y := 1; (fun x => let a := x; a + y) @@ -185,7 +185,7 @@ example : (fun x => let a := x; let y := 1; a + y) 2 = 2 + 1 := by Lifting out of binder type. -/ /-- -info: ⊢ let ty := Nat; +trace: ⊢ let ty := Nat; (fun x => Nat) 2 -/ #guard_msgs in @@ -211,7 +211,7 @@ Four cases to this test, depending on whether a `have` or `let` is seen first, and whether the second is a `have` or `let`. -/ /-- -info: ⊢ ∀ (n : Nat), +trace: ⊢ ∀ (n : Nat), let_fun x := n; x = x -/ @@ -222,7 +222,7 @@ example : ∀ n : Nat, (have x := n; x) = (have x' := n; x') := by intros rfl /-- -info: ⊢ ∀ (n : Nat), +trace: ⊢ ∀ (n : Nat), let x := n; x = x -/ @@ -233,7 +233,7 @@ example : ∀ n : Nat, (let x := n; x) = (have x' := n; x') := by intros rfl /-- -info: ⊢ ∀ (n : Nat), +trace: ⊢ ∀ (n : Nat), let x := n; x = x -/ @@ -244,7 +244,7 @@ example : ∀ n : Nat, (have x := n; x) = (let x' := n; x') := by intros rfl /-- -info: ⊢ ∀ (n : Nat), +trace: ⊢ ∀ (n : Nat), let x := n; x = x -/ @@ -267,7 +267,7 @@ example : ∀ n : Nat, let x := n; let y := x; y = n := by Lifting from underneath an unliftable let is OK. -/ /-- -info: ⊢ let y := 0; +trace: ⊢ let y := 0; ∀ (n : Nat), let x := n; x + y = n @@ -294,7 +294,7 @@ example : (id : (let ty := Nat; ty) → Nat) = @id Nat := by Enable lifting from implicit arguments using `+implicit`. -/ /-- -info: ⊢ let ty := Nat; +trace: ⊢ let ty := Nat; id = id -/ #guard_msgs in @@ -307,7 +307,7 @@ example : (id : (let ty := Nat; ty) → Nat) = @id Nat := by Lifting at a local hypothesis. -/ /-- -info: y : Nat +trace: y : Nat h : let x := 1; x = y @@ -323,7 +323,7 @@ example (h : (let x := 1; x) = y) : True := by Lifting in both the type and value for local declarations. -/ /-- -info: v : let ty := Nat; +trace: v : let ty := Nat; id ty := let x := 2; id x @@ -340,7 +340,7 @@ example : True := by Merges using local context, even if the local declaration comes after. -/ /-- -info: y : Type := Nat +trace: y : Type := Nat h : y ⊢ True -/ @@ -355,7 +355,7 @@ example (h : let x := Nat; x) : True := by A test to make sure `lift_lets` works after other tactics. -/ /-- -info: y : Nat +trace: y : Nat ⊢ let x := 1; x = y → True -/ @@ -372,7 +372,7 @@ example (h : (let x := 1; x) = y) : True := by Lifting `let`s in proofs in `+proof` mode. -/ /-- -info: m : Nat +trace: m : Nat h : ∃ n, n + 1 = m x : Fin m y : Fin (h.choose + 1) @@ -397,10 +397,10 @@ Unlike `extract_lets`, the `lift_lets` conv tactic's modifications persist, since the local context remains the same. -/ /-- -info: | let x := Nat; +trace: | let x := Nat; x = Int --- -info: ⊢ let x := Nat; +trace: ⊢ let x := Nat; x = Int -/ #guard_msgs in @@ -415,10 +415,10 @@ example : (let x := Nat; x) = Int := by Merging with local context. -/ /-- -info: y : Type := Nat +trace: y : Type := Nat | y --- -info: y : Type := Nat +trace: y : Type := Nat ⊢ y = Int -/ #guard_msgs in diff --git a/tests/lean/run/meta2.lean b/tests/lean/run/meta2.lean index c2096ce305..a08fca4b01 100644 --- a/tests/lean/run/meta2.lean +++ b/tests/lean/run/meta2.lean @@ -38,7 +38,7 @@ do print "----- tst1 -----"; checkM $ isExprDefEq mvar (mkNatLit 10); pure () -/-- info: [Meta.debug] ----- tst1 ----- -/ +/-- trace: [Meta.debug] ----- tst1 ----- -/ #guard_msgs in #eval tst1 @@ -49,7 +49,7 @@ do print "----- tst2 -----"; checkM $ isExprDefEq mvar (mkNatLit 10); pure () -/-- info: [Meta.debug] ----- tst2 ----- -/ +/-- trace: [Meta.debug] ----- tst2 ----- -/ #guard_msgs in #eval tst2 @@ -66,7 +66,7 @@ do print "----- tst3 -----"; pure () /-- -info: [Meta.debug] ----- tst3 ----- +trace: [Meta.debug] ----- tst3 ----- [Meta.debug] fun x => x.add (Nat.add 10 x) -/ #guard_msgs in @@ -87,7 +87,7 @@ do print "----- tst4 -----"; pure () /-- -info: [Meta.debug] ----- tst4 ----- +trace: [Meta.debug] ----- tst4 ----- [Meta.debug] fun x => x.add (Nat.add 10 x) -/ #guard_msgs in @@ -125,7 +125,7 @@ do print "----- tst5 -----"; print y /-- -info: [Meta.debug] ----- tst5 ----- +trace: [Meta.debug] ----- tst5 ----- [Meta.debug] (1, 2).fst [Meta.debug] 1 [Meta.debug] 1 @@ -161,7 +161,7 @@ do print "----- tst6 -----"; pure () /-- -info: [Meta.debug] ----- tst6 ----- +trace: [Meta.debug] ----- tst6 ----- [Meta.debug] x + 2 [Meta.debug] 6 -/ @@ -186,7 +186,7 @@ do print "----- tst7 -----"; /-- error: check failed --- -info: [Meta.debug] ----- tst7 ----- +trace: [Meta.debug] ----- tst7 ----- -/ #guard_msgs in #eval tst7 @@ -199,7 +199,7 @@ do print "----- tst9 -----"; pure () /-- -info: [Meta.debug] ----- tst9 ----- +trace: [Meta.debug] ----- tst9 ----- [Meta.debug] true [Meta.debug] false -/ @@ -218,7 +218,7 @@ do print "----- tst10 -----"; pure () /-- -info: [Meta.debug] ----- tst10 ----- +trace: [Meta.debug] ----- tst10 ----- [Meta.debug] fun x => x.add (Nat.add 2 3) [Meta.debug] fun x => x.succ.succ.succ.succ.succ -/ @@ -243,7 +243,7 @@ do print "----- tst11 -----"; pure () /-- -info: [Meta.debug] ----- tst11 ----- +trace: [Meta.debug] ----- tst11 ----- [Meta.debug] ∀ (x : Nat), x = 0 -/ #guard_msgs in @@ -263,7 +263,7 @@ do print "----- tst12 -----"; pure () /-- -info: [Meta.debug] ----- tst12 ----- +trace: [Meta.debug] ----- tst12 ----- [Meta.debug] fun x => Eq.refl x [Meta.debug] ∀ (x : Nat), x = x [Meta.debug] true @@ -303,7 +303,7 @@ do print "----- tst14 -----"; pure () /-- -info: [Meta.debug] ----- tst14 ----- +trace: [Meta.debug] ----- tst14 ----- [Meta.debug] StateM Nat [Meta.debug] #[@StateT.instMonad] -/ @@ -318,7 +318,7 @@ do print "----- tst15 -----"; pure () /-- -info: [Meta.debug] ----- tst15 ----- +trace: [Meta.debug] ----- tst15 ----- [Meta.debug] instAddNat -/ #guard_msgs in @@ -335,7 +335,7 @@ do print "----- tst16 -----"; pure () /-- -info: [Meta.debug] ----- tst16 ----- +trace: [Meta.debug] ----- tst16 ----- [Meta.debug] ToString (Nat × Nat) [Meta.debug] instToStringProd -/ @@ -353,7 +353,7 @@ do print "----- tst17 -----"; pure () /-- -info: [Meta.debug] ----- tst17 ----- +trace: [Meta.debug] ----- tst17 ----- [Meta.debug] ToString (Bool × Nat × Nat) [Meta.debug] instToStringProd -/ @@ -368,7 +368,7 @@ do print "----- tst18 -----"; pure () /-- -info: [Meta.debug] ----- tst18 ----- +trace: [Meta.debug] ----- tst18 ----- [Meta.debug] instDecidableEqNat -/ #guard_msgs in @@ -385,7 +385,7 @@ do print "----- tst19 -----"; pure () /-- -info: [Meta.debug] ----- tst19 ----- +trace: [Meta.debug] ----- tst19 ----- [Meta.debug] StateM Nat [Meta.debug] Monad (StateM Nat) [Meta.debug] StateT.instMonad @@ -404,7 +404,7 @@ do print "----- tst20 -----"; pure () /-- -info: [Meta.debug] ----- tst20 ----- +trace: [Meta.debug] ----- tst20 ----- [Meta.debug] StateM Nat [Meta.debug] MonadState Nat (StateM Nat) [Meta.debug] instMonadStateOfMonadStateOf Nat (StateM Nat) @@ -437,7 +437,7 @@ do print "----- tst21 -----"; pure () /-- -info: [Meta.debug] ----- tst21 ----- +trace: [Meta.debug] ----- tst21 ----- [Meta.debug] congrArg (fun x => x.succ.succ) (Eq.symm (Eq.trans h₁ h₂)) [Meta.debug] z.succ.succ = x.succ.succ [Meta.debug] x.succ = x.succ @@ -458,7 +458,7 @@ do print "----- tst22 -----"; pure () /-- -info: [Meta.debug] ----- tst22 ----- +trace: [Meta.debug] ----- tst22 ----- [Meta.debug] Add.add x y [Meta.debug] Add.add y x [Meta.debug] toString x @@ -476,7 +476,7 @@ do print "----- tst23 -----"; print v.headBeta /-- -info: [Meta.debug] ----- tst23 ----- +trace: [Meta.debug] ----- tst23 ----- [Meta.debug] (fun x y => x + y) 0 1 [Meta.debug] 0 + 1 -/ @@ -493,7 +493,7 @@ checkM $ do { let b ← m1.mvarId!.isAssigned; pure (!b) }; checkM $ m3.mvarId!.isAssigned; pure () -/-- info: [Meta.debug] ----- tst26 ----- -/ +/-- trace: [Meta.debug] ----- tst26 ----- -/ #guard_msgs in #eval tst26 @@ -533,7 +533,7 @@ withLocalDeclD `z nat $ fun z => do pure () /-- -info: [Meta.debug] ----- tst28 ----- +trace: [Meta.debug] ----- tst28 ----- [Meta.debug] ∀ (z : Nat), Add.add z y = Add.add (Add.add x (Add.add x y)) (Add.add x (Add.add x y)) [Meta.debug] ∀ (z : Nat), Add.add z y = Add.add #0 #0 [Meta.debug] ∀ (z : Nat), Add.add z y = Add.add (Add.add x #0) (Add.add x #0) @@ -568,7 +568,7 @@ print (norm m); pure () /-- -info: [Meta.debug] ----- tst29 ----- +trace: [Meta.debug] ----- tst29 ----- [Meta.debug] u+1 [Meta.debug] u+1 [Meta.debug] max (max 1 (u+2)) 2 @@ -596,7 +596,7 @@ withLocalDeclD `x nat $ fun x => do pure () /-- -info: [Meta.debug] ----- tst30 ----- +trace: [Meta.debug] ----- tst30 ----- [Meta.debug] Nat.succ (?_ x) [Meta.debug] Nat.succ ?_ [Meta.debug] fun x => ?_ @@ -630,7 +630,7 @@ check r; pure () /-- -info: [Meta.debug] ----- tst32 ----- +trace: [Meta.debug] ----- tst32 ----- [Meta.debug] a.add a = a [Meta.debug] h2 ▸ h1 [Meta.debug] a.add b = a @@ -658,7 +658,7 @@ check r; pure () /-- -info: [Meta.debug] ----- tst33 ----- +trace: [Meta.debug] ----- tst33 ----- [Meta.debug] h2 ▸ h1 [Meta.debug] a.add b = a -/ @@ -675,7 +675,7 @@ withLocalDeclD `α type $ fun α => do pure () /-- -info: [Meta.debug] ----- tst34 ----- +trace: [Meta.debug] ----- tst34 ----- [Meta.debug] fun α => ?_ α → ?_ α -/ #guard_msgs in @@ -699,7 +699,7 @@ withLocalDeclD `α type $ fun α => do pure () /-- -info: [Meta.debug] ----- tst35 ----- +trace: [Meta.debug] ----- tst35 ----- [Meta.debug] fun α => ?_ α → ?_ α [Meta.debug] fun α => α → α -/ @@ -718,7 +718,7 @@ withLocalDeclD `α type $ fun α => do checkM $ approxDefEq $ isDefEq m1 (mkConst `Id [levelZero]); pure () -/-- info: [Meta.debug] ----- tst36 ----- -/ +/-- trace: [Meta.debug] ----- tst36 ----- -/ #guard_msgs in #eval tst36 @@ -735,7 +735,7 @@ withLocalDeclD `v nat $ fun v => do pure () /-- -info: [Meta.debug] ----- tst37 ----- +trace: [Meta.debug] ----- tst37 ----- [Meta.debug] ?_ v (?_ v) [Meta.debug] StateM Nat Nat -/ @@ -869,7 +869,7 @@ check t; | none => throwError "array lit expected") /-- -info: [Meta.debug] ----- tst42 ----- +trace: [Meta.debug] ----- tst42 ----- [Meta.debug] [1, 2] [Meta.debug] #[1, 2] -/ diff --git a/tests/lean/run/meta3.lean b/tests/lean/run/meta3.lean index 79d3b5b031..58d452c441 100644 --- a/tests/lean/run/meta3.lean +++ b/tests/lean/run/meta3.lean @@ -53,7 +53,7 @@ do let d : DiscrTree Nat := {}; set_option trace.Meta.debug true in set_option pp.mvars false in /-- -info: [Meta.debug] (Add.add => (node +trace: [Meta.debug] (Add.add => (node (Nat => (node (* => (node (* => (node (10 => (node #[1])) (20 => (node #[4])))) (0 => (node (10 => (node #[2])))))))))) (* => (node #[5])) diff --git a/tests/lean/run/meta4.lean b/tests/lean/run/meta4.lean index 182517ccc0..73afff443e 100644 --- a/tests/lean/run/meta4.lean +++ b/tests/lean/run/meta4.lean @@ -40,7 +40,7 @@ forallBoundedTelescope cinfo.type (some 10) $ fun xs body => do { print xs; chec pure () /-- -info: [Meta.debug] (α β : Type) → α → β → DecidableEq β +trace: [Meta.debug] (α β : Type) → α → β → DecidableEq β [Meta.debug] (β : Type) → ?α → β → DecidableEq β [Meta.debug] (b : ?β) → Decidable (?a = b) [Meta.debug] Decidable (?a = ?b) diff --git a/tests/lean/run/meta5.lean b/tests/lean/run/meta5.lean index 2e4b11edd6..28afc84145 100644 --- a/tests/lean/run/meta5.lean +++ b/tests/lean/run/meta5.lean @@ -27,7 +27,7 @@ set_option pp.mvars false set_option trace.Meta.debug true /-- -info: [Meta.debug] ?_ +trace: [Meta.debug] ?_ [Meta.debug] fun y => let x := 0; ?_ diff --git a/tests/lean/run/meta7.lean b/tests/lean/run/meta7.lean index 6e968a6a7d..21a980ea66 100644 --- a/tests/lean/run/meta7.lean +++ b/tests/lean/run/meta7.lean @@ -57,7 +57,7 @@ forallBoundedTelescope t (some 1) fun xs b => do pure () /-- -info: [Meta.debug] ----- tst2 ----- +trace: [Meta.debug] ----- tst2 ----- [Meta.debug] Nat → IO Nat [Meta.debug] IO Nat -/ @@ -79,7 +79,7 @@ forallBoundedTelescope t (some 0) fun xs b => do pure () /-- -info: [Meta.debug] ----- tst2 ----- +trace: [Meta.debug] ----- tst2 ----- [Meta.debug] IO Nat [Meta.debug] IO Nat -/ @@ -109,7 +109,7 @@ pure () set_option pp.mvars false in /-- -info: [Meta.debug] ----- tst4 ----- +trace: [Meta.debug] ----- tst4 ----- [Meta.debug] x y : Nat ⊢ Nat [Meta.debug] ?_ (Add.add 10 y) y @@ -139,7 +139,7 @@ check m; pure () /-- -info: [Meta.debug] ----- tst5 ----- +trace: [Meta.debug] ----- tst5 ----- [Meta.debug] p q : Prop h₁ : q h₂ : p = q @@ -172,7 +172,7 @@ pure () set_option pp.mvars false in /-- -info: [Meta.debug] ----- tst6 ----- +trace: [Meta.debug] ----- tst6 ----- [Meta.debug] x y : Nat ⊢ Nat [Meta.debug] ?_ (Add.add 10 y) @@ -200,7 +200,7 @@ checkM (pure $ val == expected); pure () /-- -info: [Meta.debug] ----- tst7 ----- +trace: [Meta.debug] ----- tst7 ----- [Meta.debug] Add.add x y [Meta.debug] Add.add 0 1 [Meta.debug] Add.add 0 1 @@ -221,7 +221,7 @@ def tst8 : MetaM Unit := do pure () /-- -info: [Meta.debug] ----- tst8 ----- +trace: [Meta.debug] ----- tst8 ----- [Meta.debug] match [1, 2, 3] with | [] => true | head :: tail => false @@ -237,7 +237,7 @@ def tst9 : MetaM Unit := do pure () /-- -info: [Meta.debug] ----- tst9 ----- +trace: [Meta.debug] ----- tst9 ----- [Meta.debug] [(instOfNatNat, 100)] -/ #guard_msgs in @@ -269,7 +269,7 @@ def tst11 : MetaM Unit := do checkM (isDefEq x y) pure () -/-- info: [Meta.debug] ----- tst11 ----- -/ +/-- trace: [Meta.debug] ----- tst11 ----- -/ #guard_msgs in #eval tst11 @@ -287,7 +287,7 @@ def tst12 : MetaM Unit := do pure () /-- -info: [Meta.debug] ----- tst12 ----- +trace: [Meta.debug] ----- tst12 ----- [Meta.debug] Add.add 10 y [Meta.debug] Add.add (Int.ofNat 10) (Int.ofNat y) [Meta.debug] Add.add 10 y diff --git a/tests/lean/run/multiTargetCasesInductionIssue.lean b/tests/lean/run/multiTargetCasesInductionIssue.lean index 211ccc709c..9b4dd6ba54 100644 --- a/tests/lean/run/multiTargetCasesInductionIssue.lean +++ b/tests/lean/run/multiTargetCasesInductionIssue.lean @@ -24,7 +24,7 @@ def Vec.casesOn | ⟨as, h⟩ => go n as h /-- -info: α : Type u_1 +trace: α : Type u_1 n✝ : Nat a✝ : α as✝ : Vec α n✝ @@ -43,7 +43,7 @@ example (n : Nat) (a : α) (as : Vec α n) : Vec.cons a (Vec.cons a as) = Vec.co constructor /-- -info: α : Type u_1 +trace: α : Type u_1 n✝ : Nat a✝ : α as✝ : Vec α n✝ @@ -62,7 +62,7 @@ example (n : Nat) (a : α) (as : Vec α n) : Vec.cons a (Vec.cons a as) = Vec.co constructor /-- -info: α : Type u_1 +trace: α : Type u_1 n : Nat a : α as : Vec α n diff --git a/tests/lean/run/opaqueNewCodeGen.lean b/tests/lean/run/opaqueNewCodeGen.lean index fa4b15d73f..fd46a297bb 100644 --- a/tests/lean/run/opaqueNewCodeGen.lean +++ b/tests/lean/run/opaqueNewCodeGen.lean @@ -3,7 +3,7 @@ import Lean set_option compiler.enableNew true /-- -info: [Compiler.result] size: 1 +trace: [Compiler.result] size: 1 def f x : Nat := let _x.1 := Nat.add x x; return _x.1 @@ -14,7 +14,7 @@ opaque f : Nat → Nat := fun x => Nat.add x x /-- -info: [Compiler.result] size: 0 +trace: [Compiler.result] size: 0 def g a._@.opaqueNewCodeGen._hyg.1 a._@.opaqueNewCodeGen._hyg.2 : Nat := extern -/ diff --git a/tests/lean/run/ppMVars.lean b/tests/lean/run/ppMVars.lean index 968c2be219..d57eecedda 100644 --- a/tests/lean/run/ppMVars.lean +++ b/tests/lean/run/ppMVars.lean @@ -13,8 +13,8 @@ Default values /-- info: ?a : Nat -/ #guard_msgs in #check (?a : Nat) -/-- info: ⊢ Sort ?u.1 -/ -#guard_msgs (info, drop all) in +/-- trace: ⊢ Sort ?u.1 -/ +#guard_msgs (trace, drop all) in example : (by_elab do return .sort (.mvar (.mk (.num `_uniq 1)))) := by trace_state sorry @@ -31,14 +31,14 @@ set_option pp.mvars false /-- info: ?_ : Nat -/ #guard_msgs in #check (_ : Nat) -/-- info: ⊢ Sort _ -/ -#guard_msgs (info, drop all) in +/-- trace: ⊢ Sort _ -/ +#guard_msgs (trace, drop all) in example : (by_elab do return .sort (.mvar (.mk (.num `_uniq 1)))) := by trace_state sorry -/-- info: ⊢ Type _ -/ -#guard_msgs (info, drop all) in +/-- trace: ⊢ Type _ -/ +#guard_msgs (trace, drop all) in example : Type _ := by trace_state sorry @@ -63,14 +63,14 @@ set_option pp.mvars.levels false Lean.MonadMCtx.modifyMCtx fun mctx => mctx.addExprMVarDecl mvarId .anonymous lctx {} type .natural 0 return .mvar mvarId -/-- info: ⊢ Sort _ -/ -#guard_msgs (info, drop all) in +/-- trace: ⊢ Sort _ -/ +#guard_msgs (trace, drop all) in example : (by_elab do return .sort (.mvar (.mk (.num `_uniq 1)))) := by trace_state sorry -/-- info: ⊢ Type _ -/ -#guard_msgs (info, drop all) in +/-- trace: ⊢ Type _ -/ +#guard_msgs (trace, drop all) in example : Type _ := by trace_state sorry @@ -95,14 +95,14 @@ set_option pp.mvars.anonymous false Lean.MonadMCtx.modifyMCtx fun mctx => mctx.addExprMVarDecl mvarId .anonymous lctx {} type .natural 0 return .mvar mvarId -/-- info: ⊢ Sort _ -/ -#guard_msgs (info, drop all) in +/-- trace: ⊢ Sort _ -/ +#guard_msgs (trace, drop all) in example : (by_elab do return .sort (.mvar (.mk (.num `_uniq 1)))) := by trace_state sorry -/-- info: ⊢ Type _ -/ -#guard_msgs (info, drop all) in +/-- trace: ⊢ Type _ -/ +#guard_msgs (trace, drop all) in example : Type _ := by trace_state sorry diff --git a/tests/lean/run/safeExp.lean b/tests/lean/run/safeExp.lean index ec9986fb78..8b112a2557 100644 --- a/tests/lean/run/safeExp.lean +++ b/tests/lean/run/safeExp.lean @@ -19,7 +19,7 @@ example : 2^257 = 2*2^256 := /-- warning: exponent 2008 exceeds the threshold 256, exponentiation operation was not evaluated, use `set_option exponentiation.threshold ` to set a new threshold --- -info: k : Nat +trace: k : Nat h : k = 2008 ^ 2 + 2 ^ 2008 ⊢ ((4032064 + 2 ^ 2008) ^ 2 + 2 ^ (4032064 + 2 ^ 2008)) % 10 = 6 --- @@ -34,7 +34,7 @@ example (k : Nat) (h : k = 2008^2 + 2^2008) : (k^2 + 2^k)%10 = 6 := by sorry /-- -info: k : Nat +trace: k : Nat h : k = 2008 ^ 2 + 2 ^ 2008 ⊢ ((2008 ^ 2 + 2 ^ 2008) ^ 2 + 2 ^ (2008 ^ 2 + 2 ^ 2008)) % 10 = 6 --- diff --git a/tests/lean/run/simpArithCacheIssue.lean b/tests/lean/run/simpArithCacheIssue.lean index 21f426497a..2e7037129c 100644 --- a/tests/lean/run/simpArithCacheIssue.lean +++ b/tests/lean/run/simpArithCacheIssue.lean @@ -1,5 +1,5 @@ /-- -info: x y : Nat +trace: x y : Nat h : y = 0 ⊢ id (2 * x + y) = id (2 * x) -/ diff --git a/tests/lean/run/simpDiag.lean b/tests/lean/run/simpDiag.lean index 20feb4999d..23260790fc 100644 --- a/tests/lean/run/simpDiag.lean +++ b/tests/lean/run/simpDiag.lean @@ -8,7 +8,7 @@ theorem f_eq : f (x + 1) = q (f x) := rfl axiom q_eq (x : Nat) : q x = x /-- -info: [simp] Diagnostics +trace: [simp] Diagnostics [simp] used theorems (max: 50, num: 2): [simp] f_eq ↦ 50 [simp] q_eq ↦ 50 @@ -32,7 +32,7 @@ def ack : Nat → Nat → Nat | x+1, y+1 => ack x (ack (x+1) y) /-- -info: [simp] Diagnostics +trace: [simp] Diagnostics [simp] used theorems (max: 1201, num: 3): [simp] ack.eq_3 ↦ 1201 [simp] Nat.reduceAdd (builtin simproc) ↦ 771 @@ -98,14 +98,14 @@ opaque q1 : Nat → Nat → Prop @[simp] axiom q1_ax (x : Nat) : q1 x 10 /-- -info: [simp] Diagnostics +trace: [simp] Diagnostics [simp] used theorems (max: 1, num: 1): [simp] q1_ax ↦ 1 [simp] tried theorems (max: 1, num: 1): [simp] q1_ax ↦ 1, succeeded: 1 use `set_option diagnostics.threshold ` to control threshold for reporting counters --- -info: [diag] Diagnostics +trace: [diag] Diagnostics [reduction] unfolded declarations (max: 246, num: 2): [reduction] Nat.rec ↦ 246 [reduction] OfNat.ofNat ↦ 24 diff --git a/tests/lean/run/simpStar.lean b/tests/lean/run/simpStar.lean index 669dd3988e..6e4fb52880 100644 --- a/tests/lean/run/simpStar.lean +++ b/tests/lean/run/simpStar.lean @@ -13,7 +13,7 @@ theorem ex2 (x : Nat) (h₁ : f x x = g x) (h₂ : g x = x) : f x (f x x) = x := axiom g_ax (x : Nat) : g x = 0 /-- -info: x y : Nat +trace: x y : Nat h₁ : f x x = g x h₂ : g x < 5 ⊢ g x + g x = 0 diff --git a/tests/lean/run/sorry.lean b/tests/lean/run/sorry.lean index cb4f0222f0..8d66421ab8 100644 --- a/tests/lean/run/sorry.lean +++ b/tests/lean/run/sorry.lean @@ -84,7 +84,7 @@ error: unknown identifier 'a' --- error: unknown identifier 'b' --- -info: ⊢ sorry = sorry +trace: ⊢ sorry = sorry -/ #guard_msgs in set_option autoImplicit false in @@ -98,7 +98,7 @@ error: unknown identifier 'a' --- error: unknown identifier 'b' --- -info: ⊢ sorry `«sorry:106:10» = sorry `«sorry:106:14» +trace: ⊢ sorry `«sorry:106:10» = sorry `«sorry:106:14» -/ #guard_msgs in set_option autoImplicit false in @@ -111,7 +111,7 @@ This requires `Lean.Widget.ppExprTagged` to have a pretty printing mode that doe https://github.com/leanprover/lean4/issues/6715 -/ /-- -info: n : Nat := sorry +trace: n : Nat := sorry ⊢ True --- warning: declaration uses 'sorry' diff --git a/tests/lean/run/structInst.lean b/tests/lean/run/structInst.lean index 2895fdb1a6..b78ed39369 100644 --- a/tests/lean/run/structInst.lean +++ b/tests/lean/run/structInst.lean @@ -198,7 +198,7 @@ structure Bar extends Foo where /- Rather than `(fun x => x) 0 = 0` or `{ toFun := fun x => x }.toFun 0 = 0` -/ -/-- info: ⊢ 0 = 0 -/ +/-- trace: ⊢ 0 = 0 -/ #guard_msgs in def bar : Bar where toFun x := x @@ -309,9 +309,9 @@ structure A where m : Fin n /-- -info: a +trace: a --- -info: b +trace: b -/ #guard_msgs in example : A where diff --git a/tests/lean/run/structuralMutual.lean b/tests/lean/run/structuralMutual.lean index be2f6f530e..74406a81be 100644 --- a/tests/lean/run/structuralMutual.lean +++ b/tests/lean/run/structuralMutual.lean @@ -73,7 +73,7 @@ theorem B_size_eq3 : B.empty.size = 0 := rfl -- Smart unfolding works /-- -info: a : A +trace: a : A h : (B.other a).size = 1 ⊢ a.size = 0 -/ @@ -249,7 +249,7 @@ theorem eq_true_of_not_eq_false {b : Bool} : (! b) = false → b = true := by si theorem eq_false_of_not_eq_true {b : Bool} : (! b) = true → b = false := by simp /-- -info: n : Nat +trace: n : Nat h : isOdd (n + 1) = false ⊢ isEven n = true -/ diff --git a/tests/lean/run/tactic.lean b/tests/lean/run/tactic.lean index 6ac073f7d0..56f3d4fdc8 100644 --- a/tests/lean/run/tactic.lean +++ b/tests/lean/run/tactic.lean @@ -20,6 +20,6 @@ print result set_option trace.Meta.Tactic true -/-- info: [Meta.Tactic] fun {p q} a a_1 => a -/ +/-- trace: [Meta.Tactic] fun {p q} a a_1 => a -/ #guard_msgs in #eval tst1 diff --git a/tests/lean/run/tactic_config.lean b/tests/lean/run/tactic_config.lean index 5dee17ae49..b2ce2ed7e3 100644 --- a/tests/lean/run/tactic_config.lean +++ b/tests/lean/run/tactic_config.lean @@ -151,7 +151,7 @@ error: structure 'C' does not have a field named 'x' --- info: config is { b := { toA := { x := true } } } --- -info: ⊢ True +trace: ⊢ True -/ #guard_msgs in example : True := by @@ -160,7 +160,7 @@ example : True := by trivial -- Check that when recovery mode is false, no error is reported. -/-- info: ⊢ True -/ +/-- trace: ⊢ True -/ #guard_msgs in example : True := by fail_if_success ctac -x diff --git a/tests/lean/run/trace.lean b/tests/lean/run/trace.lean index 139c7444db..421eebd47a 100644 --- a/tests/lean/run/trace.lean +++ b/tests/lean/run/trace.lean @@ -2,7 +2,7 @@ import Lean.CoreM open Lean -structure MyState := +structure MyState where (trace_state : TraceState := {}) (s : Nat := 0) @@ -60,7 +60,7 @@ info: [module] message [bughunt] at test2 ERROR --- -info: [module] message +trace: [module] message [module] hello world [bughunt] at test2 @@ -78,7 +78,7 @@ info: [module] message world [bughunt] at end of tst3 --- -info: [module] message +trace: [module] message [module] hello world [bughunt] at test2 diff --git a/tests/lean/run/traceFormat.lean b/tests/lean/run/traceFormat.lean index a809bf7662..35abf80ccf 100644 --- a/tests/lean/run/traceFormat.lean +++ b/tests/lean/run/traceFormat.lean @@ -18,7 +18,7 @@ def withNode (cls : Name) (msg : MessageData) (k : CoreM Unit) (collapsed := tru oldTraces.push { ref, msg } /-- -info: [test] top-level leaf +trace: [test] top-level leaf [test] top-level leaf [test] node with single leaf [test] leaf diff --git a/tests/lean/run/wf_preprocess.lean b/tests/lean/run/wf_preprocess.lean index c7b54bea1e..f9c34a9939 100644 --- a/tests/lean/run/wf_preprocess.lean +++ b/tests/lean/run/wf_preprocess.lean @@ -8,12 +8,12 @@ structure Tree (α : Type u) where def Tree.isLeaf (t : Tree α) := t.cs.isEmpty /-- -info: α : Type u_1 +trace: α : Type u_1 t t' : Tree α h✝ : t' ∈ t.cs ⊢ sizeOf t' < sizeOf t -/ -#guard_msgs in +#guard_msgs(trace) in def Tree.map (f : α → β) (t : Tree α) : Tree β := ⟨f t.val, t.cs.map (fun t' => t'.map f)⟩ termination_by t @@ -35,12 +35,12 @@ info: Tree.map.induct.{u_1} {α : Type u_1} (motive : Tree α → Prop) #check Tree.map.induct /-- -info: α : Type u_1 +trace: α : Type u_1 t x✝ : Tree α h✝ : x✝ ∈ t.cs ⊢ sizeOf x✝ < sizeOf t -/ -#guard_msgs in +#guard_msgs(trace) in def Tree.pruneRevAndMap (f : α → β) (t : Tree α) : Tree β := ⟨f t.val, (t.cs.filter (fun t' => not t'.isLeaf)).reverse.map (·.pruneRevAndMap f)⟩ termination_by t @@ -64,14 +64,14 @@ info: Tree.pruneRevAndMap.induct.{u_1} {α : Type u_1} (motive : Tree α → Pro #check Tree.pruneRevAndMap.induct /-- -info: α : Type u_1 +trace: α : Type u_1 v : α cs : List (Tree α) x✝ : Tree α h✝ : x✝ ∈ cs ⊢ sizeOf x✝ < sizeOf { val := v, cs := cs } -/ -#guard_msgs in +#guard_msgs(trace) in def Tree.pruneRevAndMap' (f : α → β) : Tree α → Tree β | ⟨v,cs⟩ => ⟨f v, (cs.filter (fun t' => not t'.isLeaf)).reverse.map (·.pruneRevAndMap' f)⟩ termination_by t => t @@ -125,7 +125,7 @@ structure MTree (α : Type u) where /-- warning: declaration uses 'sorry' --- -info: α : Type u_1 +trace: α : Type u_1 t : MTree α x✝¹ : List (MTree α) h✝¹ : x✝¹ ∈ t.cs @@ -156,7 +156,7 @@ info: MTree.map.induct.{u_1} {α : Type u_1} (motive : MTree α → Prop) #check MTree.map.induct /-- -info: α : Type u_1 +trace: α : Type u_1 t : MTree α css : List (MTree α) h✝¹ : css ∈ t.cs @@ -164,7 +164,7 @@ c : MTree α h✝ : c ∈ css ⊢ sizeOf c < sizeOf t -/ -#guard_msgs in +#guard_msgs(trace) in def MTree.size (t : MTree α) : Nat := Id.run do let mut s := 1 for css in t.cs do @@ -223,7 +223,7 @@ inductive Expression where /-- warning: declaration uses 'sorry' --- -info: L : List (String × Expression) +trace: L : List (String × Expression) x : String × Expression h✝ : x ∈ L ⊢ sizeOf x.snd < sizeOf (Expression.object L) @@ -264,7 +264,7 @@ inductive Expression where /-- warning: declaration uses 'sorry' --- -info: L : List (String × Expression) +trace: L : List (String × Expression) x : String × Expression h✝ : x ∈ L ⊢ sizeOf x.snd < sizeOf (Expression.object L) @@ -316,7 +316,7 @@ section Binary -- Main point of this test is to check whether `Tree.map2._unary` leaks the preprocessing /-- -info: α : Type u_1 +trace: α : Type u_1 β : Type u_2 t1 : Tree α t2 y : Tree β diff --git a/tests/lean/run/wf_preprocess_leak.lean b/tests/lean/run/wf_preprocess_leak.lean index dd6d908233..e6e5854753 100644 --- a/tests/lean/run/wf_preprocess_leak.lean +++ b/tests/lean/run/wf_preprocess_leak.lean @@ -9,7 +9,7 @@ def Tree.isLeaf (t : Tree α) := t.cs.isEmpty -- the proof state: /-- -info: α : Type +trace: α : Type n : Nat cs : List (Tree α) x✝ : @@ -19,7 +19,7 @@ x✝ : ⊢ Prod.Lex (fun a₁ a₂ => a₁ < a₂) (fun a₁ a₂ => sizeOf a₁ < sizeOf a₂) (n, { cs := List.map (fun x => x✝ ⟨n + 1, x.val⟩ ⋯) cs.attach }) (n.succ, { cs := cs }) -/ -#guard_msgs in +#guard_msgs(trace) in def Tree.revrev : (n : Nat) → (t : Tree α) → Tree α | 0, t => t | n + 1, Tree.mk cs => revrev n (Tree.mk (cs.map (·.revrev (n + 1)))) diff --git a/tests/lean/run/zetaUnused.lean b/tests/lean/run/zetaUnused.lean index f096fbe76b..cdf0dca1e6 100644 --- a/tests/lean/run/zetaUnused.lean +++ b/tests/lean/run/zetaUnused.lean @@ -1,6 +1,6 @@ /-- -info: b : Bool +trace: b : Bool ⊢ if b = true then let_fun unused := (); True @@ -13,7 +13,7 @@ example (b : Bool) : if b then have unused := (); True else False := by trace_state; sorry /-- -info: b : Bool +trace: b : Bool ⊢ b = true --- warning: declaration uses 'sorry' @@ -23,7 +23,7 @@ example (b : Bool) : if b then have unused := (); True else False := by simp; trace_state; sorry /-- -info: b : Bool +trace: b : Bool ⊢ b = true ∧ let_fun unused := (); True @@ -40,7 +40,7 @@ example (b : Bool) : if b then have unused := (); True else False := by simp (config := Lean.Meta.Simp.neutralConfig) only; trace_state; sorry /-- -info: b : Bool +trace: b : Bool ⊢ if b = true then True else False --- warning: declaration uses 'sorry' @@ -51,7 +51,7 @@ example (b : Bool) : if b then have unused := (); True else False := by /-- -info: b : Bool +trace: b : Bool ⊢ if b = true then True else False --- warning: declaration uses 'sorry' @@ -65,7 +65,7 @@ example (b : Bool) : if b then have unused := (); True else False := by -- Now they are preserved: /-- -info: case isTrue +trace: case isTrue b : Bool h✝ : b = true ⊢ let_fun unused := (); diff --git a/tests/lean/withSetOptionIn.lean b/tests/lean/withSetOptionIn.lean index 8f34667133..bc6e3a657e 100644 --- a/tests/lean/withSetOptionIn.lean +++ b/tests/lean/withSetOptionIn.lean @@ -26,7 +26,7 @@ Ensure that `#trace_debug_foo` works as expected. #trace_debug_foo /-- info: [debug] foo -/ -#guard_msgs in +#guard_msgs(trace) in set_option trace.debug true in #trace_debug_foo /-! ## Test @@ -35,5 +35,5 @@ Should trace `[debug] foo`, and not log the error "unexpected command 'in'". -/ /-- info: [debug] foo -/ -#guard_msgs in +#guard_msgs(trace) in #test set_option trace.debug true in #trace_debug_foo diff --git a/tests/lean/withSetOptionIn.lean.expected.out b/tests/lean/withSetOptionIn.lean.expected.out index e69de29bb2..36ff910b23 100644 --- a/tests/lean/withSetOptionIn.lean.expected.out +++ b/tests/lean/withSetOptionIn.lean.expected.out @@ -0,0 +1,8 @@ +[debug] foo +withSetOptionIn.lean:29:0-29:11: error: ❌️ Docstring on `#guard_msgs` does not match generated message: + +trace: [debug] foo +[debug] foo +withSetOptionIn.lean:38:0-38:11: error: ❌️ Docstring on `#guard_msgs` does not match generated message: + +trace: [debug] foo