using dojo object for intermediate <state, tactic> pair

[Sara-Rajaee]

Hi, I'm diving into the implementation of lean-dojo library and I was wondering if an arbitrary pair of tactic and state is applicable on the related dojo object.
For example,
`dojo, state_0 = Dojo(theorem)._enter_()

response = dojo(state_2, tactic)`

Here I'm not using state_0 as the initial state to apply tactic. I'm starting the proof from state_2.

[yangky11]

Where does state_2 come from?

[Sara-Rajaee]

Let's say we know a proof for an example. So instead of starting the proof from the initial state, I was wondering if I can apply a known state and tactic to the dojo object. In other words, does the interaction with lean needs to be sequential? or for a specific theorem, if I can begin the proof from an arbitrary state.

[yangky11]

It does not need to be sequential. You can run a tactic on an older state you've seen before. However, the older state has to come from previous interactions in the same Dojo instance. You cannot, say, pickle a state to disk and load it in another process.