diff --git a/src/Lean/Compiler/Main.lean b/src/Lean/Compiler/Main.lean index d146065563..101ae3b722 100644 --- a/src/Lean/Compiler/Main.lean +++ b/src/Lean/Compiler/Main.lean @@ -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 } diff --git a/tests/lean/run/lcnf1.lean b/tests/lean/run/lcnf1.lean index 6b32771f71..60e4da001e 100644 --- a/tests/lean/run/lcnf1.lean +++ b/tests/lean/run/lcnf1.lean @@ -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]