feat: show typeclass and tactic names in profile output

leanprover · Mar 27, 2023 · b076d48 · b076d48
1 parent 4048455
commit b076d48
Show file tree

Hide file tree

Showing 4 changed files with 12 additions and 11 deletions.
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
@@ -140,7 +140,7 @@ structure EvalTacticFailure where
   state : SavedState
 
 partial def evalTactic (stx : Syntax) : TacticM Unit := do
-  profileitM Exception "tactic execution" (← getOptions) <|
+  profileitM Exception "tactic execution" (decl := stx.getKind) (← getOptions) <|
   withRef stx <| withIncRecDepth <| withFreshMacroScope <| match stx with
     | .node _ k _    =>
       if k == nullKind then

diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
@@ -658,7 +658,7 @@ private def preprocessOutParam (type : Expr) : MetaM Expr :=
   Remark: we use a different option for controlling the maximum result size for coercions.
 -/
 
-def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do profileitM Exception "typeclass inference" (← getOptions) do
+def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do profileitM Exception "typeclass inference" (← getOptions) (decl := type.getAppFn.constName?.getD .anonymous) do
   let opts ← getOptions
   let maxResultSize := maxResultSize?.getD (synthInstance.maxSize.get opts)
   withTraceNode `Meta.synthInstance

diff --git a/src/Lean/Util/Profile.lean b/src/Lean/Util/Profile.lean
@@ -9,18 +9,18 @@ namespace Lean
 
 /-- Print and accumulate run time of `act` when option `profiler` is set to `true`. -/
 @[extern "lean_profileit"]
-def profileit {α : Type} (category : @& String) (opts : @& Options) (fn : Unit → α) : α := fn ()
+def profileit {α : Type} (category : @& String) (opts : @& Options) (fn : Unit → α) (decl := Name.anonymous) : α := fn ()
 
-unsafe def profileitIOUnsafe {ε α : Type} (category : String) (opts : Options) (act : EIO ε α) : EIO ε α :=
-  match profileit category opts fun _ => unsafeEIO act with
+unsafe def profileitIOUnsafe {ε α : Type} (category : String) (opts : Options) (act : EIO ε α) (decl := Name.anonymous) : EIO ε α :=
+  match profileit (decl := decl) category opts fun _ => unsafeEIO act with
   | Except.ok a    => pure a
   | Except.error e => throw e
 
 @[implemented_by profileitIOUnsafe]
-def profileitIO {ε α : Type} (category : String) (opts : Options) (act : EIO ε α) : EIO ε α := act
+def profileitIO {ε α : Type} (category : String) (opts : Options) (act : EIO ε α) (decl := Name.anonymous) : EIO ε α := act
 
 -- impossible to infer `ε`
-def profileitM {m : Type → Type} (ε : Type) [MonadFunctorT (EIO ε) m] {α : Type} (category : String) (opts : Options) (act : m α) : m α :=
-  monadMap (fun {β} => profileitIO (ε := ε) (α := β) category opts) act
+def profileitM {m : Type → Type} (ε : Type) [MonadFunctorT (EIO ε) m] {α : Type} (category : String) (opts : Options) (act : m α) (decl := Name.anonymous) : m α :=
+  monadMap (fun {β} => profileitIO (ε := ε) (α := β) (decl := decl) category opts) act
 
 end Lean
diff --git a/src/library/time_task.cpp b/src/library/time_task.cpp
@@ -68,10 +68,11 @@ time_task::~time_task() {
     }
 }
 
-/* profileit {α : Type} (category : String) (opts : Options) (fn : Unit → α) : α */
-extern "C" LEAN_EXPORT obj_res lean_profileit(b_obj_arg category, b_obj_arg opts, obj_arg fn) {
+/* profileit {α : Type} (category : String) (opts : Options) (fn : Unit → α) (decl : Name) : α */
+extern "C" LEAN_EXPORT obj_res lean_profileit(b_obj_arg category, b_obj_arg opts, obj_arg fn, obj_arg decl) {
     time_task t(string_to_std(category),
-                TO_REF(options, opts));
+                TO_REF(options, opts),
+                name(decl));
     return apply_1(fn, box(0));
 }
 }