From f986a2e9ef5156b627ee66e4e47280a9b00f38e6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 16 Jul 2024 17:43:23 +0200 Subject: [PATCH] chore: missing `profileitM` (#4753) This PR addresses the absence of the `profileitM` function in two auxiliary functions. The added `profileitM` instances are particularly useful for diagnosing performance issues in declarations that contain many repeated sub-terms. --- src/Lean/Elab/PreDefinition/Basic.lean | 3 ++- src/Lean/Elab/PreDefinition/Main.lean | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/Basic.lean b/src/Lean/Elab/PreDefinition/Basic.lean index 17f795c3ee..0b39151d85 100644 --- a/src/Lean/Elab/PreDefinition/Basic.lean +++ b/src/Lean/Elab/PreDefinition/Basic.lean @@ -52,7 +52,8 @@ private def getLevelParamsPreDecls (preDefs : Array PreDefinition) (scopeLevelNa | Except.error msg => throwError msg | Except.ok levelParams => pure levelParams -def fixLevelParams (preDefs : Array PreDefinition) (scopeLevelNames allUserLevelNames : List Name) : TermElabM (Array PreDefinition) := do +def fixLevelParams (preDefs : Array PreDefinition) (scopeLevelNames allUserLevelNames : List Name) : TermElabM (Array PreDefinition) := +do profileitM Exception s!"fix level params" (← getOptions) do -- We used to use `shareCommon` here, but is was a bottleneck let levelParams ← getLevelParamsPreDecls preDefs scopeLevelNames allUserLevelNames let us := levelParams.map mkLevelParam diff --git a/src/Lean/Elab/PreDefinition/Main.lean b/src/Lean/Elab/PreDefinition/Main.lean index 58ecd81b62..897b197c3e 100644 --- a/src/Lean/Elab/PreDefinition/Main.lean +++ b/src/Lean/Elab/PreDefinition/Main.lean @@ -152,7 +152,7 @@ def shouldUseWF (preDefs : Array PreDefinition) : Bool := preDef.termination.decreasingBy?.isSome -def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLCtx {} {} do +def addPreDefinitions (preDefs : Array PreDefinition) : TermElabM Unit := withLCtx {} {} do profileitM Exception "add pre-definitions" (← getOptions) do for preDef in preDefs do trace[Elab.definition.body] "{preDef.declName} : {preDef.type} :=\n{preDef.value}" let preDefs ← preDefs.mapM ensureNoUnassignedMVarsAtPreDef