From 1b2a2d5c8d1589de58ccf551788c1b5b40346bc2 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 20 Jun 2025 10:19:42 -0700 Subject: [PATCH 1/5] test: Intentionally generate aux lemmas --- Test/Common.lean | 16 ++++++++++++++-- Test/Serial.lean | 39 ++++++++++++++++++++++++++++++--------- 2 files changed, 44 insertions(+), 11 deletions(-) diff --git a/Test/Common.lean b/Test/Common.lean index 5c288f7..397caf6 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -96,12 +96,14 @@ def runCoreMSeq (env: Environment) (coreM: CoreM LSpec.TestSeq) (options: Array | .ok a => return a def runMetaMSeq (env: Environment) (metaM: MetaM LSpec.TestSeq): IO LSpec.TestSeq := runCoreMSeq env metaM.run' -def runTermElabMInMeta { α } (termElabM: Lean.Elab.TermElabM α): Lean.MetaM α := +def runTermElabMInMeta { α } (termElabM: Elab.TermElabM α): MetaM α := termElabM.run' (ctx := defaultElabContext) +def runTermElabMInCore { α } (termElabM: Elab.TermElabM α): CoreM α := + (runTermElabMInMeta termElabM).run' def runTermElabMSeq (env: Environment) (termElabM: Elab.TermElabM LSpec.TestSeq): IO LSpec.TestSeq := runMetaMSeq env $ termElabM.run' (ctx := defaultElabContext) -def exprToStr (e: Expr): Lean.MetaM String := toString <$> Meta.ppExpr e +def exprToStr (e: Expr): MetaM String := toString <$> Meta.ppExpr e def strToTermSyntax (s: String): CoreM Syntax := do let .ok stx := Parser.runParserCategory @@ -159,6 +161,16 @@ end Monadic def runTestTermElabM (env: Environment) (t: TestT Elab.TermElabM Unit): IO LSpec.TestSeq := runTermElabMSeq env $ runTest t +def transformTestT { α } { μ μ' : Type → Type } + [Monad μ] [Monad μ'] [MonadLiftT (ST IO.RealWorld) μ] [MonadLiftT (ST IO.RealWorld) μ'] + (tr : {β : Type} → μ β → μ' β) (m : TestT μ α) : TestT μ' α := do + let tests ← get + let (a, tests) ← tr (β := α × LSpec.TestSeq) (m.run tests) + set tests + return a + + + def cdeclOf (userName: Name) (type: Expr): Condensed.LocalDecl := { userName, type } diff --git a/Test/Serial.lean b/Test/Serial.lean index c86343d..9fb8601 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -27,7 +27,7 @@ def runCoreM { α } (state : Core.State) (testCoreM : TestT CoreM α) : TestM ( set $ (← getThe LSpec.TestSeq) ++ tests return (a, state') -def test_environment_pickling : TestM Unit := do +def test_pickling_environment : TestM Unit := do let coreSrc : Core.State := { env := ← getEnv } let coreDst : Core.State := { env := ← getEnv } @@ -36,13 +36,13 @@ def test_environment_pickling : TestM Unit := do let ((), _) ← runCoreM coreSrc do let type: Expr := .forallE `p (.sort 0) (.forallE `h (.bvar 0) (.bvar 1) .default) .default let value: Expr := .lam `p (.sort 0) (.lam `h (.bvar 0) (.bvar 0) .default) .default - let c := Lean.Declaration.defnDecl <| Lean.mkDefinitionValEx + let c := Declaration.defnDecl <| mkDefinitionValEx (name := name) (levelParams := []) (type := type) (value := value) - (hints := Lean.mkReducibilityHintsRegularEx 1) - (safety := Lean.DefinitionSafety.safe) + (hints := mkReducibilityHintsRegularEx 1) + (safety := .safe) (all := []) addDecl c environmentPickle (← getEnv) envPicklePath @@ -53,7 +53,7 @@ def test_environment_pickling : TestM Unit := do let anotherName := `mystery2 checkTrue s!"Doesn't have symbol {anotherName}" (env'.find? anotherName).isNone -def test_goal_state_pickling_simple : TestM Unit := do +def test_goal_state_simple : TestM Unit := do let coreSrc : Core.State := { env := ← getEnv } let coreDst : Core.State := { env := ← getEnv } IO.FS.withTempFile λ _ statePath => do @@ -72,11 +72,31 @@ def test_goal_state_pickling_simple : TestM Unit := do let types ← metaM.run' checkTrue "Goals" $ types[0]!.equal type +def test_pickling_env_extensions : TestM Unit := do + let coreSrc : Core.State := { env := ← getEnv } + let ((), _) ← runCoreM coreSrc $ transformTestT runTermElabMInCore do + let .ok e ← elabTerm (← `(term|2 ≤ 5)) .none | unreachable! + let state ← GoalState.create e + let .success state _ ← state.tacticOn' 0 (← `(tactic|apply Nat.le_trans)) | unreachable! + let .success state' _ ← state.tacticOn' 2 (← `(tactic|exact 3)) | unreachable! + let state := state'.immediateResume state + let .success state1 _ ← state.tacticOn' 1 (← `(tactic|simp)) | unreachable! + let parentExpr := state1.parentExpr?.get! + IO.println s!"{parentExpr}" + checkTrue "has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma + + let state1 := state1.immediateResume state + let .success stateT _ ← state.tacticOn' 0 (← `(tactic|simp)) | unreachable! + let rootExpr:= stateT.rootExpr?.get! + IO.println s!"root is {rootExpr}" + checkTrue "has aux lemma" $ rootExpr.getUsedConstants.any λ name => name.isAuxLemma + return () + structure Test where name : String routine: TestM Unit -protected def Test.run (test: Test) (env: Lean.Environment) : IO LSpec.TestSeq := do +protected def Test.run (test: Test) (env: Environment) : IO LSpec.TestSeq := do -- Create the state let state : MultiState := { coreContext := ← createCoreContext #[], @@ -87,10 +107,11 @@ protected def Test.run (test: Test) (env: Lean.Environment) : IO LSpec.TestSeq : | .error e => return LSpec.check s!"Emitted exception: {e.toString}" (e.toString == "") -def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) := +def suite (env : Environment): List (String × IO LSpec.TestSeq) := let tests: List Test := [ - { name := "environment_pickling", routine := test_environment_pickling, }, - { name := "goal_state_pickling_simple", routine := test_goal_state_pickling_simple, }, + { name := "environment", routine := test_pickling_environment, }, + { name := "goal simple", routine := test_goal_state_simple, }, + { name := "extensions", routine := test_pickling_env_extensions, }, ] tests.map (fun test => (test.name, test.run env)) -- 2.44.1 From 771f8ad266760dc355842bf90e777ce7f999c38d Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 20 Jun 2025 10:20:33 -0700 Subject: [PATCH 2/5] chore: Formatting --- Test/Common.lean | 3 --- 1 file changed, 3 deletions(-) diff --git a/Test/Common.lean b/Test/Common.lean index 397caf6..8bea339 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -169,9 +169,6 @@ def transformTestT { α } { μ μ' : Type → Type } set tests return a - - - def cdeclOf (userName: Name) (type: Expr): Condensed.LocalDecl := { userName, type } -- 2.44.1 From 9d9f5dee884f3442247e7dbb03384191fc8efd88 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 20 Jun 2025 12:00:25 -0700 Subject: [PATCH 3/5] test: Use synthetic tactic to generate aux lemmas --- Test/Common.lean | 20 ++++++++++++++++++++ Test/Serial.lean | 25 ++++++++++++------------- 2 files changed, 32 insertions(+), 13 deletions(-) diff --git a/Test/Common.lean b/Test/Common.lean index 8bea339..34ce07b 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -183,6 +183,26 @@ def buildGoal (nameType: List (String × String)) (target: String) (userName?: O })).toArray } +namespace Tactic + +/-- Create an aux lemma and assigns it to `mvarId`, which is circuitous, but +exercises the aux lemma generator. -/ +def assignWithAuxLemma (type value : Expr) : Elab.Tactic.TacticM Unit := do + let type ← instantiateMVars type + let value ← instantiateMVars value + if type.hasExprMVar then + throwError "Type has expression mvar" + if value.hasExprMVar then + throwError "value has expression mvar" + let goal ← Elab.Tactic.getMainGoal + goal.withContext do + let name ← Meta.mkAuxLemma [] type value + unless ← Meta.isDefEq type (← goal.getType) do + throwError "Type provided is incorrect" + goal.assign (.const name []) + +end Tactic + end Test end Pantograph diff --git a/Test/Serial.lean b/Test/Serial.lean index 9fb8601..b37cc95 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -74,22 +74,21 @@ def test_goal_state_simple : TestM Unit := do def test_pickling_env_extensions : TestM Unit := do let coreSrc : Core.State := { env := ← getEnv } + let p := mkIdent `p + let h := mkIdent `h let ((), _) ← runCoreM coreSrc $ transformTestT runTermElabMInCore do - let .ok e ← elabTerm (← `(term|2 ≤ 5)) .none | unreachable! + let .ok e ← elabTerm (← `(term|(2: Nat) ≤ 3 ∧ (3: Nat) ≤ 5)) .none | unreachable! let state ← GoalState.create e - let .success state _ ← state.tacticOn' 0 (← `(tactic|apply Nat.le_trans)) | unreachable! - let .success state' _ ← state.tacticOn' 2 (← `(tactic|exact 3)) | unreachable! - let state := state'.immediateResume state - let .success state1 _ ← state.tacticOn' 1 (← `(tactic|simp)) | unreachable! - let parentExpr := state1.parentExpr?.get! - IO.println s!"{parentExpr}" - checkTrue "has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma + let .success state _ ← state.tacticOn' 0 (← `(tactic|apply And.intro)) | unreachable! - let state1 := state1.immediateResume state - let .success stateT _ ← state.tacticOn' 0 (← `(tactic|simp)) | unreachable! - let rootExpr:= stateT.rootExpr?.get! - IO.println s!"root is {rootExpr}" - checkTrue "has aux lemma" $ rootExpr.getUsedConstants.any λ name => name.isAuxLemma + let goal := state.goals[0]! + let (type, value) ← goal.withContext do + let .ok type ← elabTerm (← `(term|(2: Nat) ≤ 3)) (.some $ .sort 0) | unreachable! + let .ok value ← elabTerm (← `(term|sorry)) (.some type) | unreachable! + pure (type, value) + let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type value) | unreachable! + let parentExpr := state1.parentExpr?.get! + checkTrue "has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma return () structure Test where -- 2.44.1 From dfa491a5c2f3869a2ae477c4743a1aa23720cce5 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 20 Jun 2025 12:10:31 -0700 Subject: [PATCH 4/5] test: Pickling of aux lemma --- Test/Serial.lean | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/Test/Serial.lean b/Test/Serial.lean index b37cc95..55170dc 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -74,8 +74,8 @@ def test_goal_state_simple : TestM Unit := do def test_pickling_env_extensions : TestM Unit := do let coreSrc : Core.State := { env := ← getEnv } - let p := mkIdent `p - let h := mkIdent `h + let coreDst : Core.State := { env := ← getEnv } + IO.FS.withTempFile λ _ statePath => do let ((), _) ← runCoreM coreSrc $ transformTestT runTermElabMInCore do let .ok e ← elabTerm (← `(term|(2: Nat) ≤ 3 ∧ (3: Nat) ≤ 5)) .none | unreachable! let state ← GoalState.create e @@ -88,7 +88,13 @@ def test_pickling_env_extensions : TestM Unit := do pure (type, value) let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type value) | unreachable! let parentExpr := state1.parentExpr?.get! - checkTrue "has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma + checkTrue "src has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma + goalStatePickle state statePath + let ((), _) ← runCoreM coreDst $ transformTestT runTermElabMInCore do + let (state1, _) ← goalStateUnpickle statePath (← getEnv) + let parentExpr := state1.parentExpr?.get! + checkTrue "dst has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma + return () structure Test where -- 2.44.1 From 6323c02f47872194efd8a8c0c2f9c8aa4ecdc7a6 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Fri, 20 Jun 2025 12:25:40 -0700 Subject: [PATCH 5/5] test: Fix pickle state name --- Test/Serial.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Test/Serial.lean b/Test/Serial.lean index 55170dc..64717b9 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -89,7 +89,7 @@ def test_pickling_env_extensions : TestM Unit := do let .success state1 _ ← state.tryTacticM goal (Tactic.assignWithAuxLemma type value) | unreachable! let parentExpr := state1.parentExpr?.get! checkTrue "src has aux lemma" $ parentExpr.getUsedConstants.any λ name => name.isAuxLemma - goalStatePickle state statePath + goalStatePickle state1 statePath let ((), _) ← runCoreM coreDst $ transformTestT runTermElabMInCore do let (state1, _) ← goalStateUnpickle statePath (← getEnv) let parentExpr := state1.parentExpr?.get! -- 2.44.1