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

feat: add timing profiling to the new compiler

Browse source
This commit is contained in:
Henrik Böving 2023-04-09 10:37:47 +02:00 • committed by Sebastian Ullrich
parent 8a302e6135
commit 36f0acfc51
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -72,8 +72,8 @@ def run (declNames : Array Name) : CompilerM (Array Decl) := withAtLeastMaxRecDe
decls := markRecDecls decls
let manager ← getPassManager
for pass in manager.passes do
trace[Compiler] "Running pass: {pass.name}"
decls ← withPhase pass.phase <| pass.run decls
decls ← withTraceNode `Compiler (fun _ => return m!"new compiler phase: {pass.phase}, pass: {pass.name}") do
withPhase pass.phase <| pass.run decls
withPhase pass.phaseOut <| checkpoint pass.name decls
if (← Lean.isTracingEnabledFor `Compiler.result) then
for decl in decls do
@ -94,7 +94,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
CompilerM.run <| discard <| PassManager.run declNames.toArray
withTraceNode `Compiler (fun _ => return m!"compiling new: {declNames}") do
CompilerM.run <| discard <| PassManager.run declNames.toArray
builtin_initialize
registerTraceClass `Compiler.init (inherited := true)