feat: add benchmarking tactic TACBENCH

[bollu]

This allows a user to run

theorem eg1 : 1 = 1 := by
  tac_bench ["rfl" : rfl, "wrong" : (rw [Nat.add_comm]), "success" : simp, "done" : done, "sorry" : sorry]
  sorry

which results in the trace output of

▶ 94:3-94:107: information:
TACSTART
  TACBENCH rfl PASS, TIME_ELAPSED 0.691666 ms, 
  TACBENCH wrong FAIL, TIME_ELAPSED 0.129250 ms, 
    tactic 'rewrite' failed, did not find instance of the pattern in the target expression
      ?n + ?m
    ⊢ 1 = 1
  TACBENCH success PASS, TIME_ELAPSED 0.290417 ms, 
  TACBENCH done FAIL, TIME_ELAPSED 0.030875 ms, 
    internal exception #4
  TACBENCH sorry PASS, TIME_ELAPSED 0.120958 ms, 
TACEND

which can be then parsed by our tools for easy benchmarking.

[github-actions]

Alive Statistics: 90 / 93 (3 failed)