Save Lean example contexts for later

Right now, Lean example contexts exist in an ephemeral environment extension that contains an environment. This is fine if all the examples exist in a single file, but it doesn't work well if one wants to e.g. have a blog post or book chapter that builds on another one.

Serializing the saved environment to a .olean isn't really a good idea. So I plan to add an option to save the syntax of the commands that gave rise to the environment and export them for replay while rendering the other environment.

This is not great for complex running examples (like in Functional Programming in Lean), though. For that, we need a better solution. It could look like writing the example in an examples file with named commands, as the book's text is now, but extracting them into Verso via metaprogramming rather than regexps. This needs further thought.

The issue describes saving Lean command syntax for replay across rendered environments, with a separate need for complex running examples. Read the example-context environment extension and rendering entry points to understand how contexts are currently stored and consumed. The issue says the design needs further thought; done would require a decided approach for replaying saved commands across documents.