max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: print decl size at trace message

Browse source
This commit is contained in:
Leonardo de Moura 2022-08-25 18:11:49 -07:00
parent 4c9c2d2bf7
commit 14944aeb3c
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Compiler/LCNF/Main.lean
View file

@ -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