From 29178ca4083fcbe4b9c427027cf80d321ce53c0f Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 11 Oct 2023 17:05:03 +1100 Subject: [PATCH] update README --- README.md | 28 +++++++++++++++++++++++++++- 1 file changed, 27 insertions(+), 1 deletion(-) diff --git a/README.md b/README.md index ef32b5f..05ced53 100644 --- a/README.md +++ b/README.md @@ -91,7 +91,33 @@ At present there is nothing you can do with a completed proof state: we would like to extend this so that you can replace the original `sorry` with your tactic script, and obtain the resulting `Environment` +## Pickling + +The REPL supports pickling environments and proof states to disk as `.olean` files. +As long as the same imports are available, it should be possible to move such an `.olean` file +to another machine and unpickle into a new REPL session. + +The commands are + +```json +{"pickleTo": "path/to/file.olean", "env": 7} + +{"pickleTo": "path/to/file.olean", "proofState": 17} + +{"unpickleEnvFrom": "path/to/file.olean"} + +{"unpickleProofStateFrom": "path/to/file.olean"} +``` + +The unpickling commands will report the new "env" or "proofState" identifier that +you can use in subsequent commands. + +Pickling is quite efficient: +* we don't record full `Environment`s, only the changes relative to imports +* unpickling uses memory mapping +* file sizes are generally small, but see https://github.com/digama0/leangz if compression is + desirable + ## Future work * Replay tactic scripts from tactic mode back into the original `sorry`. -* Serialization and deserialization of environments and proof states