Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: See what a tactic does and roll back


Patrick Massot (Jan 19 2022 at 18:25):

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 (Jan 19 2022 at 18:35):

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 (Jan 19 2022 at 18:37):

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

Mario Carneiro (Jan 19 2022 at 18:53):

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

Mario Carneiro (Jan 19 2022 at 18:54):

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 (Jan 19 2022 at 18:57):

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

Rob Lewis (Jan 19 2022 at 18:57):

Should we dedup these?

Patrick Massot (Jan 19 2022 at 19:03):

thanks everybody!


Last updated: Dec 20 2023 at 11:08 UTC