From 544f9912b70df75511e73eaef1f57573bf92b351 Mon Sep 17 00:00:00 2001
From: Cameron Zwarich <cameron@lean-fro.org>
Date: Sat, 9 Aug 2025 22:00:49 -0700
Subject: [PATCH] chore: add separate profiling entries for base, mono, and IR
 phases (#9817)

---
 src/Lean/Compiler/LCNF/Main.lean | 36 +++++++++++++++++++-------------
 1 file changed, 21 insertions(+), 15 deletions(-)

diff --git a/src/Lean/Compiler/LCNF/Main.lean b/src/Lean/Compiler/LCNF/Main.lean
index 085ab0ea89..d9859e172a 100644
--- a/src/Lean/Compiler/LCNF/Main.lean
+++ b/src/Lean/Compiler/LCNF/Main.lean
@@ -108,24 +108,31 @@ def run (declNames : Array Name) : CompilerM (Array IR.Decl) := withAtLeastMaxRe
       if let some info ← getDeclInfo? declName then
         if !(isValidMainType info.type) then
           throwError "`main` function must have type `(List String →)? IO (UInt32 | Unit | PUnit)`"
-  let mut decls ← declNames.mapM toDecl
-  decls := markRecDecls decls
+  let decls ← declNames.mapM toDecl
+  let decls := markRecDecls decls
   let manager ← getPassManager
   let isCheckEnabled := compiler.check.get (← getOptions)
-  for pass in manager.basePasses do
-    decls ← withTraceNode `Compiler (fun _ => return m!"compiler phase: {pass.phase}, pass: {pass.name}") do
-      withPhase pass.phase <| pass.run decls
-    withPhase pass.phaseOut <| checkpoint pass.name decls (isCheckEnabled || pass.shouldAlwaysRunCheck)
-  for pass in manager.monoPasses do
-    decls ← withTraceNode `Compiler (fun _ => return m!"compiler phase: {pass.phase}, pass: {pass.name}") do
-      withPhase pass.phase <| pass.run decls
-    withPhase pass.phaseOut <| checkpoint pass.name decls (isCheckEnabled || pass.shouldAlwaysRunCheck)
+  let decls ← profileitM Exception "compilation (LCNF base)" (← getOptions) do
+    let mut decls := decls
+    for pass in manager.basePasses do
+      decls ← withTraceNode `Compiler (fun _ => return m!"compiler phase: {pass.phase}, pass: {pass.name}") do
+        withPhase pass.phase <| pass.run decls
+      withPhase pass.phaseOut <| checkpoint pass.name decls (isCheckEnabled || pass.shouldAlwaysRunCheck)
+    return decls
+  let decls ← profileitM Exception "compilation (LCNF mono)" (← getOptions) do
+    let mut decls := decls
+    for pass in manager.monoPasses do
+      decls ← withTraceNode `Compiler (fun _ => return m!"compiler phase: {pass.phase}, pass: {pass.name}") do
+        withPhase pass.phase <| pass.run decls
+      withPhase pass.phaseOut <| checkpoint pass.name decls (isCheckEnabled || pass.shouldAlwaysRunCheck)
+    return decls
   if (← Lean.isTracingEnabledFor `Compiler.result) then
     for decl in decls do
       let decl ← normalizeFVarIds decl
       Lean.addTrace `Compiler.result m!"size: {decl.size}\n{← ppDecl' decl}"
-  let irDecls ← IR.toIR decls
-  IR.compile irDecls
+  profileitM Exception "compilation (IR)" (← getOptions) do
+    let irDecls ← IR.toIR decls
+    IR.compile irDecls
 
 end PassManager
 
@@ -138,9 +145,8 @@ def showDecl (phase : Phase) (declName : Name) : CoreM Format := do
 
 @[export lean_lcnf_compile_decls]
 def main (declNames : Array Name) : CoreM Unit := do
-  profileitM Exception "compilation" (← getOptions) do
-    withTraceNode `Compiler (fun _ => return m!"compiling: {declNames}") do
-      CompilerM.run <| discard <| PassManager.run declNames
+  withTraceNode `Compiler (fun _ => return m!"compiling: {declNames}") do
+    CompilerM.run <| discard <| PassManager.run declNames
 
 builtin_initialize
   registerTraceClass `Compiler.init (inherited := true)