From b2b7cc388afc7719d12a9da623a0eff0cf1fe489 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 17 Jun 2025 10:54:10 -0700 Subject: [PATCH] chore: Fix most test failures --- Test/Delate.lean | 2 +- Test/Environment.lean | 6 +++--- Test/Integration.lean | 8 ++++---- Test/Metavar.lean | 15 ++++++++------- 4 files changed, 16 insertions(+), 15 deletions(-) diff --git a/Test/Delate.lean b/Test/Delate.lean index 7c5eec3..1139f3e 100644 --- a/Test/Delate.lean +++ b/Test/Delate.lean @@ -51,7 +51,7 @@ def test_sexp_of_elab (env: Environment): IO LSpec.TestSeq := do ("λ x: Array Nat => x.data", [], "(:lambda x ((:c Array) (:c Nat)) ((:c Array.data) (:c Nat) 0))"), ("λ {α: Sort (u + 1)} => List α", [`u], "(:lambda α (:sort (+ u 1)) ((:c List) 0) :i)"), ("λ {α} => List α", [], "(:lambda α (:sort (+ (:mv _uniq.4) 1)) ((:c List) 0) :i)"), - ("(2: Nat) <= (5: Nat)", [], "((:c LE.le) (:mv _uniq.18) (:mv _uniq.19) ((:c OfNat.ofNat) (:mv _uniq.4) (:lit 2) (:mv _uniq.5)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))"), + ("(2: Nat) <= (5: Nat)", [], "((:c LE.le) (:mv _uniq.20) (:mv _uniq.21) ((:c OfNat.ofNat) (:mv _uniq.4) (:lit 2) (:mv _uniq.5)) ((:c OfNat.ofNat) (:mv _uniq.15) (:lit 5) (:mv _uniq.16)))"), ] entries.foldlM (λ suites (source, levels, target) => let termElabM := do diff --git a/Test/Environment.lean b/Test/Environment.lean index 29b2780..13afbfd 100644 --- a/Test/Environment.lean +++ b/Test/Environment.lean @@ -96,10 +96,10 @@ def test_symbol_location (env : Environment) : TestT IO Unit := do -- Extraction of source doesn't work for symbols in `Init` for some reason checkTrue "file" result.sourceUri?.isNone - checkEq "pos" (result.sourceStart?.map (·.column)) <| .some 0 - checkEq "pos" (result.sourceEnd?.map (·.column)) <| .some 88 + checkEq "sourceStart" (result.sourceStart?.map (·.column)) <| .some 0 + checkEq "sourceEnd" (result.sourceEnd?.map (·.column)) <| .some 88 let { imports, constNames, .. } ← Environment.moduleRead ⟨"Init.Data.Nat.Basic"⟩ - checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero"] + checkEq "imports" imports #["Init.SimpLemmas", "Init.Data.NeZero", "Init.Grind.Tactics"] checkTrue "constNames" $ constNames.contains "Nat.succ_add" def test_matcher (env : Environment) : TestT IO Unit := do diff --git a/Test/Integration.lean b/Test/Integration.lean index 9945185..0c8a7a5 100644 --- a/Test/Integration.lean +++ b/Test/Integration.lean @@ -101,7 +101,7 @@ example : (1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3 := by def test_tactic_timeout : Test := [ step "goal.start" ({ expr := "(1 : Nat) + (2 * 3) = 1 + (4 - 3) + (6 - 4) + 3" }: Protocol.GoalStart) - ({ stateId := 0, root := "_uniq.319" }: Protocol.GoalStartResult), + ({ stateId := 0, root := "_uniq.355" }: Protocol.GoalStartResult), -- timeout of 10 milliseconds step "options.set" ({ timeout? := .some 10 } : Protocol.OptionsSet) ({ }: Protocol.OptionsSetResult), @@ -280,9 +280,9 @@ def test_frontend_process_sorry : Test := def test_import_open : Test := let header := "import Init\nopen Nat\nuniverse u" let goal1: Protocol.Goal := { - name := "_uniq.67", + name := "_uniq.77", target := { pp? := .some "n + 1 = n.succ" }, - vars := #[{ name := "_uniq.66", userName := "n", type? := .some { pp? := .some "Nat" }}], + vars := #[{ name := "_uniq.76", userName := "n", type? := .some { pp? := .some "Nat" }}], } [ step "frontend.process" @@ -298,7 +298,7 @@ def test_import_open : Test := ], }: Protocol.FrontendProcessResult), step "goal.start" ({ expr := "∀ (n : Nat), n + 1 = Nat.succ n"} : Protocol.GoalStart) - ({ stateId := 0, root := "_uniq.65" }: Protocol.GoalStartResult), + ({ stateId := 0, root := "_uniq.75" }: Protocol.GoalStartResult), step "goal.tactic" ({ stateId := 0, tactic? := .some "intro n" }: Protocol.GoalTactic) ({ nextStateId? := .some 1, goals? := #[goal1], }: Protocol.GoalTacticResult), step "goal.tactic" ({ stateId := 1, tactic? := .some "apply add_one" }: Protocol.GoalTactic) diff --git a/Test/Metavar.lean b/Test/Metavar.lean index 8659fdf..a3b03eb 100644 --- a/Test/Metavar.lean +++ b/Test/Metavar.lean @@ -25,8 +25,8 @@ def test_instantiate_mvar: TestM Unit := do addTest $ assertUnreachable e return () let t ← Lean.Meta.inferType expr - addTest $ LSpec.check "typing" ((toString (← serializeExpressionSexp t)) = - "((:c LE.le) (:c Nat) (:c instLENat) ((:c OfNat.ofNat) (:mv _uniq.2) (:lit 2) (:mv _uniq.3)) ((:c OfNat.ofNat) (:mv _uniq.14) (:lit 5) (:mv _uniq.15)))") + checkEq "typing" (toString (← serializeExpressionSexp t)) + "((:c LE.le) (:c Nat) (:c instLENat) ((:c OfNat.ofNat) (:mv _uniq.2) (:lit 2) (:mv _uniq.3)) ((:c OfNat.ofNat) (:mv _uniq.15) (:lit 5) (:mv _uniq.16)))" return () def startProof (expr: String): TestM (Option GoalState) := do @@ -118,8 +118,9 @@ def test_m_couple_simp: TestM Unit := do let serializedState1 ← state1.serializeGoals (options := { ← read with printDependentMVars := true }) addTest $ LSpec.check "apply Nat.le_trans" (serializedState1.map (·.target.pp?) = #[.some "2 ≤ ?m", .some "?m ≤ 5", .some "Nat"]) + let n := state1.goals[2]! addTest $ LSpec.check "(metavariables)" (serializedState1.map (·.target.dependentMVars?.get!) = - #[#["_uniq.38"], #["_uniq.38"], #[]]) + #[#[toString n.name], #[toString n.name], #[]]) let state2 ← match ← state1.tacticOn (goalId := 2) (tactic := "exact 2") with | .success state _ => pure state @@ -158,10 +159,10 @@ def test_m_couple_simp: TestM Unit := do addTest $ assertUnreachable "(5 root)" return () let rootStr: String := toString (← Lean.Meta.ppExpr root) - addTest $ LSpec.check "(5 root)" (rootStr = "Nat.le_trans (of_eq_true (Init.Data.Nat.Basic._auxLemma.4 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))") + checkEq "(5 root)" rootStr "Nat.le_trans (of_eq_true (_proof_4✝ 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))" let unfoldedRoot ← unfoldAuxLemmas root - addTest $ LSpec.check "(5 root)" ((toString (← Lean.Meta.ppExpr unfoldedRoot)) = - "Nat.le_trans (of_eq_true (eq_true (Nat.le_refl 2))) (of_eq_true (eq_true_of_decide (Eq.refl true)))") + checkEq "(5 root)" (toString (← Lean.Meta.ppExpr unfoldedRoot)) + "Nat.le_trans (of_eq_true (_proof_4✝ 2)) (of_eq_true (eq_true_of_decide (Eq.refl true)))" return () def test_proposition_generation: TestM Unit := do @@ -258,7 +259,7 @@ def test_partial_continuation: TestM Unit := do -- Continuation should fail if the state does not exist: match state0.resume coupled_goals with - | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals [_uniq.40, _uniq.41, _uniq.38, _uniq.47] are not in scope") + | .error error => addTest $ LSpec.check "(continuation failure message)" (error = "Goals [_uniq.44, _uniq.45, _uniq.42, _uniq.51] are not in scope") | .ok _ => addTest $ assertUnreachable "(continuation failure)" -- Continuation should fail if some goals have not been solved match state2.continue state1 with