See what a tactic does and roll back

Stream: metaprogramming / tactics

[Patrick Massot]

In a tactic, is there a way to tell Lean to apply a tactic, inspect the resulting tactic state and they roll back to the previous tactic state without loosing all information? I am meta-meta-programming. I want my tactic to inspect the goal, say: "If you apply assumption h then the new goal will be ..." but not actually applying assumption h. I know I can do

do { apply h, trace "some text, fail "" } <|> do
...

but this only work with trace, I can't assign a variable in the first block and use it in the second one. Does my question make sense?

[Alex J. Best]

Maybe docs#tactic.lock_tactic_state ?

import tactic.core

open tactic
meta def ta : tactic unit :=
do
  l ← lock_tactic_state (do `[apply false.elim], get_state),
  trace l


lemma o : true :=
begin
  ta,
end

[Rob Lewis]

Is docs#tactic.lock_tactic_state the same as docs#tactic.retrieve ?

[Mario Carneiro]

No, it's the same as docs#tactic.retrieve'

[Mario Carneiro]

The difference is that regular retrieve does not roll back the tactic state in case of error while retrieve' rolls it back either way

[Rob Lewis]

Er, yeah, that's the one I was reading. Pesky ' is hard to see

[Rob Lewis]

Should we dedup these?

[Patrick Massot]

thanks everybody!