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)

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

Test/Common.lean

@@ -128,8 +128,17 @@ abbrev TestT := StateT LSpec.TestSeq
 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) :=
+  t.run LSpec.TestSeq.done
 
 def runTestTermElabM (env: Environment) (t: TestT Elab.TermElabM Unit):
   IO LSpec.TestSeq :=

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),

Test/Serial.lean

@@ -0,0 +1,87 @@
+import LSpec
+import Test.Common
+import Lean
+import Pantograph.Library
+
+open Lean
+
+namespace Pantograph.Test.Serial
+
+def tempPath : IO System.FilePath := do
+  Prod.snd <$> IO.FS.createTempFile
+
+structure MultiState where
+  coreContext : Core.Context
+  env: Environment
+
+abbrev TestM := TestT $ StateRefT MultiState $ IO
+
+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 e => do
+    throw $ .userError $ ← e.toMessageData.toString
+  | .ok ((a, tests), state') => do
+    set $ (← getThe LSpec.TestSeq) ++ tests
+    return (a, state')
+
+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
+  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 #[],
+    env,
+  }
+  match ← ((runTest $ test.routine).run' state).toBaseIO with
+  | .ok 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 := "environment_pickling", nInstances := 2, routine := test_environment_pickling },
+  ]
+  tests.map (fun test => (test.name, test.run env))
+
+end Pantograph.Test.Serial