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

chore: add Compiler.stat trace option

Browse source
This commit is contained in:
Leonardo de Moura 2022-08-18 00:10:56 -07:00
parent c780d390d6
commit 23be59b747
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -60,6 +60,7 @@ def compileStage1Impl (declNames : Array Name) : CoreM (Array Decl) := do
let decls ← decls.mapM (·.cse)
checkpoint `cse decls
saveStage1Decls decls
decls.forM fun decl => do trace[Compiler.stat] "{decl.name}: {← getLCNFSize decl.value}"
return decls
/--
@ -71,6 +72,7 @@ def compile (declNames : Array Name) : CoreM Unit := do profileitM Exception "co
builtin_initialize
registerTraceClass `Compiler
registerTraceClass `Compiler.stat
registerTraceClass `Compiler.init (inherited := true)
registerTraceClass `Compiler.terminalCases (inherited := true)
registerTraceClass `Compiler.simp (inherited := true)