feat: add profileitM to compiler new entry point
This commit is contained in:
parent
e04453a89e
commit
104196e599
2 changed files with 2 additions and 1 deletions
|
|
@ -35,7 +35,7 @@ def checkpoint (step : Name) (decls : Array Decl) (cfg : Check.Config := {}): Co
|
|||
trace[Compiler.step] "{decl.name} := {decl.value}"
|
||||
decl.check cfg
|
||||
|
||||
def compile (declNames : Array Name) : CoreM Unit := do
|
||||
def compile (declNames : Array Name) : CoreM Unit := do profileitM Exception "compiler new" (← getOptions) do
|
||||
let declNames ← declNames.filterM shouldGenerateCode
|
||||
let decls ← declNames.mapM toDecl
|
||||
checkpoint `init decls { terminalCasesOnly := false }
|
||||
|
|
|
|||
|
|
@ -47,5 +47,6 @@ def Vec.head : Vec α (n+1) → α
|
|||
|
||||
#eval Compiler.compile #[``Lean.Elab.Term.synthesizeSyntheticMVars]
|
||||
|
||||
set_option profiler true
|
||||
set_option trace.Compiler.step true
|
||||
#eval Compiler.compile #[``Lean.Meta.isExprDefEqAuxImpl]
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue