Tactic.run idiosyncrasies

Stream: lean4

[Josh Clune]

I'm trying to benchmark a tactic I've been working on, but I've been running into issues where the function I use to evaluate my tactic gives different results from running the tactic in practice.

Here is a minimal version of what I'm trying to do:

def testMyTactic (goal : Expr) (tac : TacticM Unit) : MetaM Bool := do
  let g ← mkFreshExprMVar goal -- Run `tac` on `goal`
  let gs ←
    try
      TermElabM.run' do
        pure $ some $ ← Tactic.run g.mvarId! tac
    catch e =>
      dbg_trace "Error: {← e.toMessageData.toString}"
      pure none
  return gs.isSome

I expect and intend for testMyTactic to run tac on goal and return false if and only if the tactic threw an error. But I've encountered situations where tac will work in practice but testMyTactic will claim it encountered an error. I describe one example of this more fully in #metaprogramming / tactics > Difference between Tactic.run and actually running tactic.

What are the known differences in behavior between actually running a tactic in the environment and trying to test the behavior of a tactic using Tactic.run? Are there any gotchas I should know about regarding how I'm using TermElabM.run or Tactic.run?