move time tactic to separate file

lecopivo · Jun 18, 2024 · d24fec2 · d24fec2
1 parent 3f5d37d
commit d24fec2
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 8 deletions.
diff --git a/SciLean/Tactic/TimeTactic.lean b/SciLean/Tactic/TimeTactic.lean
@@ -0,0 +1,10 @@
+import Lean
+import Aesop
+
+open Lean Meta Elab Term Tactic Conv in
+elab "time_tactic" t:conv : conv => do
+
+  let target ← getMainTarget
+  let ((targetNew, proof),time) ← Aesop.time <| convert target (withTacticInfoContext (← getRef) (evalTactic t))
+  liftMetaTactic1 fun mvarId => mvarId.replaceTargetEq targetNew proof
+  IO.println s!"tactic {t.raw.prettyPrint} took {time.printAsMillis}"
diff --git a/test/lsimp_basic_tests.lean b/test/lsimp_basic_tests.lean
@@ -117,14 +117,6 @@ open SciLean
 -- set_option trace.Meta.Tactic.simp.steps true
 
 
-open Lean Meta Elab Term Tactic Conv in
-elab "timeTactic" t:conv : conv => do
-
-  let target ← getMainTarget
-  let ((targetNew, proof),time) ← Aesop.time <| convert target (withTacticInfoContext (← getRef) (evalTactic t))
-  liftMetaTactic1 fun mvarId => mvarId.replaceTargetEq targetNew proof
-  IO.println s!"tactic {t.raw.prettyPrint} took {time.printAsMillis}"
-
 
 #check (∇ x : Float, let y := x * x; x * y)
   rewrite_by