From 7c9b092200ffc3365060cf7e0d6d0db1c809aeb4 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 30 Nov 2024 23:21:16 -0800 Subject: [PATCH 1/2] test: Dual monad testing stub --- Test/Common.lean | 2 ++ Test/Main.lean | 4 +++- Test/Serial.lean | 56 ++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 61 insertions(+), 1 deletion(-) create mode 100644 Test/Serial.lean diff --git a/Test/Common.lean b/Test/Common.lean index 3998293..ce21ce8 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -130,6 +130,8 @@ def addTest [Monad m] (test: LSpec.TestSeq): TestT m Unit := do def runTest [Monad m] (t: TestT m Unit): m LSpec.TestSeq := Prod.snd <$> t.run LSpec.TestSeq.done +def runTestWithResult { α } [Monad m] (t: TestT m α): m (α × LSpec.TestSeq) := + t.run LSpec.TestSeq.done def runTestTermElabM (env: Environment) (t: TestT Elab.TermElabM Unit): IO LSpec.TestSeq := diff --git a/Test/Main.lean b/Test/Main.lean index 25bb0d9..6bf410e 100644 --- a/Test/Main.lean +++ b/Test/Main.lean @@ -1,11 +1,12 @@ import LSpec +import Test.Delate import Test.Environment import Test.Frontend import Test.Integration import Test.Library import Test.Metavar import Test.Proofs -import Test.Delate +import Test.Serial import Test.Tactic -- Test running infrastructure @@ -51,6 +52,7 @@ def main (args: List String) := do ("Metavar", Metavar.suite env_default), ("Proofs", Proofs.suite env_default), ("Delate", Delate.suite env_default), + ("Serial", Serial.suite env_default), ("Tactic/Congruence", Tactic.Congruence.suite env_default), ("Tactic/Motivated Apply", Tactic.MotivatedApply.suite env_default), ("Tactic/No Confuse", Tactic.NoConfuse.suite env_default), diff --git a/Test/Serial.lean b/Test/Serial.lean new file mode 100644 index 0000000..4cca464 --- /dev/null +++ b/Test/Serial.lean @@ -0,0 +1,56 @@ +import LSpec +import Test.Common +import Lean +import Pantograph.Library + +open Lean + +namespace Pantograph.Test.Serial + +structure MultiState where + coreContext : Core.Context + coreStates : Array Core.State + +abbrev TestM := StateRefT MultiState $ TestT $ EIO LSpec.TestSeq + +def runCoreM { α } (id : Nat) (testCoreM: TestT CoreM α) : TestM α := do + let multiState ← get + let state ← match multiState.coreStates[id]? with + | .some state => pure state + | .none => + let test := LSpec.test "Invalid index" (id < multiState.coreStates.size) + throw test + let coreM := runTestWithResult testCoreM + match ← (coreM.run' multiState.coreContext state).toBaseIO with + | .error _ => do + let test := LSpec.test "Exception" false + throw test + | .ok (a, tests) => do + set $ (← getThe LSpec.TestSeq) ++ tests + return a + +def simple : TestM Unit := do + return + +structure Test where + name : String + nInstances : Nat + routine: TestM Unit + +protected def Test.run (test: Test) (env: Lean.Environment) : IO LSpec.TestSeq := do + -- Create the state + let state : MultiState := { + coreContext := ← createCoreContext #[], + coreStates := Array.range test.nInstances |>.map λ _ => { env }, + } + match ← (runTest $ test.routine.run' state).toBaseIO with + | .ok e => return e + | .error e => return e + +def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) := + let tests: List Test := [ + { name := "simple", nInstances := 2, routine := simple } + ] + tests.map (fun test => (test.name, test.run env)) + +end Pantograph.Test.Serial -- 2.44.1 From 0f946880ae87a5b746b188dcc946ee8c2cbefa8b Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Wed, 4 Dec 2024 10:44:33 -0800 Subject: [PATCH 2/2] test: Environment pickling --- Pantograph/Serial.lean | 4 +-- Repl.lean | 4 +-- Test/Common.lean | 9 +++++- Test/Serial.lean | 73 ++++++++++++++++++++++++++++++------------ 4 files changed, 64 insertions(+), 26 deletions(-) diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 2f04bdb..e60fc54 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -55,7 +55,7 @@ and when unpickling, we build a fresh `Environment` from the imports, and then add the new constants. -/ @[export pantograph_env_pickle_m] -def env_pickle (env : Environment) (path : System.FilePath) : IO Unit := +def environmentPickle (env : Environment) (path : System.FilePath) : IO Unit := Pantograph.pickle path (env.header.imports, env.constants.map₂) /-- @@ -65,7 +65,7 @@ We construct a fresh `Environment` with the relevant imports, and then replace the new constants. -/ @[export pantograph_env_unpickle_m] -def env_unpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do +def environmentUnpickle (path : System.FilePath) : IO (Environment × CompactedRegion) := unsafe do let ((imports, map₂), region) ← Pantograph.unpickle (Array Import × PHashMap Name ConstantInfo) path let env ← importModules imports {} 0 return (← env.replay (Std.HashMap.ofList map₂.toList), region) diff --git a/Repl.lean b/Repl.lean index e162f05..f0572a1 100644 --- a/Repl.lean +++ b/Repl.lean @@ -90,10 +90,10 @@ def execute (command: Protocol.Command): MainM Lean.Json := do Environment.addDecl args env_save (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do let env ← Lean.MonadEnv.getEnv - env_pickle env args.path + environmentPickle env args.path return .ok {} env_load (args: Protocol.EnvSaveLoad): MainM (CR Protocol.EnvSaveLoadResult) := do - let (env, _) ← env_unpickle args.path + let (env, _) ← environmentUnpickle args.path Lean.setEnv env return .ok {} expr_echo (args: Protocol.ExprEcho): MainM (CR Protocol.ExprEchoResult) := do diff --git a/Test/Common.lean b/Test/Common.lean index ce21ce8..0a0b44c 100644 --- a/Test/Common.lean +++ b/Test/Common.lean @@ -125,9 +125,16 @@ def mvarUserNameAndType (mvarId: MVarId): MetaM (Name × String) := do abbrev TestT := StateT LSpec.TestSeq -def addTest [Monad m] (test: LSpec.TestSeq): TestT m Unit := do +def addTest [Monad m] (test: LSpec.TestSeq) : TestT m Unit := do set $ (← get) ++ test +def checkEq [Monad m] [DecidableEq α] (desc : String) (lhs rhs : α) : TestT m Unit := do + addTest $ LSpec.check desc (lhs == rhs) +def checkTrue [Monad m] (desc : String) (flag : Bool) : TestT m Unit := do + addTest $ LSpec.check desc flag +def fail [Monad m] (desc : String) : TestT m Unit := do + addTest $ LSpec.check desc false + def runTest [Monad m] (t: TestT m Unit): m LSpec.TestSeq := Prod.snd <$> t.run LSpec.TestSeq.done def runTestWithResult { α } [Monad m] (t: TestT m α): m (α × LSpec.TestSeq) := diff --git a/Test/Serial.lean b/Test/Serial.lean index 4cca464..d1ce661 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -7,30 +7,60 @@ open Lean namespace Pantograph.Test.Serial +def tempPath : IO System.FilePath := do + Prod.snd <$> IO.FS.createTempFile + structure MultiState where coreContext : Core.Context - coreStates : Array Core.State + env: Environment -abbrev TestM := StateRefT MultiState $ TestT $ EIO LSpec.TestSeq +abbrev TestM := TestT $ StateRefT MultiState $ IO -def runCoreM { α } (id : Nat) (testCoreM: TestT CoreM α) : TestM α := do - let multiState ← get - let state ← match multiState.coreStates[id]? with - | .some state => pure state - | .none => - let test := LSpec.test "Invalid index" (id < multiState.coreStates.size) - throw test +instance : MonadEnv TestM where + getEnv := return (← getThe MultiState).env + modifyEnv f := do modifyThe MultiState fun s => { s with env := f s.env } + +def runCoreM { α } (state : Core.State) (testCoreM : TestT CoreM α) : TestM (α × Core.State) := do + let multiState ← getThe MultiState let coreM := runTestWithResult testCoreM - match ← (coreM.run' multiState.coreContext state).toBaseIO with - | .error _ => do - let test := LSpec.test "Exception" false - throw test - | .ok (a, tests) => do + match ← (coreM.run multiState.coreContext state).toBaseIO with + | .error e => do + throw $ .userError $ ← e.toMessageData.toString + | .ok ((a, tests), state') => do set $ (← getThe LSpec.TestSeq) ++ tests - return a + return (a, state') -def simple : TestM Unit := do - return +def test_environment_pickling : TestM Unit := do + let stateSrc: Core.State := { env := ← getEnv } + let stateDst: Core.State := { env := ← getEnv } + + let name := `mystery + let envPicklePath ← tempPath + let ((), _) ← runCoreM stateSrc 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 + (name := name) + (levelParams := []) + (type := type) + (value := value) + (hints := Lean.mkReducibilityHintsRegularEx 1) + (safety := Lean.DefinitionSafety.safe) + (all := []) + let env' ← match (← getEnv).addDecl (← getOptions) c with + | .error e => do + let error ← (e.toMessageData (← getOptions)).toString + throwError error + | .ok env' => pure env' + environmentPickle env' envPicklePath + + let _ ← runCoreM stateDst do + let (env', _) ← environmentUnpickle envPicklePath + checkTrue s!"Has symbol {name}" (env'.find? name).isSome + let anotherName := `mystery2 + checkTrue s!"Doesn't have symbol {anotherName}" (env'.find? anotherName).isNone + + IO.FS.removeFile envPicklePath structure Test where name : String @@ -41,15 +71,16 @@ protected def Test.run (test: Test) (env: Lean.Environment) : IO LSpec.TestSeq : -- Create the state let state : MultiState := { coreContext := ← createCoreContext #[], - coreStates := Array.range test.nInstances |>.map λ _ => { env }, + env, } - match ← (runTest $ test.routine.run' state).toBaseIO with + match ← ((runTest $ test.routine).run' state).toBaseIO with | .ok e => return e - | .error e => return e + | .error e => + return LSpec.check "Emitted exception" (e.toString == "") def suite (env : Lean.Environment): List (String × IO LSpec.TestSeq) := let tests: List Test := [ - { name := "simple", nInstances := 2, routine := simple } + { name := "environment_pickling", nInstances := 2, routine := test_environment_pickling }, ] tests.map (fun test => (test.name, test.run env)) -- 2.44.1