From 49369f9c7c4fb35403abafff5aa4948f85dbc23e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 15 May 2025 09:56:26 +0200 Subject: [PATCH] chore: change chatty test to interactive test (#8348) --- .../1018unknowMVarIssue.lean.expected.out | 85 ------------------- .../1018unknowMVarIssue.lean | 8 +- .../1018unknowMVarIssue.lean.expected.out | 5 ++ 3 files changed, 11 insertions(+), 87 deletions(-) delete mode 100644 tests/lean/1018unknowMVarIssue.lean.expected.out rename tests/lean/{ => interactive}/1018unknowMVarIssue.lean (54%) create mode 100644 tests/lean/interactive/1018unknowMVarIssue.lean.expected.out diff --git a/tests/lean/1018unknowMVarIssue.lean.expected.out b/tests/lean/1018unknowMVarIssue.lean.expected.out deleted file mode 100644 index d8d4d1cf38..0000000000 --- a/tests/lean/1018unknowMVarIssue.lean.expected.out +++ /dev/null @@ -1,85 +0,0 @@ -[Elab.info] - • command @ ⟨6, 0⟩-⟨6, 31⟩ @ Lean.Elab.Command.elabSetOption - • [.] (Command.set_option "set_option" `trace.Elab.info []) @ ⟨6, 0⟩-⟨6, 26⟩ - • option trace.Elab.info @ ⟨6, 11⟩-⟨6, 26⟩ -1018unknowMVarIssue.lean:9:18-9:19: error: don't know how to synthesize placeholder -context: -α✝ β : Type -x : Fam2 α✝ β -α : Type -a : α -⊢ α -[Elab.info] - • command @ ⟨7, 0⟩-⟨10, 19⟩ @ Lean.Elab.Command.elabDeclaration - • α : Type @ ⟨7, 13⟩-⟨7, 14⟩ @ Lean.Elab.Term.elabIdent - • [.] α : some Sort.{?_uniq} @ ⟨7, 13⟩-⟨7, 14⟩ - • α : Type @ ⟨7, 13⟩-⟨7, 14⟩ - • a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩ - • Fam2 α β : Type 1 @ ⟨7, 21⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabApp - • [.] Fam2 : some Sort.{?_uniq} @ ⟨7, 21⟩-⟨7, 25⟩ - • Fam2 : Type → Type → Type 1 @ ⟨7, 21⟩-⟨7, 25⟩ - • α : Type @ ⟨7, 26⟩-⟨7, 27⟩ @ Lean.Elab.Term.elabIdent - • [.] α : some Type @ ⟨7, 26⟩-⟨7, 27⟩ - • α : Type @ ⟨7, 26⟩-⟨7, 27⟩ - • β : Type @ ⟨7, 28⟩-⟨7, 29⟩ @ Lean.Elab.Term.elabIdent - • [.] β : some Type @ ⟨7, 28⟩-⟨7, 29⟩ - • β : Type @ ⟨7, 28⟩-⟨7, 29⟩ - • x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩ - • β : Type @ ⟨7, 33⟩-⟨7, 34⟩ @ Lean.Elab.Term.elabIdent - • [.] β : some Sort.{?_uniq} @ ⟨7, 33⟩-⟨7, 34⟩ - • β : Type @ ⟨7, 33⟩-⟨7, 34⟩ - • CustomInfo(Lean.Elab.InlayHint) - • _example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩†!-⟨7, 7⟩†! - • a (isBinder := true) : α @ ⟨7, 9⟩-⟨7, 10⟩ - • x (isBinder := true) : Fam2 α β @ ⟨7, 17⟩-⟨7, 18⟩ - • CustomInfo(Lean.Elab.Term.BodyInfo) - • Partial term @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.Quotation.elabMatchSyntax - • match α, β, x, a with - | α_1, .(α_1), Fam2.any, a => ?m x α_1 a - | .(Nat), .(Nat), Fam2.nat n, a => n : β @ ⟨8, 2⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabMatch - • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent - • [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩ - • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ - • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ @ Lean.Elab.Term.elabIdent - • [.] x : none @ ⟨8, 8⟩-⟨8, 9⟩ - • x : Fam2 α β @ ⟨8, 8⟩-⟨8, 9⟩ - • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩ - • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩ - • @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩ - • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩ - • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩ - • [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩ - • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩ - • [.] Fam2.any : none @ ⟨9, 4⟩-⟨9, 12⟩ - • @Fam2.any : {α : Type} → Fam2 α α @ ⟨9, 4⟩-⟨9, 12⟩ - • [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩† - • [.] Fam2.any : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨9, 4⟩-⟨9, 12⟩ - • [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩† - • α (isBinder := true) : Type @ ⟨8, 2⟩†-⟨10, 19⟩† - • α : Type @ ⟨8, 2⟩†-⟨10, 19⟩† - • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩† - • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩† - • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩† - • FVarAlias a: _uniq.608 -> _uniq.325 - • FVarAlias α: _uniq.607 -> _uniq.323 - • ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole - • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩ - • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩ - • [.] n : none @ ⟨10, 13⟩-⟨10, 14⟩ - • [.] a : none @ ⟨8, 2⟩†-⟨10, 19⟩† - • [.] Fam2.nat : some Fam2 ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) ([mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]]) @ ⟨10, 4⟩-⟨10, 12⟩ - • [.] n : some Nat @ ⟨10, 13⟩-⟨10, 14⟩ - • [.] a : some [mdata _patWithRef: [mdata _inaccessible:1 [mdata _patWithRef: ?_uniq]]] @ ⟨8, 2⟩†-⟨10, 19⟩† - • Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† - • Nat : Type @ ⟨8, 2⟩†-⟨10, 19⟩† - • Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩ - • n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩ - • a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩† - • FVarAlias a: _uniq.639 -> _uniq.325 - • FVarAlias n: _uniq.638 -> _uniq.323 - • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent - • [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩ - • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ - • @_example (isBinder := true) : {α β : Type} → α → Fam2 α β → β @ ⟨7, 0⟩-⟨7, 7⟩ -[Elab.info] - • command @ ⟨11, 0⟩-⟨11, 0⟩ @ Lean.Elab.Command.elabEoi diff --git a/tests/lean/1018unknowMVarIssue.lean b/tests/lean/interactive/1018unknowMVarIssue.lean similarity index 54% rename from tests/lean/1018unknowMVarIssue.lean rename to tests/lean/interactive/1018unknowMVarIssue.lean index 3b36c85e1a..1494fd55fa 100644 --- a/tests/lean/1018unknowMVarIssue.lean +++ b/tests/lean/interactive/1018unknowMVarIssue.lean @@ -1,10 +1,14 @@ +/-! +The expected type used to show "unknown metavariable '?_uniq.31828'" because of missing +backtracking of the info tree. +-/ + inductive Fam2 : Type → Type → Type 1 where | any : Fam2 α α | nat : Nat → Fam2 Nat Nat -set_option pp.rawOnError true -set_option trace.Elab.info true example (a : α) (x : Fam2 α β) : β := match x with | Fam2.any => _ + --^ $/lean/plainTermGoal | Fam2.nat n => n diff --git a/tests/lean/interactive/1018unknowMVarIssue.lean.expected.out b/tests/lean/interactive/1018unknowMVarIssue.lean.expected.out new file mode 100644 index 0000000000..5a1141e7b4 --- /dev/null +++ b/tests/lean/interactive/1018unknowMVarIssue.lean.expected.out @@ -0,0 +1,5 @@ +{"textDocument": {"uri": "file:///1018unknowMVarIssue.lean"}, + "position": {"line": 11, "character": 18}} +{"range": + {"start": {"line": 11, "character": 18}, "end": {"line": 11, "character": 19}}, + "goal": "α✝ β : Type\nx : Fam2 α✝ β\nα : Type\na : α\n⊢ α"}