From 14944aeb3c0d8ec0df738087b72cc0db494d1f36 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 25 Aug 2022 18:11:49 -0700
Subject: [PATCH] chore: print decl size at trace message

---
 src/Lean/Compiler/LCNF/Main.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Compiler/LCNF/Main.lean b/src/Lean/Compiler/LCNF/Main.lean
index 646f8e3907..d1d166a15a 100644
--- a/src/Lean/Compiler/LCNF/Main.lean
+++ b/src/Lean/Compiler/LCNF/Main.lean
@@ -43,7 +43,7 @@ def checkpoint (stepName : Name) (decls : Array Decl) : CompilerM Unit := do
     withOptions (fun opts => opts.setBool `pp.motives.pi false) do
       let clsName := `Compiler ++ stepName
       if (← Lean.isTracingEnabledFor clsName) then
-        Lean.addTrace clsName m!"\n{← ppDecl decl}"
+        Lean.addTrace clsName m!"size: {decl.size}\n{← ppDecl decl}"
       if compiler.check.get (← getOptions) then
         decl.check