From 8c4db341ddbbf63479b7fba73c270f27e5143f99 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 25 Aug 2025 16:20:36 -0700 Subject: [PATCH] chore: use `ofConstName` in error messages (#10121) --- src/Lean/Attributes.lean | 4 ++-- src/Lean/Compiler/IR/Checker.lean | 2 +- src/Lean/Compiler/ImplementedByAttr.lean | 4 ++-- src/Lean/Compiler/InlineAttrs.lean | 4 ++-- src/Lean/Compiler/LCNF/Check.lean | 2 +- src/Lean/Compiler/LCNF/Simp/SimpM.lean | 8 ++++---- src/Lean/Compiler/LCNF/ToDecl.lean | 4 ++-- src/Lean/Compiler/LCNF/ToLCNF.lean | 2 +- src/Lean/CoreM.lean | 2 +- src/Lean/DocString/Add.lean | 2 +- src/Lean/DocString/Extension.lean | 2 +- src/Lean/Elab/DeclModifiers.lean | 4 ++-- src/Lean/Elab/Deriving/Basic.lean | 2 +- src/Lean/Elab/Deriving/Inhabited.lean | 2 +- src/Lean/Elab/LetRec.lean | 2 +- src/Lean/Elab/PreDefinition/Eqns.lean | 8 ++++---- .../PreDefinition/PartialFixpoint/Eqns.lean | 2 +- .../Elab/PreDefinition/Structural/Eqns.lean | 2 +- .../BVDecide/Frontend/Normalize/Enums.lean | 6 +++--- src/Lean/Elab/Tactic/Rewrite.lean | 2 +- src/Lean/Elab/Tactic/Simp.lean | 4 ++-- src/Lean/KeyedDeclsAttribute.lean | 2 +- src/Lean/Meta/Instances.lean | 8 ++++---- src/Lean/Meta/Match/MatchPatternAttr.lean | 2 +- src/Lean/Meta/RecursorInfo.lean | 20 +++++++++---------- src/Lean/Meta/Structure.lean | 2 +- src/Lean/Meta/Tactic/Ext.lean | 2 +- src/Lean/Meta/Tactic/Simp/Attr.lean | 4 ++-- src/Lean/Meta/Tactic/Simp/Simproc.lean | 20 +++++++++---------- src/Lean/Meta/Tactic/Unfold.lean | 4 ++-- src/Lean/Parser/Extension.lean | 7 ++++--- src/Lean/Parser/Tactic/Doc.lean | 4 ++-- src/Lean/ReducibilityAttrs.lean | 18 ++++++++--------- src/Lean/ResolveName.lean | 2 +- .../lean/implementedByIssue.lean.expected.out | 4 ++-- 35 files changed, 85 insertions(+), 84 deletions(-) diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index 1fb424d1a9..2ba0b3f982 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -139,7 +139,7 @@ def throwAttrNotInAsyncCtx (attrName declName : Name) (asyncPrefix? : Option Nam throwError "Cannot add attribute `[{attrName}]` to declaration `{.ofConstName declName}` because it is not from the present async context{asyncPrefix}" def throwAttrDeclNotOfExpectedType (attrName declName : Name) (givenType expectedType : Expr) : m α := - throwError m!"Cannot add attribute `[{attrName}]`: Declaration `{declName}` has type{indentExpr givenType}\n\ + throwError m!"Cannot add attribute `[{attrName}]`: Declaration `{.ofConstName declName}` has type{indentExpr givenType}\n\ but `[{attrName}]` can only be added to declarations of type{indentExpr expectedType}" end @@ -383,7 +383,7 @@ unsafe def mkAttributeImplOfConstantUnsafe (env : Environment) (opts : Options) | some info => match info.type with | Expr.const `Lean.AttributeImpl _ => env.evalConst AttributeImpl opts declName - | _ => throw s!"Unexpected attribute implementation type: `{declName}` is not of type `Lean.AttributeImpl`" + | _ => throw "Unexpected attribute implementation type: `{.ofConstName declName}` is not of type `Lean.AttributeImpl`" @[implemented_by mkAttributeImplOfConstantUnsafe] opaque mkAttributeImplOfConstant (env : Environment) (opts : Options) (declName : Name) : Except String AttributeImpl diff --git a/src/Lean/Compiler/IR/Checker.lean b/src/Lean/Compiler/IR/Checker.lean index 22547c33e2..45496ea5a9 100644 --- a/src/Lean/Compiler/IR/Checker.lean +++ b/src/Lean/Compiler/IR/Checker.lean @@ -41,7 +41,7 @@ abbrev M := ReaderT CheckerContext <| StateRefT CheckerState CompilerM def throwCheckerError {α : Type} (msg : String) : M α := do let declName := (← read).currentDecl.name - throwError s!"failed to compile definition, compiler IR check failed at '{declName}'. Error: {msg}" + throwError "failed to compile definition, compiler IR check failed at `{.ofConstName declName}`. Error: {msg}" def markIndex (i : Index) : M Unit := do let s ← get diff --git a/src/Lean/Compiler/ImplementedByAttr.lean b/src/Lean/Compiler/ImplementedByAttr.lean index ea37ac247e..0a16662cc7 100644 --- a/src/Lean/Compiler/ImplementedByAttr.lean +++ b/src/Lean/Compiler/ImplementedByAttr.lean @@ -58,11 +58,11 @@ builtin_initialize implementedByAttr : ParametricAttribute Name ← registerPara let fnName ← Elab.realizeGlobalConstNoOverloadWithInfo fnNameStx let fnDecl ← getConstVal fnName unless decl.levelParams.length == fnDecl.levelParams.length do - throwError "Invalid `implemented_by` argument `{fnName}`: `{fnName}` has {fnDecl.levelParams.length} universe level parameter(s), but `{declName}` has {decl.levelParams.length}" + throwError "Invalid `implemented_by` argument `{fnName}`: `{fnName}` has {fnDecl.levelParams.length} universe level parameter(s), but `{.ofConstName declName}` has {decl.levelParams.length}" let declType := decl.type let fnType ← Core.instantiateTypeLevelParams fnDecl (decl.levelParams.map mkLevelParam) unless declType == fnType do - throwError "Invalid `implemented_by` argument `{fnName}`: `{fnName}` has type{indentExpr fnType}\nbut `{declName}` has type{indentExpr declType}" + throwError "Invalid `implemented_by` argument `{fnName}`: `{fnName}` has type{indentExpr fnType}\nbut `{.ofConstName declName}` has type{indentExpr declType}" if decl.name == fnDecl.name then throwError "Invalid `implemented_by` argument `{fnName}`: Definition cannot be implemented by itself" return fnName diff --git a/src/Lean/Compiler/InlineAttrs.lean b/src/Lean/Compiler/InlineAttrs.lean index 67f84d7667..c3fc04312a 100644 --- a/src/Lean/Compiler/InlineAttrs.lean +++ b/src/Lean/Compiler/InlineAttrs.lean @@ -76,10 +76,10 @@ builtin_initialize inlineAttrs : EnumAttributes InlineAttributeKind ← s!"Cannot add attribute `[{kind.toAttrString}]`: {e}" if kind matches .macroInline then unless (← isValidMacroInline declName) do - throwError "Cannot add `[macro_inline]` attribute to `{declName}`: This attribute does not support this kind of declaration; only non-recursive definitions are supported" + throwError "Cannot add `[macro_inline]` attribute to `{.ofConstName declName}`: This attribute does not support this kind of declaration; only non-recursive definitions are supported" withExporting (isExporting := !isPrivateName declName) do if !(← getConstInfo declName).isDefinition then - throwError "invalid `[macro_inline]` attribute, '{declName}' must be an exposed definition" + throwError "invalid `[macro_inline]` attribute, '{.ofConstName declName}' must be an exposed definition" def setInlineAttribute (env : Environment) (declName : Name) (kind : InlineAttributeKind) : Except String Environment := inlineAttrs.setValue env declName kind diff --git a/src/Lean/Compiler/LCNF/Check.lean b/src/Lean/Compiler/LCNF/Check.lean index c7c900a42c..ccf54c3950 100644 --- a/src/Lean/Compiler/LCNF/Check.lean +++ b/src/Lean/Compiler/LCNF/Check.lean @@ -200,7 +200,7 @@ partial def checkFunDeclCore (declName : Name) (params : Array Param) (type : Ex if (← checkTypes) then let valueType ← mkForallParams params (← value.inferType) unless (← InferType.compatibleTypes type valueType) do - throwError "type mismatch at `{declName}`, value has type{indentExpr valueType}\nbut is expected to have type{indentExpr type}" + throwError "type mismatch at `{.ofConstName declName}`, value has type{indentExpr valueType}\nbut is expected to have type{indentExpr type}" partial def checkFunDecl (funDecl : FunDecl) : CheckM Unit := do checkFunDeclCore funDecl.binderName funDecl.params funDecl.type funDecl.value diff --git a/src/Lean/Compiler/LCNF/Simp/SimpM.lean b/src/Lean/Compiler/LCNF/Simp/SimpM.lean index 856a06139e..f1d1a10dc0 100644 --- a/src/Lean/Compiler/LCNF/Simp/SimpM.lean +++ b/src/Lean/Compiler/LCNF/Simp/SimpM.lean @@ -135,12 +135,12 @@ Otherwise, do not change the `inlineStack`. x where check (declName : Name) : SimpM Nat := do - trace[Compiler.simp.inline] "{declName}" + trace[Compiler.simp.inline] "{.ofConstName declName}" let numOccs := (← read).inlineStackOccs.find? declName |>.getD 0 let numOccs := numOccs + 1 let inlineIfReduce ← if let some decl ← getDecl? declName then pure decl.inlineIfReduceAttr else pure false if recursive && inlineIfReduce && numOccs > (← getConfig).maxRecInlineIfReduce then - throwError "function `{declName}` has been recursively inlined more than #{(← getConfig).maxRecInlineIfReduce}, consider removing the attribute `[inline_if_reduce]` from this declaration or increasing the limit using `set_option compiler.maxRecInlineIfReduce `" + throwError "function `{.ofConstName declName}` has been recursively inlined more than #{(← getConfig).maxRecInlineIfReduce}, consider removing the attribute `[inline_if_reduce]` from this declaration or increasing the limit using `set_option compiler.maxRecInlineIfReduce `" return numOccs /-- @@ -158,7 +158,7 @@ where match (← read).inlineStack with | [] => throwError maxRecDepthErrorMessage | declName :: stack => - let mut fmt := f!"{declName}\n" + let mut fmt := m!"{.ofConstName declName}\n" let mut prev := declName let mut ellipsis := false for declName in stack do @@ -167,7 +167,7 @@ where ellipsis := true fmt := fmt ++ "...\n" else - fmt := fmt ++ f!"{declName}\n" + fmt := fmt ++ m!"{.ofConstName declName}\n" prev := declName ellipsis := false throwError "maximum recursion depth reached in the code generator\nfunction inline stack:\n{fmt}" diff --git a/src/Lean/Compiler/LCNF/ToDecl.lean b/src/Lean/Compiler/LCNF/ToDecl.lean index 25ef2bc1ae..bad8963e20 100644 --- a/src/Lean/Compiler/LCNF/ToDecl.lean +++ b/src/Lean/Compiler/LCNF/ToDecl.lean @@ -101,7 +101,7 @@ The steps for this are roughly: -/ def toDecl (declName : Name) : CompilerM Decl := do let declName := if let some name := isUnsafeRecName? declName then name else declName - let some info ← getDeclInfo? declName | throwError "declaration `{declName}` not found" + let some info ← getDeclInfo? declName | throwError "declaration `{.ofConstName declName}` not found" let safe := !info.isPartial && !info.isUnsafe let env ← getEnv let inlineAttr? := getInlineAttribute? env declName @@ -125,7 +125,7 @@ def toDecl (declName : Name) : CompilerM Decl := do let params ← paramsFromTypeBinders type return { name := declName, params, type, value := .extern { entries := [] }, levelParams := info.levelParams, safe, inlineAttr? } else - let some value := info.value? (allowOpaque := true) | throwError "declaration `{declName}` does not have a value" + let some value := info.value? (allowOpaque := true) | throwError "declaration `{.ofConstName declName}` does not have a value" let (type, value) ← Meta.MetaM.run' do let type ← toLCNFType info.type let value ← Meta.lambdaTelescope value fun xs body => do Meta.mkLambdaFVars xs (← Meta.etaExpand body) diff --git a/src/Lean/Compiler/LCNF/ToLCNF.lean b/src/Lean/Compiler/LCNF/ToLCNF.lean index 83ba04151a..ed1ccece97 100644 --- a/src/Lean/Compiler/LCNF/ToLCNF.lean +++ b/src/Lean/Compiler/LCNF/ToLCNF.lean @@ -686,7 +686,7 @@ where let type ← toLCNFType (← liftMetaM <| Meta.inferType e) mkUnreachable type | _, _ => - throwError "code generator failed, unsupported occurrence of `{declName}`" + throwError "code generator failed, unsupported occurrence of `{.ofConstName declName}`" expandNoConfusionMajor (major : Expr) (numFields : Nat) : M Expr := do match numFields with diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean index ea610e5be4..0e281aa937 100644 --- a/src/Lean/CoreM.lean +++ b/src/Lean/CoreM.lean @@ -674,7 +674,7 @@ private def checkUnsupported [Monad m] [MonadEnv m] [MonadError m] (decl : Decla && !supportedRecursors.contains declName | _ => false match unsupportedRecursor? with - | some (Expr.const declName ..) => throwError "code generator does not support recursor '{declName}' yet, consider using 'match ... with' and/or structural recursion" + | some (Expr.const declName ..) => throwError "code generator does not support recursor '{.ofConstName declName}' yet, consider using 'match ... with' and/or structural recursion" | _ => pure () /-- diff --git a/src/Lean/DocString/Add.lean b/src/Lean/DocString/Add.lean index 833298a0b9..5dcd284c3b 100644 --- a/src/Lean/DocString/Add.lean +++ b/src/Lean/DocString/Add.lean @@ -49,7 +49,7 @@ def addDocString [Monad m] [MonadError m] [MonadEnv m] [MonadLog m] [AddMessageContext m] [MonadOptions m] [MonadLiftT IO m] (declName : Name) (docComment : TSyntax `Lean.Parser.Command.docComment) : m Unit := do unless (← getEnv).getModuleIdxFor? declName |>.isNone do - throwError s!"invalid doc string, declaration '{declName}' is in an imported module" + throwError "invalid doc string, declaration '{.ofConstName declName}' is in an imported module" validateDocComment docComment let docString : String ← getDocStringText docComment modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces diff --git a/src/Lean/DocString/Extension.lean b/src/Lean/DocString/Extension.lean index 7365fde8c9..d005447185 100644 --- a/src/Lean/DocString/Extension.lean +++ b/src/Lean/DocString/Extension.lean @@ -34,7 +34,7 @@ def addBuiltinDocString (declName : Name) (docString : String) : IO Unit := do def addDocStringCore [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString : String) : m Unit := do unless (← getEnv).getModuleIdxFor? declName |>.isNone do - throwError s!"invalid doc string, declaration '{declName}' is in an imported module" + throwError "invalid doc string, declaration '{.ofConstName declName}' is in an imported module" modifyEnv fun env => docStringExt.insert env declName docString.removeLeadingSpaces def addDocStringCore' [Monad m] [MonadError m] [MonadEnv m] (declName : Name) (docString? : Option String) : m Unit := diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean index e059383130..4470e20dcb 100644 --- a/src/Lean/Elab/DeclModifiers.lean +++ b/src/Lean/Elab/DeclModifiers.lean @@ -38,7 +38,7 @@ def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadError m] [MonadFina | none => throwError "'{.ofConstName declName true}' has already been declared" | some declName => throwError "private declaration '{.ofConstName declName true}' has already been declared" if isReservedName env (privateToUserName declName) || isReservedName env (mkPrivateName (← getEnv) declName) then - throwError "'{declName}' is a reserved name" + throwError "'{.ofConstName declName}' is a reserved name" if env.contains (mkPrivateName env declName) then addInfo (mkPrivateName env declName) throwError "a private declaration '{.ofConstName declName true}' has already been declared" @@ -225,7 +225,7 @@ def checkIfShadowingStructureField (declName : Name) : m Unit := do let fieldNames := getStructureFieldsFlattened (← getEnv) pre for fieldName in fieldNames do if pre ++ fieldName == declName then - throwError "invalid declaration name '{declName}', structure '{pre}' has field '{fieldName}'" + throwError "invalid declaration name '{.ofConstName declName}', structure '{pre}' has field '{fieldName}'" | _ => pure () def mkDeclName (currNamespace : Name) (modifiers : Modifiers) (shortName : Name) : m (Name × Name) := do diff --git a/src/Lean/Elab/Deriving/Basic.lean b/src/Lean/Elab/Deriving/Basic.lean index f6d96443c8..d1125f35e1 100644 --- a/src/Lean/Elab/Deriving/Basic.lean +++ b/src/Lean/Elab/Deriving/Basic.lean @@ -168,7 +168,7 @@ def processDefDeriving (view : DerivingClassView) (decl : Expr) : TermElabM Unit -- and we make sure to put the instance in the private scope. withoutExporting (when := isPrivateName declName) do let ConstantInfo.defnInfo info ← getConstInfo declName - | throwError "Failed to delta derive instance, `{declName}` is not a definition." + | throwError "Failed to delta derive instance, `{.ofConstName declName}` is not a definition." let value := info.value.beta decl.getAppArgs let result : Closure.MkValueTypeClosureResult ← -- Assumption: users intend delta deriving to apply to the body of a definition, even if in the source code diff --git a/src/Lean/Elab/Deriving/Inhabited.lean b/src/Lean/Elab/Deriving/Inhabited.lean index 245f59376e..ad0ce03efd 100644 --- a/src/Lean/Elab/Deriving/Inhabited.lean +++ b/src/Lean/Elab/Deriving/Inhabited.lean @@ -121,7 +121,7 @@ private def mkInhabitedInstance (declName : Name) : CommandElabM Unit := do return true return false unless (← doIt false <||> doIt true) do - throwError "failed to generate 'Inhabited' instance for '{declName}'" + throwError "failed to generate 'Inhabited' instance for '{.ofConstName declName}'" def mkInhabitedInstanceHandler (declNames : Array Name) : CommandElabM Bool := do if (← declNames.allM isInductive) then diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean index cc66f79441..0830c00fff 100644 --- a/src/Lean/Elab/LetRec.lean +++ b/src/Lean/Elab/LetRec.lean @@ -53,7 +53,7 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do let declName := parentName?.getD Name.anonymous ++ shortDeclName if decls.any fun decl => decl.declName == declName then withRef declId do - throwError "'{declName}' has already been declared" + throwError "'{.ofConstName declName}' has already been declared" checkNotAlreadyDeclared declName applyAttributesAt declName attrs AttributeApplicationTime.beforeElaboration addDocString' declName docStr? diff --git a/src/Lean/Elab/PreDefinition/Eqns.lean b/src/Lean/Elab/PreDefinition/Eqns.lean index 4f05c4cfd4..16426ad7b3 100644 --- a/src/Lean/Elab/PreDefinition/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Eqns.lean @@ -394,7 +394,7 @@ private partial def mkEqnProof (declName : Name) (type : Expr) (tryRefl : Bool) else if let some mvarIds ← splitTarget? mvarId (useNewSemantics := true) then mvarIds.forM go else - throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}" + throwError "failed to generate equational theorem for '{.ofConstName declName}'\n{MessageData.ofGoal mvarId}" /-- @@ -408,7 +408,7 @@ This is currently used for non-recursive functions, well-founded recursion and p but not for structural recursion. -/ def mkEqns (declName : Name) (declNames : Array Name) (tryRefl := true): MetaM (Array Name) := do - trace[Elab.definition.eqns] "mkEqns: {declName}" + trace[Elab.definition.eqns] "mkEqns: {.ofConstName declName}" let info ← getConstInfoDefn declName let us := info.levelParams.map mkLevelParam withOptions (tactic.hygienic.set · false) do @@ -449,7 +449,7 @@ where until one of the equational theorems is applicable. -/ partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do - let some eqs ← getEqnsFor? declName | throwError "failed to generate equations for '{declName}'" + let some eqs ← getEqnsFor? declName | throwError "failed to generate equations for '{.ofConstName declName}'" let tryEqns (mvarId : MVarId) : MetaM Bool := eqs.anyM fun eq => commitWhen do checkpointDefEq (mayPostpone := false) do try @@ -475,7 +475,7 @@ partial def mkUnfoldProof (declName : Name) (mvarId : MVarId) : MetaM Unit := do if (← tryContradiction mvarId) then return () - throwError "failed to generate unfold theorem for '{declName}'\n{MessageData.ofGoal mvarId}" + throwError "failed to generate unfold theorem for '{.ofConstName declName}'\n{MessageData.ofGoal mvarId}" go mvarId builtin_initialize diff --git a/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean b/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean index df982e059c..be53af89f8 100644 --- a/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/PartialFixpoint/Eqns.lean @@ -99,7 +99,7 @@ where trace[Elab.definition.partialFixpoint] "mkUnfoldEq rfl succeeded" instantiateMVars goal catch e => - throwError "failed to generate unfold theorem for '{declName}':\n{e.toMessageData}" + throwError "failed to generate unfold theorem for '{.ofConstName declName}':\n{e.toMessageData}" let type ← mkForallFVars xs type let type ← letToHave type let value ← mkLambdaFVars xs goal diff --git a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean index 339679d79d..50dacf91bb 100644 --- a/src/Lean/Elab/PreDefinition/Structural/Eqns.lean +++ b/src/Lean/Elab/PreDefinition/Structural/Eqns.lean @@ -74,7 +74,7 @@ where trace[Elab.definition.structural.eqns] "splitTarget? succeeded" mvarIds.forM go else - throwError "failed to generate equational theorem for '{declName}'\n{MessageData.ofGoal mvarId}" + throwError "failed to generate equational theorem for '{.ofConstName declName}'\n{MessageData.ofGoal mvarId}" def mkEqns (info : EqnInfo) : MetaM (Array Name) := withOptions (tactic.hygienic.set · false) do diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Enums.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Enums.lean index 86895de02d..05fcd2f71d 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Enums.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Enums.lean @@ -52,9 +52,9 @@ def getEnumToBitVecFor (declName : Name) : MetaM Name := do let enumToBitVecName := Name.str declName enumToBitVecSuffix realizeConst declName enumToBitVecName do let env ← getEnv - let .inductInfo inductiveInfo ← getConstInfo declName | throwError m!"{declName} is not an inductive." + let .inductInfo inductiveInfo ← getConstInfo declName | throwError m!"{.ofConstName declName} is not an inductive." if !(← isEnumType declName) then - throwError m!"{declName} is not an enum inductive." + throwError m!"{.ofConstName declName} is not an enum inductive." let domainSize := inductiveInfo.ctors.length let bvSize := getBitVecSize domainSize let bvType := mkApp (mkConst ``BitVec) (toExpr bvSize) @@ -348,7 +348,7 @@ def getMatchEqCondFor (declName : Name) : MetaM Name := do if let some kind ← isSupportedMatch declName then return (← getMatchEqCondForAux declName kind) else - throwError m!"{matchEqCondSuffix} lemma could not be established for {declName}" + throwError m!"{matchEqCondSuffix} lemma could not be established for {.ofConstName declName}" builtin_initialize registerReservedNamePredicate fun env name => Id.run do diff --git a/src/Lean/Elab/Tactic/Rewrite.lean b/src/Lean/Elab/Tactic/Rewrite.lean index 6c191520f6..f0a4ca1358 100644 --- a/src/Lean/Elab/Tactic/Rewrite.lean +++ b/src/Lean/Elab/Tactic/Rewrite.lean @@ -65,7 +65,7 @@ def withRWRulesSeq (token : Syntax) (rwRulesSeqStx : Syntax) (x : (symm : Bool) let hint := if eqThms.size = 1 then m!"" else .hint' m!"Try rewriting with `{Name.str declName unfoldThmSuffix}`" let rec go : List Name → TacticM Unit - | [] => throwError m!"Failed to rewrite using equation theorems for `{declName}`" ++ hint + | [] => throwError m!"Failed to rewrite using equation theorems for `{.ofConstName declName}`" ++ hint | eqThm::eqThms => (x symm (mkCIdentFrom id eqThm)) <|> go eqThms discard <| Term.addTermInfo id (← mkConstWithFreshMVarLevels declName) (lctx? := ← getLCtx) go eqThms.toList diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index 405a310aa2..5afca13d3b 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -178,9 +178,9 @@ private def elabDeclToUnfoldOrTheorem (config : Meta.ConfigWithKey) (id : Origin return .addEntries <| thms.map (SimpEntry.thm ·) else if inv then - throwError m!"Invalid `←` modifier: `{declName}` is a declaration name to be unfolded" + throwError m!"Invalid `←` modifier: `{.ofConstName declName}` is a declaration name to be unfolded" ++ .hint' m!"The simplifier cannot \"refold\" definitions by name. Use `rw` for this instead, - or use the `←` simp modifier with an equational lemma for `{declName}`." + or use the `←` simp modifier with an equational lemma for `{.ofConstName declName}`." if kind == .dsimp then return .addEntries #[.toUnfold declName] else diff --git a/src/Lean/KeyedDeclsAttribute.lean b/src/Lean/KeyedDeclsAttribute.lean index d6e8c8b1e8..4d1a443ce2 100644 --- a/src/Lean/KeyedDeclsAttribute.lean +++ b/src/Lean/KeyedDeclsAttribute.lean @@ -105,7 +105,7 @@ def mkStateOfTable (table : Table γ) : ExtensionState γ := { def ExtensionState.erase (s : ExtensionState γ) (attrName : Name) (declName : Name) : CoreM (ExtensionState γ) := do unless s.declNames.contains declName do - throwError "Cannot erase attribute `{attrName}`: `{declName}` does not have this attribute" + throwError "Cannot erase attribute `{attrName}`: `{.ofConstName declName}` does not have this attribute" return { s with erased := s.erased.insert declName, declNames := s.declNames.erase declName } protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name := by exact decl_name%) : IO (KeyedDeclsAttribute γ) := do diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean index 1e87555f4a..d749c13643 100644 --- a/src/Lean/Meta/Instances.lean +++ b/src/Lean/Meta/Instances.lean @@ -87,7 +87,7 @@ def Instances.eraseCore (d : Instances) (declName : Name) : Instances := def Instances.erase [Monad m] [MonadError m] (d : Instances) (declName : Name) : m Instances := do unless d.instanceNames.contains declName do - throwError "'{declName}' does not have [instance] attribute" + throwError "'{.ofConstName declName}' does not have [instance] attribute" return d.eraseCore declName builtin_initialize instanceExtension : SimpleScopedEnvExtension InstanceEntry Instances ← @@ -311,15 +311,15 @@ builtin_initialize defaultInstanceExtension : SimplePersistentEnvExtension Defau def addDefaultInstance (declName : Name) (prio : Nat := 0) : MetaM Unit := do match (← getEnv).find? declName with - | none => throwError "Unknown constant `{declName}`" + | none => throwError "Unknown constant `{.ofConstName declName}`" | some info => forallTelescopeReducing info.type fun _ type => do match type.getAppFn with | Expr.const className _ => unless isClass (← getEnv) className do - throwError "invalid default instance '{declName}', it has type '({className} ...)', but {className}' is not a type class" + throwError "invalid default instance '{.ofConstName declName}', it has type '({className} ...)', but {className}' is not a type class" setEnv <| defaultInstanceExtension.addEntry (← getEnv) { className := className, instanceName := declName, priority := prio } - | _ => throwError "invalid default instance '{declName}', type must be of the form '(C ...)' where 'C' is a type class" + | _ => throwError "invalid default instance '{.ofConstName declName}', type must be of the form '(C ...)' where 'C' is a type class" builtin_initialize registerBuiltinAttribute { diff --git a/src/Lean/Meta/Match/MatchPatternAttr.lean b/src/Lean/Meta/Match/MatchPatternAttr.lean index a9d856e350..b216a5c764 100644 --- a/src/Lean/Meta/Match/MatchPatternAttr.lean +++ b/src/Lean/Meta/Match/MatchPatternAttr.lean @@ -36,7 +36,7 @@ builtin_initialize matchPatternAttr : TagAttribute ← (validate := fun declName => do withExporting (isExporting := !isPrivateName declName) do if !(← getConstInfo declName).isDefinition then - throwError "invalid `@[match_pattern]` attribute, '{declName}' is not an exposed definition") + throwError "invalid `@[match_pattern]` attribute, '{.ofConstName declName}' is not an exposed definition") @[export lean_has_match_pattern_attribute] def hasMatchPatternAttribute (env : Environment) (n : Name) : Bool := diff --git a/src/Lean/Meta/RecursorInfo.lean b/src/Lean/Meta/RecursorInfo.lean index 06a5f2648e..be0b09b924 100644 --- a/src/Lean/Meta/RecursorInfo.lean +++ b/src/Lean/Meta/RecursorInfo.lean @@ -87,7 +87,7 @@ private def getMajorPosIfAuxRecursor? (declName : Name) (majorPos? : Option Nat) private def checkMotive (declName : Name) (motive : Expr) (motiveArgs : Array Expr) : MetaM Unit := unless motive.isFVar && motiveArgs.all Expr.isFVar do - throwError "invalid user defined recursor '{declName}', result type must be of the form (C t), where C is a bound variable, and t is a (possibly empty) sequence of bound variables" + throwError "invalid user defined recursor '{.ofConstName declName}', result type must be of the form (C t), where C is a bound variable, and t is a (possibly empty) sequence of bound variables" /-- Compute number of parameters for (user-defined) recursor. We assume a parameter is anything that occurs before the motive -/ @@ -109,11 +109,11 @@ private def getMajorPosDepElim (declName : Name) (majorPos? : Option Nat) (xs : else throwError "invalid major premise position for user defined recursor, recursor has only {xs.size} arguments" | none => do if motiveArgs.isEmpty then - throwError "invalid user defined recursor, '{declName}' does not support dependent elimination, and position of the major premise was not specified (solution: set attribute '[recursor ]', where is the position of the major premise)" + throwError "invalid user defined recursor, '{.ofConstName declName}' does not support dependent elimination, and position of the major premise was not specified (solution: set attribute '[recursor ]', where is the position of the major premise)" let major := motiveArgs.back! match xs.idxOf? major with | some majorPos => pure (major, majorPos, true) - | none => throwError "ill-formed recursor '{declName}'" + | none => throwError "ill-formed recursor '{.ofConstName declName}'" private def getParamsPos (declName : Name) (xs : Array Expr) (numParams : Nat) (Iargs : Array Expr) : MetaM (List (Option Nat)) := do let mut paramsPos := #[] @@ -126,7 +126,7 @@ private def getParamsPos (declName : Name) (xs : Array Expr) (numParams : Nat) ( if localDecl.binderInfo.isInstImplicit then paramsPos := paramsPos.push none else - throwError"invalid user defined recursor '{declName}', type of the major premise does not contain the recursor parameter" + throwError"invalid user defined recursor '{.ofConstName declName}', type of the major premise does not contain the recursor parameter" pure paramsPos.toList private def getIndicesPos (declName : Name) (xs : Array Expr) (majorPos numIndices : Nat) (Iargs : Array Expr) : MetaM (List Nat) := do @@ -136,7 +136,7 @@ private def getIndicesPos (declName : Name) (xs : Array Expr) (majorPos numIndic let x := xs[i]! match (← Iargs.findIdxM? fun Iarg => isDefEq Iarg x) with | some j => indicesPos := indicesPos.push j - | none => throwError "invalid user defined recursor '{declName}', type of the major premise does not contain the recursor index" + | none => throwError "invalid user defined recursor '{.ofConstName declName}', type of the major premise does not contain the recursor index" pure indicesPos.toList private def getMotiveLevel (declName : Name) (motiveResultType : Expr) : MetaM Level := @@ -144,7 +144,7 @@ private def getMotiveLevel (declName : Name) (motiveResultType : Expr) : MetaM L | Expr.sort u@(Level.zero) => pure u | Expr.sort u@(Level.param _) => pure u | _ => - throwError "invalid user defined recursor '{declName}', motive result sort must be Prop or (Sort u) where u is a universe level parameter" + throwError "invalid user defined recursor '{.ofConstName declName}', motive result sort must be Prop or (Sort u) where u is a universe level parameter" private def getUnivLevelPos (declName : Name) (lparams : List Name) (motiveLvl : Level) (Ilevels : List Level) : MetaM (List RecursorUnivLevelPos) := do let Ilevels := Ilevels.toArray @@ -156,7 +156,7 @@ private def getUnivLevelPos (declName : Name) (lparams : List Name) (motiveLvl : match Ilevels.findIdx? fun u => u == mkLevelParam p with | some i => univLevelPos := univLevelPos.push (RecursorUnivLevelPos.majorType i) | none => - throwError "invalid user defined recursor '{declName}', major premise type does not contain universe level parameter '{p}'" + throwError "invalid user defined recursor '{.ofConstName declName}', major premise type does not contain universe level parameter '{p}'" pure univLevelPos.toList private def getProduceMotiveAndRecursive (xs : Array Expr) (numParams numIndices majorPos : Nat) (motive : Expr) : MetaM (List Bool × Bool) := do @@ -180,7 +180,7 @@ private def getProduceMotiveAndRecursive (xs : Array Expr) (numParams numIndices private def checkMotiveResultType (declName : Name) (motiveArgs : Array Expr) (motiveResultType : Expr) (motiveTypeParams : Array Expr) : MetaM Unit := do if !motiveResultType.isSort || motiveArgs.size != motiveTypeParams.size then - throwError "invalid user defined recursor '{declName}', motive must have a type of the form (C : Pi (i : B A), I A i -> Type), where A is (possibly empty) sequence of variables (aka parameters), (i : B A) is a (possibly empty) telescope (aka indices), and I is a constant" + throwError "invalid user defined recursor '{.ofConstName declName}', motive must have a type of the form (C : Pi (i : B A), I A i -> Type), where A is (possibly empty) sequence of variables (aka parameters), (i : B A) is a (possibly empty) telescope (aka indices), and I is a constant" private def mkRecursorInfoCore (declName : Name) (majorPos? : Option Nat) : MetaM RecursorInfo := do let cinfo ← getConstInfo declName @@ -191,7 +191,7 @@ private def mkRecursorInfoCore (declName : Name) (majorPos? : Option Nat) : Meta let (major, majorPos, depElim) ← getMajorPosDepElim declName majorPos? xs motiveArgs let numIndices := if depElim then motiveArgs.size - 1 else motiveArgs.size if majorPos < numIndices then - throwError "invalid user defined recursor '{declName}', indices must occur before major premise" + throwError "invalid user defined recursor '{.ofConstName declName}', indices must occur before major premise" let majorType ← inferType major majorType.withApp fun I Iargs => match I with @@ -216,7 +216,7 @@ private def mkRecursorInfoCore (declName : Name) (majorPos? : Option Nat) : Meta indicesPos := indicesPos, numArgs := xs.size } - | _ => throwError "invalid user defined recursor '{declName}', type of the major premise must be of the form (I ...), where I is a constant" + | _ => throwError "invalid user defined recursor '{.ofConstName declName}', type of the major premise must be of the form (I ...), where I is a constant" /- @[builtin_attr_parser] def «recursor» := leading_parser "recursor " >> numLit diff --git a/src/Lean/Meta/Structure.lean b/src/Lean/Meta/Structure.lean index a025ce82b5..d650de0a10 100644 --- a/src/Lean/Meta/Structure.lean +++ b/src/Lean/Meta/Structure.lean @@ -26,7 +26,7 @@ def getStructureName (struct : Expr) : MetaM Name := match struct.getAppFn with | Expr.const declName .. => do unless isStructure (← getEnv) declName do - throwError "'{declName}' is not a structure" + throwError "'{.ofConstName declName}' is not a structure" return declName | _ => throwError "expected structure" diff --git a/src/Lean/Meta/Tactic/Ext.lean b/src/Lean/Meta/Tactic/Ext.lean index 86c0688cb9..028fc61bcb 100644 --- a/src/Lean/Meta/Tactic/Ext.lean +++ b/src/Lean/Meta/Tactic/Ext.lean @@ -83,7 +83,7 @@ found somewhere in the state's tree, and is not erased. def ExtTheorems.erase [Monad m] [MonadError m] (d : ExtTheorems) (declName : Name) : m ExtTheorems := do unless d.contains declName do - throwError "Cannot erase `[ext]` attribute from `{declName}`: It does not have this attribute" + throwError "Cannot erase `[ext]` attribute from `{.ofConstName declName}`: It does not have this attribute" return d.eraseCore declName end Lean.Meta.Ext diff --git a/src/Lean/Meta/Tactic/Simp/Attr.lean b/src/Lean/Meta/Tactic/Simp/Attr.lean index 05a28ece77..9ef3668bd9 100644 --- a/src/Lean/Meta/Tactic/Simp/Attr.lean +++ b/src/Lean/Meta/Tactic/Simp/Attr.lean @@ -36,7 +36,7 @@ def mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension) addSimpTheorem ext declName post (inv := inv) attrKind prio else if info.kind matches .defn then if inv then - throwError m!"Invalid `←` modifier: `{declName}` is a declaration name to be unfolded" + throwError m!"Invalid `←` modifier: `{.ofConstName declName}` is a declaration name to be unfolded" ++ .note m!"The simplifier will automatically unfold definitions marked with the `[simp]` \ attribute, but it will not \"refold\" them" if (← Simp.ignoreEquations declName) then @@ -50,7 +50,7 @@ def mkSimpAttr (attrName : Name) (attrDescr : String) (ext : SimpExtension) else ext.add (SimpEntry.toUnfold declName) attrKind else - throwError m!"Cannot add `simp` attribute to `{declName}`: It is not a proposition nor a definition (to unfold)" + throwError m!"Cannot add `simp` attribute to `{.ofConstName declName}`: It is not a proposition nor a definition (to unfold)" ++ .note m!"The `[simp]` attribute can be added to lemmas that should be automatically used by the simplifier \ and to definitions that the simplifier should automatically unfold" discard <| go.run {} {} diff --git a/src/Lean/Meta/Tactic/Simp/Simproc.lean b/src/Lean/Meta/Tactic/Simp/Simproc.lean index 413059e04f..aef95a7161 100644 --- a/src/Lean/Meta/Tactic/Simp/Simproc.lean +++ b/src/Lean/Meta/Tactic/Simp/Simproc.lean @@ -87,7 +87,7 @@ def registerBuiltinSimprocCore (declName : Name) (key : Array SimpTheoremKey) (p unless (← initializing) do throw (IO.userError s!"Invalid builtin simproc declaration: It can only be registered during initialization") if (← builtinSimprocDeclsRef.get).keys.contains declName then - throw (IO.userError s!"Invalid builtin simproc declaration `{declName}`: This builtin simproc has already been declared") + throw (IO.userError s!"Invalid builtin simproc declaration `{privateToUserName declName}`: This builtin simproc has already been declared") builtinSimprocDeclsRef.modify fun { keys, procs } => { keys := keys.insert declName key, procs := procs.insert declName proc } @@ -100,9 +100,9 @@ def registerBuiltinDSimproc (declName : Name) (key : Array SimpTheoremKey) (proc def registerSimproc (declName : Name) (keys : Array SimpTheoremKey) : CoreM Unit := do let env ← getEnv unless (env.getModuleIdxFor? declName).isNone do - throwError "Invalid simproc declaration `{declName}`: This function is declared in an imported module" + throwError "Invalid simproc declaration `{.ofConstName declName}`: This function is declared in an imported module" if (← isSimproc declName) then - throwError "Invalid simproc declaration `{declName}`: This simproc has already been declared" + throwError "Invalid simproc declaration `{.ofConstName declName}`: This simproc has already been declared" modifyEnv fun env => simprocDeclExt.modifyState env fun s => { s with newEntries := s.newEntries.insert declName keys } instance : BEq SimprocEntry where @@ -132,7 +132,7 @@ unsafe def getSimprocFromDeclImpl (declName : Name) : ImportM (Sum Simproc DSimp return .inl (← IO.ofExcept <| ctx.env.evalConst Simproc ctx.opts declName) | .const ``DSimproc _ => return .inr (← IO.ofExcept <| ctx.env.evalConst DSimproc ctx.opts declName) - | _ => throw <| IO.userError s!"Simproc `{declName}` has an unexpected type: Expected `Simproc` or `DSimproc`, but found `{info.type}`" + | _ => throw <| IO.userError s!"Simproc `{privateToUserName declName}` has an unexpected type: Expected `Simproc` or `DSimproc`, but found `{info.type}`" @[implemented_by getSimprocFromDeclImpl] opaque getSimprocFromDecl (declName: Name) : ImportM (Sum Simproc DSimproc) @@ -143,13 +143,13 @@ def toSimprocEntry (e : SimprocOLeanEntry) : ImportM SimprocEntry := do def eraseSimprocAttr (ext : SimprocExtension) (declName : Name) : AttrM Unit := do let s := ext.getState (← getEnv) unless s.simprocNames.contains declName do - throwError "`{declName}` does not have a [simproc] attribute" + throwError "`{.ofConstName declName}` does not have a [simproc] attribute" modifyEnv fun env => ext.modifyState env fun s => s.erase declName def addSimprocAttrCore (ext : SimprocExtension) (declName : Name) (kind : AttributeKind) (post : Bool) : CoreM Unit := do let proc ← getSimprocFromDecl declName let some keys ← getSimprocDeclKeys? declName | - throwError "Invalid `[simproc]` attribute: `{declName}` is not a simproc" + throwError "Invalid `[simproc]` attribute: `{.ofConstName declName}` is not a simproc" ext.add { declName, post, keys, proc } kind def Simprocs.addCore (s : Simprocs) (keys : Array SimpTheoremKey) (declName : Name) (post : Bool) (proc : Sum Simproc DSimproc) : Simprocs := @@ -164,7 +164,7 @@ Implements attributes `builtin_simproc` and `builtin_sevalproc`. -/ def addSimprocBuiltinAttrCore (ref : IO.Ref Simprocs) (declName : Name) (post : Bool) (proc : Sum Simproc DSimproc) : IO Unit := do let some keys := (← builtinSimprocDeclsRef.get).keys[declName]? | - throw (IO.userError s!"Invalid `[builtin_simproc]` attribute: `{declName}` is not a builtin simproc") + throw (IO.userError s!"Invalid `[builtin_simproc]` attribute: `{privateToUserName declName}` is not a builtin simproc") ref.modify fun s => s.addCore keys declName post proc def addSimprocBuiltinAttr (declName : Name) (post : Bool) (proc : Sum Simproc DSimproc) : IO Unit := @@ -180,12 +180,12 @@ def Simprocs.add (s : Simprocs) (declName : Name) (post : Bool) : CoreM Simprocs catch e => if (← isBuiltinSimproc declName) then let some proc := (← builtinSimprocDeclsRef.get).procs[declName]? - | throwError "Invalid `[simproc]` attribute: `{declName}` is not a simproc" + | throwError "Invalid `[simproc]` attribute: `{.ofConstName declName}` is not a simproc" pure proc else throw e let some keys ← getSimprocDeclKeys? declName | - throwError "Invalid `[simproc]` attribute: `{declName}` is not a simproc" + throwError "Invalid `[simproc]` attribute: `{.ofConstName declName}` is not a simproc" return s.addCore keys declName post proc def SimprocEntry.try (s : SimprocEntry) (numExtraArgs : Nat) (e : Expr) : SimpM Step := do @@ -409,7 +409,7 @@ private def addBuiltin (declName : Name) (stx : Syntax) (addDeclName : Name) : A | .const ``Simproc _ => pure <| mkApp3 (mkConst ``Sum.inl [0, 0]) (mkConst ``Simproc) (mkConst ``DSimproc) (mkConst declName) | .const ``DSimproc _ => pure <| mkApp3 (mkConst ``Sum.inr [0, 0]) (mkConst ``Simproc) (mkConst ``DSimproc) (mkConst declName) | tp => throwError "Unexpected simproc type: Expected {.ofConstName ``Lean.Meta.Simp.Simproc} or {.ofConstName ``Lean.Meta.Simp.DSimproc}, \ - but `{declName}` has type{indentExpr tp}" + but `{.ofConstName declName}` has type{indentExpr tp}" let val := mkAppN (mkConst addDeclName) #[toExpr declName, toExpr post, procExpr] let initDeclName ← mkFreshUserName (declName ++ `declare) declareBuiltin initDeclName val diff --git a/src/Lean/Meta/Tactic/Unfold.lean b/src/Lean/Meta/Tactic/Unfold.lean index 061e947208..ecbc9f695e 100644 --- a/src/Lean/Meta/Tactic/Unfold.lean +++ b/src/Lean/Meta/Tactic/Unfold.lean @@ -36,13 +36,13 @@ where def unfoldTarget (mvarId : MVarId) (declName : Name) : MetaM MVarId := mvarId.withContext do let target ← instantiateMVars (← mvarId.getType) let r ← unfold target declName - if r.expr == target then throwError "Tactic `unfold` failed to unfold `{declName}` in{indentExpr target}" + if r.expr == target then throwError "Tactic `unfold` failed to unfold `{.ofConstName declName}` in{indentExpr target}" applySimpResultToTarget mvarId target r def unfoldLocalDecl (mvarId : MVarId) (fvarId : FVarId) (declName : Name) : MetaM MVarId := mvarId.withContext do let type ← fvarId.getType let r ← unfold (← instantiateMVars type) declName - if r.expr == type then throwError "Tactic `unfold` failed to unfold `{declName}` in{indentExpr type}" + if r.expr == type then throwError "Tactic `unfold` failed to unfold `{.ofConstName declName}` in{indentExpr type}" let some (_, mvarId) ← applySimpResultToLocalDecl mvarId fvarId r (mayCloseGoal := false) | unreachable! return mvarId diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 2a5dadbefb..65b2de5daf 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -8,6 +8,7 @@ module prelude public import Lean.Parser.Basic public import Lean.ScopedEnvExtension +import Lean.PrivateName import Lean.BuiltinDocAttr public section @@ -153,7 +154,7 @@ private def updateBuiltinTokens (info : ParserInfo) (declName : Name) : IO Unit let tokenTable ← builtinTokenTable.swap {} match addParserTokens tokenTable info with | Except.ok tokenTable => builtinTokenTable.set tokenTable - | Except.error msg => throw (IO.userError s!"invalid builtin parser '{declName}', {msg}") + | Except.error msg => throw (IO.userError s!"invalid builtin parser `{privateToUserName declName}`, {msg}") def ParserExtension.addEntryImpl (s : State) (e : Entry) : State := match e with @@ -509,7 +510,7 @@ private def BuiltinParserAttribute.add (attrName : Name) (catName : Name) | Expr.const `Lean.Parser.Parser _ => declareLeadingBuiltinParser catName declName prio | _ => throwError "Unexpected type for parser declaration: Parsers must have type `Parser` or \ - `TrailingParser`, but `{declName}` has type{indentExpr decl.type}" + `TrailingParser`, but `{.ofConstName declName}` has type{indentExpr decl.type}" declareBuiltinDocStringAndRanges declName runParserAttributeHooks catName declName (builtin := true) @@ -542,7 +543,7 @@ private def ParserAttribute.add (_attrName : Name) (catName : Name) (declName : try addToken token attrKind catch - | Exception.error _ msg => throwError "invalid parser '{declName}', {msg}" + | Exception.error _ msg => throwError "invalid parser '{.ofConstName declName}', {msg}" | ex => throw ex let kinds := parser.info.collectKinds {} kinds.forM fun kind _ => modifyEnv fun env => addSyntaxNodeKind env kind diff --git a/src/Lean/Parser/Tactic/Doc.lean b/src/Lean/Parser/Tactic/Doc.lean index bb849b149c..3ea103887c 100644 --- a/src/Lean/Parser/Tactic/Doc.lean +++ b/src/Lean/Parser/Tactic/Doc.lean @@ -283,12 +283,12 @@ def tacticDocsOnTactics : ParserAttributeHook where if catName == `tactic then return if alternativeOfTactic (← getEnv) declName |>.isSome then - throwError m!"`{declName}` is not a tactic" + throwError m!"`{.ofConstName declName}` is not a tactic" -- It's sufficient to look in the state (and not the imported entries) because this validation -- only needs to check tags added in the current module if let some tags := tacticTagExt.getState (← getEnv) |>.find? declName then if !tags.isEmpty then - throwError m!"`{declName}` is not a tactic" + throwError m!"`{.ofConstName declName}` is not a tactic" builtin_initialize registerParserAttributeHook tacticDocsOnTactics diff --git a/src/Lean/ReducibilityAttrs.lean b/src/Lean/ReducibilityAttrs.lean index a16b35d41e..7d5b190499 100644 --- a/src/Lean/ReducibilityAttrs.lean +++ b/src/Lean/ReducibilityAttrs.lean @@ -108,30 +108,30 @@ private def validate (declName : Name) (status : ReducibilityStatus) (attrKind : let statusOld := getReducibilityStatusCore (← getEnv) declName match attrKind with | .scoped => - throwError "failed to set reducibility status for `{declName}`, the `scoped` modifier is not recommended for this kind of attribute{suffix}" + throwError "failed to set reducibility status for `{.ofConstName declName}`, the `scoped` modifier is not recommended for this kind of attribute{suffix}" | .global => if (← getEnv).getModuleIdxFor? declName matches some _ then - throwError "failed to set reducibility status, `{declName}` has not been defined in this file, consider using the `local` modifier{suffix}" + throwError "failed to set reducibility status, `{.ofConstName declName}` has not been defined in this file, consider using the `local` modifier{suffix}" match status with | .reducible => unless statusOld matches .semireducible do - throwError "failed to set `[reducible]`, `{declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}" + throwError "failed to set `[reducible]`, `{.ofConstName declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}" | .irreducible => unless statusOld matches .semireducible do - throwError "failed to set `[irreducible]`, `{declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}" + throwError "failed to set `[irreducible]`, `{.ofConstName declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}" | .semireducible => - throwError "failed to set `[semireducible]` for `{declName}`, declarations are `[semireducible]` by default{suffix}" + throwError "failed to set `[semireducible]` for `{.ofConstName declName}`, declarations are `[semireducible]` by default{suffix}" | .local => match status with | .reducible => - throwError "failed to set `[local reducible]` for `{declName}`, recall that `[reducible]` affects the term indexing datastructures used by `simp` and type class resolution{suffix}" + throwError "failed to set `[local reducible]` for `{.ofConstName declName}`, recall that `[reducible]` affects the term indexing datastructures used by `simp` and type class resolution{suffix}" | .irreducible => unless statusOld matches .semireducible do - throwError "failed to set `[local irreducible]`, `{declName}` is currently `{statusOld.toAttrString}`, `[semireducible]` expected{suffix}" + throwError "failed to set `[local irreducible]`, `{.ofConstName declName}` is currently `{statusOld.toAttrString}`, `[semireducible]` expected{suffix}" | .semireducible => unless statusOld matches .irreducible do - throwError "failed to set `[local semireducible]`, `{declName}` is currently `{statusOld.toAttrString}`, `[irreducible]` expected{suffix}" - | _ => throwError "failed to set reducibility status, `{declName}` is not a definition{suffix}" + throwError "failed to set `[local semireducible]`, `{.ofConstName declName}` is currently `{statusOld.toAttrString}`, `[irreducible]` expected{suffix}" + | _ => throwError "failed to set reducibility status, `{.ofConstName declName}` is not a definition{suffix}" private def addAttr (status : ReducibilityStatus) (declName : Name) (stx : Syntax) (attrKind : AttributeKind) : AttrM Unit := do Attribute.Builtin.ensureNoArgs stx diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean index f03224002f..475b826537 100644 --- a/src/Lean/ResolveName.lean +++ b/src/Lean/ResolveName.lean @@ -25,7 +25,7 @@ For example, give a definition `foo`, we flag `foo.def` as reserved symbol. -/ def throwReservedNameNotAvailable [Monad m] [MonadError m] (declName : Name) (reservedName : Name) : m Unit := do - throwError "failed to declare `{declName}` because `{.ofConstName reservedName true}` has already been declared" + throwError "failed to declare `{.ofConstName declName}` because `{.ofConstName reservedName true}` has already been declared" def ensureReservedNameAvailable [Monad m] [MonadEnv m] [MonadError m] (declName : Name) (suffix : String) : m Unit := do let reservedName := .str declName suffix diff --git a/tests/lean/implementedByIssue.lean.expected.out b/tests/lean/implementedByIssue.lean.expected.out index 9a2a0a599b..5a3ca41aa8 100644 --- a/tests/lean/implementedByIssue.lean.expected.out +++ b/tests/lean/implementedByIssue.lean.expected.out @@ -1,5 +1,5 @@ -implementedByIssue.lean:15:11-15:31: error: Invalid `implemented_by` argument `Hidden.get_2`: `Hidden.get_2` has 0 universe level parameter(s), but `Hidden.Array.data` has 1 +implementedByIssue.lean:15:11-15:31: error: Invalid `implemented_by` argument `Hidden.get_2`: `Hidden.get_2` has 0 universe level parameter(s), but `Array.data` has 1 implementedByIssue.lean:19:11-19:31: error: Invalid `implemented_by` argument `Hidden.get_3`: `Hidden.get_3` has type {α : Type u} → {n : Nat} → Fin n → Array α n → α -but `Hidden.Array.data` has type +but `Array.data` has type {α : Type u} → {n : Nat} → Array α n → Fin n → α