custom incremental elaboration

Stream: lean4

[Jovan Gerbscheid]

I have some alternative syntax with alternative tactics, in the form

theorem .. := by
  my_tactics
    my_tac1
    my_tac2
    my_tac3

And I would like to be able to use incremental elaboration on this, just like how a normal lean tactic sequence has. Can someone give a minimal example of how to do this? I know Verso does this kind of thing, but for the whole file instead of a tactic sequence.

(@Mirek Olšák was also curious about this)

[Mirek Olšák]

I experimentally checked that incremental tag together with evalTacticSeq evaluates the tactics one by one but it doesn't save the intermediate state, as other scoped tactics do. So when I have

-- testing tactic, maybe lean calls it somehow
elab "echo " s:str : tactic => logInfo s

-- my_tactics scope
syntax (name := my_tactics) "my_tactics" ppLine tacticSeq : tactic

@[tactic my_tactics, incremental]
def myScopeElab : Tactic
  | `(tactic|my_tactics $tactics) => do
    evalTacticSeq tactics
  | _ => throwUnsupportedSyntax

example : True := by
  my_tactics
    sleep 1000
    echo "hello"
    sleep 1000
    echo "world"
    trivial

and change the last world, the entire sequence gets executed again. (but it doesn't in e.g. dotted scope)

[Sebastian Ullrich]

@[tactic my_tactics, incremental]
def myScopeElab : Tactic := Term.withNarrowedArgTacticReuse 1 evalTacticSeq

Not sure about the progress bar right now. Unfortunately all of this is quite finnicky, which is also why there are no simple docs for it.

[Mirek Olšák]

Thanks, however, as I was looking into it, I am still somewhat confused. We would like to do this with another state, possibly with a different monad which Term.withNarrowedArgTacticReuse seems to support. But I couldn't figure out what is going on inside evalTacticSeq. By looking into the code, evalTacticSeq is defined to call evalTactic which looks at the root of the syntax, finds tacticSeq, and should call evalTacticSeq back. Where is the code that actually process the tactics one by one, which is compatible with this incrementality?

[Mirek Olšák]

In particular, could I write something instead of

@[tactic my_scope, incremental]
def myScopeElab : Tactic :=
  Term.withNarrowedArgTacticReuse 1
  (fun stx =>
    match stx with
      | `(tacticSeq| $[$tacs]*) => do
        tacs.forM (fun tac => evalTactic tac)
      | _ => throwUnsupportedSyntax
  )

to keep the incremental evaluation but keep control over the loop?

[Sebastian Ullrich]

Ah, you want to see the really gnarly details? They are in evalSepTactics, good luck!

[Mirek Olšák]

Oh, so

@[tactic my_tactics, incremental]
def myScopeElab : Tactic := fun stx => evalSepTactics stx[1]

actually also works, right? Or is there a catch that needs the Term.withNarrowedArgTacticReuse 1 in front of it?

[Mirek Olšák]

thanks, I will try :-)

[Mirek Olšák]

The snapshots are currently stored in the Term.Context.tacSnap?, and when I naively tried to store them in a monad on top of the stack, it didn't work. Do you think it would be possible in principle to store the snapshots above (so it can support any state), or would I have to modify the Term.Context?

[Mirek Olšák]

I think have found a way to do it -- initialize a custom Extension, use it in my custom tactic evaluation, and make a local copy of evalSepTactics, where I replace every evalTactic with my custom evaluation using that Extension, like here: https://github.com/Human-Oriented-ATP/lean-humanproof/blob/main/HumanProof/Incremental.lean

[Mirek Olšák]

@Sebastian Ullrich , do you think it could be reasonable to make the evalSepTactics more general in the standard library, to allow a custom evalTactic? Besides the "human-proof" (slightly alternative proof environment we are now looking at), there can be also environments displaying the goal in a custom form, or running a custom simplification every step...

[Sebastian Ullrich]

Your myEvalTactic doesn't actually do anything that couldn't be done in regular tactic elaborators?

[Mirek Olšák]

True but it is just a demo. The real use case we are looking at does indeed something substantially different from just extending the tactic syntax by a few more tactics.

[Sebastian Ullrich]

I don't see the problem with copying it out. This code is unlikely to change (i.e. break) in core, while your requirements may change further.

[Mirek Olšák]

I think that having a custom tactic evaluation inside evalSepTactic (possibly with environment extension keeping the extra state) covers all possible use cases, so I don't really see how our requirements could change further. But sure, let us first try with a copy to check whether this extended evalSepTactic can be indeed used for what we want, and we will get back to you later.

[Mirek Olšák]

I implemented the "real" thing with custom incremental elaboration -- our specific proof environment. I just wanted to say that it indeed didn't require anything more than a custom environment extension, and a custom command to evaluate a tactic inside the sequence (instead of the default `evalTactic). So I think that generalizing it in the library doesn't cost much, and could benefit more users in the future, who would like a custom proof environment. Having a custom script to run a line in the block is quite powerful for a tactic-writer. The only missing part (which we didn't need but some could find it helpful) would be detecting where the scope ends.

I would be also curious if there is a better way of writing:

  Term.withNarrowedArgTacticReuse 1 (
    Term.withNarrowedArgTacticReuse 0 (
      Term.withNarrowedArgTacticReuse 0 (
        (customEvalSepTactics myEvaluationOfOneTacticStep)
      )
    )
  ) stx

but when it works, it works, I guess :-).

Should we make the PR for customEvalSepTactics?

[Jovan Gerbscheid]

lean#7702