From 036b5381f0f1a193f1734ca9ffb608f09c7b7f0b Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Wed, 17 Apr 2024 07:14:51 -0700 Subject: [PATCH] fix: make tests be aware of new instance names (#3936) #3089 caused the stage0 update to cause a number of tests to start failing because they were using the old instance names. --- tests/lean/2220.lean.expected.out | 18 ++++++++---------- tests/lean/366.lean.expected.out | 2 +- tests/lean/decreasing_by.lean.expected.out | 10 +++++----- tests/lean/defInst.lean.expected.out | 2 +- tests/lean/issue2981.lean.expected.out | 5 +++-- tests/lean/run/PPTopDownAnalyze.lean | 2 +- tests/lean/run/simpGround1.lean | 2 +- tests/lean/unifHintAndTC.lean.expected.out | 2 +- 8 files changed, 21 insertions(+), 22 deletions(-) diff --git a/tests/lean/2220.lean.expected.out b/tests/lean/2220.lean.expected.out index 3c8fcbf4d5..5857adb753 100644 --- a/tests/lean/2220.lean.expected.out +++ b/tests/lean/2220.lean.expected.out @@ -1,18 +1,16 @@ -@HPow.hPow Int Nat Int Int.instHPowIntNat (@OfNat.ofNat Int 3 (@instOfNat 3)) - (@OfNat.ofNat Nat 2 (instOfNatNat 2)) : Int -@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAddInt) (@OfNat.ofNat Int 1 (@instOfNat 1)) - (@HPow.hPow Int Nat Int Int.instHPowIntNat (@OfNat.ofNat Int 3 (@instOfNat 3)) +@HPow.hPow Int Nat Int Int.instHPowNat (@OfNat.ofNat Int 3 (@instOfNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2)) : Int +@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1)) + (@HPow.hPow Int Nat Int Int.instHPowNat (@OfNat.ofNat Int 3 (@instOfNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int -@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAddInt) (@OfNat.ofNat Int 1 (@instOfNat 1)) - (@HPow.hPow Int Nat Int Int.instHPowIntNat (@OfNat.ofNat Int 3 (@instOfNat 3)) +@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1)) + (@HPow.hPow Int Nat Int Int.instHPowNat (@OfNat.ofNat Int 3 (@instOfNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int -@HPow.hPow Int Nat Int Int.instHPowIntNat (@OfNat.ofNat Int 3 (@instOfNat 3)) - (@OfNat.ofNat Nat 2 (instOfNatNat 2)) : Int +@HPow.hPow Int Nat Int Int.instHPowNat (@OfNat.ofNat Int 3 (@instOfNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2)) : Int 2220.lean:25:19-25:24: error: failed to synthesize instance HPow Nat Nat Int -@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAddInt) (@OfNat.ofNat Int 1 (@instOfNat 1)) +@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1)) (@HPow.hPow Nat Nat Int ?m (@OfNat.ofNat Nat 3 (instOfNatNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int 2220.lean:26:12-26:17: error: failed to synthesize instance HPow Nat Nat Int -@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAddInt) (@OfNat.ofNat Int 1 (@instOfNat 1)) +@HAdd.hAdd Int Int Int (@instHAdd Int Int.instAdd) (@OfNat.ofNat Int 1 (@instOfNat 1)) (@HPow.hPow Nat Nat Int ?m (@OfNat.ofNat Nat 3 (instOfNatNat 3)) (@OfNat.ofNat Nat 2 (instOfNatNat 2))) : Int diff --git a/tests/lean/366.lean.expected.out b/tests/lean/366.lean.expected.out index f32fe47022..4fa16391e6 100644 --- a/tests/lean/366.lean.expected.out +++ b/tests/lean/366.lean.expected.out @@ -1,6 +1,6 @@ [Meta.synthInstance] ✅ Inhabited Nat [Meta.synthInstance] new goal Inhabited Nat - [Meta.synthInstance.instances] #[@instInhabited, instInhabitedNat] + [Meta.synthInstance.instances] #[@instInhabitedOfMonad, instInhabitedNat] [Meta.synthInstance] ✅ apply instInhabitedNat to Inhabited Nat [Meta.synthInstance.tryResolve] ✅ Inhabited Nat ≟ Inhabited Nat [Meta.synthInstance] result instInhabitedNat diff --git a/tests/lean/decreasing_by.lean.expected.out b/tests/lean/decreasing_by.lean.expected.out index 0393f37556..9a05a03756 100644 --- a/tests/lean/decreasing_by.lean.expected.out +++ b/tests/lean/decreasing_by.lean.expected.out @@ -15,17 +15,17 @@ Please use `termination_by` to specify a decreasing measure. decreasing_by.lean:81:13-83:3: error: unexpected token 'end'; expected '{' or tactic decreasing_by.lean:81:0-81:13: error: unsolved goals n m : Nat -⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1 ⟨n, dec2 m⟩ ⟨n, m⟩ +⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelation).1 ⟨n, dec2 m⟩ ⟨n, m⟩ n m : Nat -⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1 ⟨dec1 n, 100⟩ ⟨n, m⟩ +⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelation).1 ⟨dec1 n, 100⟩ ⟨n, m⟩ decreasing_by.lean:91:0-91:22: error: unsolved goals case a n m : Nat -⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1 ⟨n, dec2 m⟩ ⟨n, m⟩ +⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelation).1 ⟨n, dec2 m⟩ ⟨n, m⟩ n m : Nat -⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1 ⟨dec1 n, 100⟩ ⟨n, m⟩ +⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelation).1 ⟨dec1 n, 100⟩ ⟨n, m⟩ decreasing_by.lean:99:0-100:22: error: Could not find a decreasing measure. The arguments relate at each recursive call as follows: (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) @@ -35,7 +35,7 @@ The arguments relate at each recursive call as follows: Please use `termination_by` to specify a decreasing measure. decreasing_by.lean:110:0-113:17: error: unsolved goals n m : Nat -⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelationProd).1 ⟨dec1 n, 100⟩ ⟨n, m⟩ +⊢ (invImage (fun x => PSigma.casesOn x fun n m => (n, m)) Prod.instWellFoundedRelation).1 ⟨dec1 n, 100⟩ ⟨n, m⟩ decreasing_by.lean:121:0-125:17: error: Could not find a decreasing measure. The arguments relate at each recursive call as follows: (<, ≤, =: relation proved, ? all proofs failed, _: no proof attempted) diff --git a/tests/lean/defInst.lean.expected.out b/tests/lean/defInst.lean.expected.out index 126cd16e2c..5a744d0f9e 100644 --- a/tests/lean/defInst.lean.expected.out +++ b/tests/lean/defInst.lean.expected.out @@ -9,4 +9,4 @@ false true true def instMMonad : Monad M := -ReaderT.instMonadReaderT +ReaderT.instMonad diff --git a/tests/lean/issue2981.lean.expected.out b/tests/lean/issue2981.lean.expected.out index 14d97db298..3ed6459f95 100644 --- a/tests/lean/issue2981.lean.expected.out +++ b/tests/lean/issue2981.lean.expected.out @@ -3,9 +3,10 @@ Tactic is run (ideally only twice) Tactic is run (ideally only twice) Tactic is run (ideally only once, in most general context) n : Nat -⊢ (invImage (fun x => x) instWellFoundedRelation).1 n n.succ +⊢ (invImage (fun x => x) instWellFoundedRelationOfSizeOf).1 n n.succ Tactic is run (ideally only twice, in most general context) Tactic is run (ideally only twice, in most general context) n : Nat ⊢ sizeOf n < sizeOf n.succ -n m : Nat ⊢ (invImage (fun x => PSigma.casesOn x fun a a_1 => a) instWellFoundedRelation).1 ⟨n, m + 1⟩ ⟨n.succ, m⟩ +n m : Nat +⊢ (invImage (fun x => PSigma.casesOn x fun a a_1 => a) instWellFoundedRelationOfSizeOf).1 ⟨n, m + 1⟩ ⟨n.succ, m⟩ diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean index 34294fa9ca..42e166ca08 100644 --- a/tests/lean/run/PPTopDownAnalyze.lean +++ b/tests/lean/run/PPTopDownAnalyze.lean @@ -344,7 +344,7 @@ set_option pp.analyze.trustSubtypeMk true in #testDelabN Lean.Xml.parse #testDelabN Add.noConfusionType #testDelabN List.filterMapM.loop -#testDelabN instMonadReaderOf +#testDelabN instMonadReaderOfOfMonadLift #testDelabN instInhabitedPUnit #testDelabN Lean.Syntax.getOptionalIdent? #testDelabN Lean.Meta.ppExpr diff --git a/tests/lean/run/simpGround1.lean b/tests/lean/run/simpGround1.lean index a95e274a3c..2cafea7414 100644 --- a/tests/lean/run/simpGround1.lean +++ b/tests/lean/run/simpGround1.lean @@ -43,7 +43,7 @@ example (h : xs = [6, 7, 8]) : f4 [1, 2, 3] 5 = xs := by simp (config := { ground := true }) rw [h] -#check List.instAppendList +#check List.instAppend example (h : xs = [4, 3, 2]) : ([1, 2, 3].map (· + 1) |>.reverse) = xs := by simp (config := { ground := true }) diff --git a/tests/lean/unifHintAndTC.lean.expected.out b/tests/lean/unifHintAndTC.lean.expected.out index d52e94aefb..de5b4ff4b5 100644 --- a/tests/lean/unifHintAndTC.lean.expected.out +++ b/tests/lean/unifHintAndTC.lean.expected.out @@ -1,4 +1,4 @@ (100, 400) (49, 576, 576) def g : Int → Int → Int := -fun (x y : Int) => @mul.{0} (@magmaOfMul.{0} Int Int.instMulInt) x y +fun (x y : Int) => @mul.{0} (@magmaOfMul.{0} Int Int.instMul) x y