From beeeead99fe04a2b00cb10ad42c19f14b9cd913a Mon Sep 17 00:00:00 2001 From: Cameron Zwarich Date: Tue, 8 Jul 2025 07:15:15 -0700 Subject: [PATCH] chore: remove mentions of the compiler being new from trace messages (#9253) --- src/Lean/Compiler/LCNF/Main.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Lean/Compiler/LCNF/Main.lean b/src/Lean/Compiler/LCNF/Main.lean index 4ab2201643..94e56ccf55 100644 --- a/src/Lean/Compiler/LCNF/Main.lean +++ b/src/Lean/Compiler/LCNF/Main.lean @@ -100,7 +100,7 @@ def run (declNames : Array Name) : CompilerM (Array IR.Decl) := withAtLeastMaxRe let manager ← getPassManager let isCheckEnabled := compiler.check.get (← getOptions) for pass in manager.passes do - decls ← withTraceNode `Compiler (fun _ => return m!"new compiler phase: {pass.phase}, pass: {pass.name}") 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) if (← Lean.isTracingEnabledFor `Compiler.result) then @@ -135,8 +135,8 @@ def showDecl (phase : Phase) (declName : Name) : CoreM Format := do @[export lean_lcnf_compile_decls] def main (declNames : List Name) : CoreM Unit := do - profileitM Exception "compilation new" (← getOptions) do - withTraceNode `Compiler (fun _ => return m!"compiling new: {declNames}") do + profileitM Exception "compilation" (← getOptions) do + withTraceNode `Compiler (fun _ => return m!"compiling: {declNames}") do CompilerM.run <| discard <| PassManager.run declNames.toArray builtin_initialize