feat: add benchmarking tactic TACBENCH (#838)

This allows a user to run 

```lean
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.

SSA.lean

@@ -1,6 +1,8 @@
 /-
 Released under Apache 2.0 license as described in the file LICENSE.
 -/
+import Mathlib.Algebra.Order.Group.Unbundled.Int
+
 
 -- Core
 -- ====

SSA/Core/Tactic.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 import SSA.Core.Framework
 import SSA.Core.Util
 import SSA.Core.MLIRSyntax.EDSL
+import SSA.Core.Tactic.TacBench
 import Qq
 import Lean.Meta.KAbstract
 import Lean.Elab.Tactic.ElabTerm

SSA/Core/Tactic/TacBench.lean

@@ -0,0 +1,105 @@
+/-
+Released under Apache 2.0 license as described in the file LICENSE.
+
+This file adds a new tactic, `tac_bench name:str T` which will log the success or failure of the tactic
+on the goal, leaving the goal unchanged.
+
+References:
+
+- `bv_compare` from Leanwuzla for running tactics: https://github.com/hargoniX/Leanwuzla/blob/4df0b4721bedcf0d3adad9818640773eef777ea7/Leanwuzla.lean#L437
+
+Authors: Siddharth Bhat
+-/
+import Lean
+open Lean.Parser.Tactic
+open Lean Meta Elab Tactic
+open Lean.Meta
+
+namespace TacBench
+/--
+Run `tac_bench <name> <tacticSeq>` to run a sequence of tactics whose runtime is benchmarked.
+This does not affect the current goal state, and thus allow multiple `tac_bench` statements to be run in sequence.
+-/
+syntax tacBenchItem := str &":" tacticSeq
+syntax (name := tacBench) "tac_bench" "["(tacBenchItem),*"]" : tactic
+
+
+def setTraceOptions (opt : Options) : Options := opt
+    |>.setBool `trace.profiler true
+    |>.setBool `trace.Meta.Tactic.bv true
+    |>.setBool `trace.Meta.Tactic.sat true
+    |>.setNat `trace.profiler.threshold 1
+
+def withFreshTraceState {α : Type} (x : TacticM α) : TacticM α := do
+    let traces ← getTraceState
+    resetTraceState
+    try x finally setTraceState traces
+
+def Nat.deltaInMs (now past : Nat) : Float := (Float.ofNat <| now - past) / 1000000.0
+
+structure Item where
+ name : String
+ tac : Syntax
+
+
+inductive Result
+| ok (item : Item) (time : Float)
+| err (item : Item) (time : Float) (e : Exception)
+
+
+def Result.toMessageData : Result → MessageData
+| .ok item timeMs => m!"TACBENCH {item.name} PASS, TIME_ELAPSED {timeMs} ms, "
+| .err item timeMs e => m!"TACBENCH {item.name} FAIL, TIME_ELAPSED {timeMs} ms, {indentD e.toMessageData}"
+
+instance : ToMessageData Result where
+  toMessageData := Result.toMessageData
+
+
+def hermeticRun (g : MVarId) (item : Item) : TacticM Result := g.withContext do
+  let t1 ← IO.monoNanosNow
+  try
+    -- TODO: think if we need this, I'm just stealing from Henrik at this point.
+    -- We can configure more options here to enable/disable tracing as needed.
+    withOptions setTraceOptions <| withoutModifyingEnv <| withoutModifyingState <| withFreshTraceState do
+      evalTactic item.tac
+      let t2 ← IO.monoNanosNow
+      return .ok item (Nat.deltaInMs t2 t1)
+  catch e =>
+    let t2 ← IO.monoNanosNow
+    return .err item (Nat.deltaInMs t2 t1) e
+
+
+
+def parseTacBenchItem : TSyntax ``tacBenchItem → TacticM Item
+| `(tacBenchItem| $name:str : $tac:tacticSeq) => 
+     return { name := name.getString, tac := tac : Item }
+| _ => throwUnsupportedSyntax
+
+
+@[tactic tacBench]
+def evalTacBench : Tactic := fun
+| `(tactic| tac_bench [$tacBenchItems:tacBenchItem,*]) => do
+    let g ← getMainGoal
+    let items ← tacBenchItems.getElems.mapM parseTacBenchItem
+    -- logInfo m!{← hermeticRun g tac}
+    let mut msg := m!""
+    for item in items do
+      let out ← hermeticRun g item
+      msg := msg ++ m!"\n" ++ out.toMessageData
+    logInfo m!"TACSTART{.nestD msg}\nTACEND"
+| _ => throwUnsupportedSyntax
+end TacBench
+
+
+section Examples
+theorem eg1 : 1 = 1 := by
+  tac_bench ["rfl" : rfl, "wrong" : (rw [Nat.add_comm]), "success" : simp, "done" : done, "sorry" : sorry]
+  sorry
+
+theorem eg2 (x y : BitVec 8) : x * y = y * x := by
+  tac_bench ["bv_decide" :  bv_decide, "ac_nf" : ac_nf]
+  sorry
+
+end Examples
+
+