Manipulating custom tactic state

Stream: lean4

[Leni Aniva]

Hi people, I am trying to create a machine interactable theorem proving environment. Ideally I want an interface where I can create a tactic state with a goal and execute tactics on it with backtracking enabled. I read in Lean/Elab/Tactic/Basic.lean that there are these two types and this function

abbrev TacticM := ReaderT Context $ StateRefT State TermElabM
abbrev Tactic  := Syntax → TacticM Unit
...
def run (mvarId : MVarId) (x : TacticM Unit) : TermElabM (List MVarId)

It seems like I can feed a tactic and a metavar into run and the tactic would manipulate the proof state. What I don't understand from this code is where can I provide the context? I have Environment objects and I would like to use them as the context.

[Scott Morrison]

TermElabM is itself a monad, responsible for maintaining that context.

[Mario Carneiro]

most of the context like the environment is hidden in the monad state of TermElabM here

[Scott Morrison]

It's a bit hard to tell what you want to do: it sounds like Lean itself is the solution to the problem you've specified. :-)

[Leni Aniva]

Scott Morrison said:

It's a bit hard to tell what you want to do: it sounds like Lean itself is the solution to the problem you've specified. :-)

I'm building a text based interface to run tactics on custom examples. Both the examples (theorem to be proven) and tactics will be fed in by text

[Leni Aniva]

Mario Carneiro said:

most of the context like the environment is hidden in the monad state of TermElabM here

What is StateRefT?

[Mario Carneiro]

You should think of it as StateT, that is, it has a state value that is modified and passed out

[Mario Carneiro]

in lean State = read-write data

[Mario Carneiro]

and Context / Reader = read-only data

[Leni Aniva]

How is StateRefT different from StateT and State?

[Mario Carneiro]

StateRefT implements the API of StateT but it uses mutable references behind the scenes to do it

[Leni Aniva]

Thanks! That answers all of my questions