From 28538fc74889ea2dedbc30e236ce26492e5823ca Mon Sep 17 00:00:00 2001 From: Henrik Date: Thu, 11 May 2023 19:30:02 +0200 Subject: [PATCH] feat: trace nodes for kernel type checking --- src/Lean/CoreM.lean | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index 70bcd32a1d..c38191e82f 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -19,6 +19,8 @@ register_builtin_option maxHeartbeats : Nat := { descr := "maximum amount of heartbeats per command. A heartbeat is number of (small) memory allocations (in thousands), 0 means no limit" } +builtin_initialize registerTraceClass `Kernel + def getMaxHeartbeats (opts : Options) : Nat := maxHeartbeats.get opts * 1000 @@ -270,12 +272,14 @@ def Exception.isMaxHeartbeat (ex : Exception) : Bool := def mkArrow (d b : Expr) : CoreM Expr := return Lean.mkForall (← mkFreshUserName `x) BinderInfo.default d b -def addDecl (decl : Declaration) : CoreM Unit := do profileitM Exception "type checking" (← getOptions) do - if !(← MonadLog.hasErrors) && decl.hasSorry then - logWarning "declaration uses 'sorry'" - match (← getEnv).addDecl decl with - | Except.ok env => setEnv env - | Except.error ex => throwKernelException ex +def addDecl (decl : Declaration) : CoreM Unit := do + profileitM Exception "type checking" (← getOptions) do + withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do + if !(← MonadLog.hasErrors) && decl.hasSorry then + logWarning "declaration uses 'sorry'" + match (← getEnv).addDecl decl with + | Except.ok env => setEnv env + | Except.error ex => throwKernelException ex private def supportedRecursors := #[``Empty.rec, ``False.rec, ``Eq.ndrec, ``Eq.rec, ``Eq.recOn, ``Eq.casesOn, ``False.casesOn, ``Empty.casesOn, ``And.rec, ``And.casesOn]