extensible state reuse for elaborator monads

Stream: lean4

[Qiu]

For now TermElabM holds a single field:

  tacSnap?         : Option (Language.SnapshotBundle Tactic.TacticParsedSnapshot) := none

which works only for tactics, but not for new syntax defined by user.

To support state reuse of my own elaboration, I must go back to command level and extract my own snapshot from CommandElabM's field

snap?          : Option (Language.SnapshotBundle Language.DynamicSnapshot)

In summary, there are a few questions:

1. Are there specific reason why TermElabM is coupled with the tactic level state?
2. Are there existing plan for extending the reuse system?
3. Why is there another field tacticCache? : Option (IO.Ref Tactic.Cache) in addition to tacSnap?? I know it's used to implement save tactic. But can it be replaced by tacSnap in general?

If the answer to 2 is no, and the dev team is welcoming contributors, I am willing to help with this.
About me: I am fairly experienced in metaprogramming in Lean4 after having internship on it for bytedance in the past months. And now I have enough sophomore time to contribute.

[Sebastian Ullrich]

No, we are not currently planning on extending that. What are you trying to achieve with it?

[Qiu]

I was trying to make another set of "tactics" but with some special constraints. One of the main goals is to interleave it with by-block and so get a way to "gradually" transform it into a whole by-block. Sorry for some reason I can't put it clear here. But this really makes sense.