tactic_benchmark fails when file contains sorry

[zhangir-azerbayev]

Being able to run tactic_benchmark on decls that use sorry is rather useful. For example, when benchmarking tactics on evaluations such as MiniF2F which don't come with proofs for every declaration. Currently, tactic_benchmark fails on files that contain sorry.

Suppose I replace Examples.lean with

import Mathlib.Tactic

theorem three_add_four : 3 + 4 = 7 := sorry

Then running lake exe tactic_benchmark --simp_all Examples yields

Examples
💥declaration uses 'sorry'
uncaught exception: Unexpected messages in: Examples during elaboration of (Command.declaration
 (Command.declModifiers [] [] [] [] [] [])
 (Command.theorem
  "theorem"
  (Command.declId `three_add_four [])
  (Command.declSig [] (Term.typeSpec ":" («term_=_» («term_+_» (num "3") "+" (num "4")) "=" (num "7"))))
  (Command.declValSimple ":=" (Term.sorry "sorry") [])
  []
  []))

Replacing sorry with by norm_num leads to successful execution of tactic_benchmark.

I'll work on fixing this, but I'm rather slow at metaprogramming, so if anyone wants to fix this before me it would be much appreciated.