Skip to content

Commit

Permalink
fix tests
Browse files Browse the repository at this point in the history
  • Loading branch information
@kmill
kmill committed Oct 21, 2024
1 parent 64b2f32 commit c666fbc
Show file tree
Hide file tree
Showing 9 changed files with 95 additions and 104 deletions.
4 changes: 1 addition & 3 deletions src/Lean/Meta/Check.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -78,9 +78,7 @@ partial def addPPExplicitToExposeDiff (a b : Expr) : MetaM (Expr × Expr) := do
where
visit (a b : Expr) : MetaM (Expr × Expr) := do
try
if ← isDefEq a b then
return (a, b)
else if !a.isApp || !b.isApp || a.getAppNumArgs != b.getAppNumArgs then
if !a.isApp || !b.isApp || a.getAppNumArgs != b.getAppNumArgs then
return (a, b)
else if !(← isDefEq a.getAppFn b.getAppFn) then
let (fa, fb) ← visit a.getAppFn b.getAppFn
Expand Down
8 changes: 4 additions & 4 deletions tests/lean/1018unknowMVarIssue.lean.expected.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,8 +58,8 @@ a : α
• Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
• α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
• a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
• FVarAlias a: _uniq.636 -> _uniq.312
• FVarAlias α: _uniq.635 -> _uniq.310
• FVarAlias a: _uniq.632 -> _uniq.312
• FVarAlias α: _uniq.631 -> _uniq.310
• ?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⟩
Expand All @@ -73,8 +73,8 @@ a : α
• 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.667 -> _uniq.312
• FVarAlias n: _uniq.666 -> _uniq.310
• FVarAlias a: _uniq.663 -> _uniq.312
• FVarAlias n: _uniq.662 -> _uniq.310
• n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
• [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
• n : Nat @ ⟨10, 18⟩-⟨10, 19⟩
Expand Down
2 changes: 1 addition & 1 deletion tests/lean/delabOverApp.lean.expected.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,4 +3,4 @@ f +' g : Nat → Nat
f * g : Nat → Nat
(f * g) 1 : Nat
mul f g : Nat → Nat
mul f g 1 : Nat
mul f g (@OfNat.ofNat Nat 1 (instOfNatNat 1)) : Nat
151 changes: 70 additions & 81 deletions tests/lean/interactive/Diff.lean.expected.out
View file
Original file line number Diff line number Diff line change
@@ -1,20 +1,18 @@
{ goals := #[{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", diffStatus? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0", diffStatus? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x")]),
Lean.Widget.TaggedText.text " → ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "True")]),
{ goals := #[{ type := Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0", diffStatus? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x")]),
Lean.Widget.TaggedText.text " → ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "True")],
isInserted? := some false,
isRemoved? := none,
hyps := #[{ type := Lean.Widget.TaggedText.tag
Expand All @@ -24,23 +22,21 @@
isInserted? := some true,
isRemoved? := none }] }] }

{ goals := #[{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", diffStatus? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0", diffStatus? := some "willDelete" }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x")]),
Lean.Widget.TaggedText.text " → ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "True")]),
{ goals := #[{ type := Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0", diffStatus? := some "willDelete" }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x")]),
Lean.Widget.TaggedText.text " → ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "True")],
isInserted? := some false,
isRemoved? := none,
hyps := #[{ type := Lean.Widget.TaggedText.tag
Expand All @@ -63,22 +59,19 @@
(Lean.Widget.TaggedText.text "Nat"),
Lean.Widget.TaggedText.text "), ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", diffStatus? := none }
{ subexprPos := "/1/0", diffStatus? := some "willDelete" }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/1/0", diffStatus? := some "willDelete" }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/1/0/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x")]),
Lean.Widget.TaggedText.text " → ",
{ subexprPos := "/1/0/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "True")])]),
{ subexprPos := "/1/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x")]),
Lean.Widget.TaggedText.text " → ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "True")]),
isInserted? := some false,
isRemoved? := none,
hyps := #[] }] }
Expand All @@ -100,23 +93,21 @@
names := #["x", "y"],
isInserted? := none,
isRemoved? := none },
{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", diffStatus? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0", diffStatus? := none }
(Lean.Widget.TaggedText.text "α"),
Lean.Widget.TaggedText.text " → ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", diffStatus? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/1/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1/1", diffStatus? := some "willChange" }
(Lean.Widget.TaggedText.text "y")])]),
{ type := Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0", diffStatus? := none }
(Lean.Widget.TaggedText.text "α"),
Lean.Widget.TaggedText.text " → ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", diffStatus? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/1/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1/1", diffStatus? := some "willChange" }
(Lean.Widget.TaggedText.text "y")])],
names := #["f"],
isInserted? := none,
isRemoved? := none },
Expand Down Expand Up @@ -151,23 +142,21 @@
names := #["x", "y"],
isInserted? := none,
isRemoved? := none },
{ type := Lean.Widget.TaggedText.tag
{ subexprPos := "/", diffStatus? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0", diffStatus? := none }
(Lean.Widget.TaggedText.text "α"),
Lean.Widget.TaggedText.text " → ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", diffStatus? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/1/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1/1", diffStatus? := some "wasChanged" }
(Lean.Widget.TaggedText.text "x")])]),
{ type := Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/0", diffStatus? := none }
(Lean.Widget.TaggedText.text "α"),
Lean.Widget.TaggedText.text " → ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1", diffStatus? := none }
(Lean.Widget.TaggedText.append
#[Lean.Widget.TaggedText.tag
{ subexprPos := "/1/0/1", diffStatus? := none }
(Lean.Widget.TaggedText.text "x"),
Lean.Widget.TaggedText.text " = ",
Lean.Widget.TaggedText.tag
{ subexprPos := "/1/1", diffStatus? := some "wasChanged" }
(Lean.Widget.TaggedText.text "x")])],
names := #["f"],
isInserted? := none,
isRemoved? := none },
Expand Down
18 changes: 10 additions & 8 deletions tests/lean/run/4405.lean
View file
Original file line number Diff line number Diff line change
@@ -1,31 +1,33 @@
import Lean.Elab.Command

set_option pp.mvars false

/--
error: application type mismatch
⟨Nat.lt_irrefl ↑(?m.58 n), Fin.is_lt (?m.58 n)⟩
⟨Nat.lt_irrefl ↑(?_ n), Fin.is_lt (?_ n)⟩
argument
Fin.is_lt (?m.58 n)
Fin.is_lt (?_ n)
has type
↑(?m.58 n) < ?m.57 n : Prop
↑(?_ n) < ?_ n : Prop
but is expected to have type
↑(?m.58 n) < ↑(?m.58 n) : Prop
↑(?_ n) < ↑(?_ n) : Prop
-/
#guard_msgs in
def foo := fun n => (not_and_self_iff _).mp ⟨Nat.lt_irrefl _, Fin.is_lt _⟩

/--
error: type mismatch
Fin.is_lt ?m.185
Fin.is_lt ?_
has type
↑?m.185 < ?m.184 : Prop
↑?_ < ?_ : Prop
but is expected to have type
?a < ?a : Prop
?_ < ?_ : Prop
---
error: unsolved goals
case a
⊢ Nat
this : ?a < ?a
this : ?_ < ?_
⊢ True
-/
#guard_msgs in
Expand Down
4 changes: 2 additions & 2 deletions tests/lean/run/delabProjectionApp.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -97,9 +97,9 @@ set_option pp.explicit true
#guard_msgs in #check x.val
/-- info: y.val : Nat -/
#guard_msgs in #check y.val
/-- info: (@Fin''.toFin0 5 z).val : Nat -/
/-- info: (@Fin''.toFin0 (@OfNat.ofNat Nat 5 (instOfNatNat 5)) z).val : Nat -/
#guard_msgs in #check z.val
/-- info: (@D.toA 5 d).x : Nat -/
/-- info: (@D.toA (@OfNat.ofNat Nat 5 (instOfNatNat 5)) d).x : Nat -/
#guard_msgs in #check d.x

end
Expand Down
6 changes: 4 additions & 2 deletions tests/lean/run/sorry.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -62,13 +62,15 @@ It is not completely unique though. The `sorry` did not pay attention to variabl
/-!
Showing source position when surfacing differences.
-/
-- note: the module name is `sorry` and not `lean.run.sorry` in the testing environment,
-- so this test fails in VS Code.
/--
error: type mismatch
rfl
has type
sorry = sorry `«lean.run.sorry:73:26» : Prop
sorry = sorry `«sorry:75:26» : Prop
but is expected to have type
sorry = sorry `«lean.run.sorry:73:41» : Prop
sorry = sorry `«sorry:75:41» : Prop
-/
#guard_msgs in example : (sorry : Nat) = sorry := rfl

Expand Down
4 changes: 2 additions & 2 deletions tests/lean/rwWithSynthesizeBug.lean.expected.out
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
rwWithSynthesizeBug.lean:36:18-39:15: error: unsolved goals
inst : Bar Nat := @Bar.mk Nat 0
h : @w Nat (@f Nat inst 5)
inst : Bar Nat := @Bar.mk Nat (@OfNat.ofNat Nat 0 (instOfNatNat 0))
h : @w Nat (@f Nat inst (@OfNat.ofNat Nat 5 (instOfNatNat 5)))
⊢ True
2 changes: 1 addition & 1 deletion tests/lean/shadow.lean.expected.out
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ inst✝ inst : α
shadow.lean:17:0-17:1: error: don't know how to synthesize placeholder
context:
α : Type u_1
inst.75 : Inhabited α
inst.78 : Inhabited α
inst inst : α
⊢ {β δ : Type} → α → β → δ → α × β × δ
shadow.lean:20:0-20:1: error: don't know how to synthesize placeholder
Expand Down

0 comments on commit c666fbc

Please sign in to comment.