From 95d3b4b58f4f2e2b65951a537ab46618031341a6 Mon Sep 17 00:00:00 2001 From: Kyle Miller Date: Tue, 29 Oct 2024 14:23:51 -0700 Subject: [PATCH] chore: move `MessageData.ofConstName` earlier (#5877) Makes `MessageData.ofConstName` available without needing to import the pretty printer. Any code making use of `MessageData` can write `m!" ... {.ofConstName n} ... "` to have the name print with hover information. More error messages now have hover information. * Now `.ofConstName` also has a boolean flag to make names print fully qualified. Default: false. * Now `.ofConstName` will sanitize names that aren't constants. It is OK to use it in `"unknown constant '{.ofConstName constName}'"` errors. Usability note: it is more user-friendly to have "has already been declared" errors report the fully qualified name. For this, write `m!"{.ofConstName n true} has already been declared"`. --- src/Lean/Class.lean | 12 +++++------ src/Lean/Elab/DeclModifiers.lean | 8 +++---- src/Lean/Elab/Deriving/TypeName.lean | 2 +- src/Lean/Elab/Print.lean | 2 +- src/Lean/Elab/Structure.lean | 10 ++++----- src/Lean/Exception.lean | 6 +++--- src/Lean/Message.lean | 31 ++++++++++++++++++++++++---- src/Lean/Meta/Match/Basic.lean | 2 +- src/Lean/Meta/Tactic/Simp/Main.lean | 2 +- src/Lean/Meta/Tactic/UnifyEq.lean | 2 +- src/Lean/MonadEnv.lean | 10 ++++----- src/Lean/PrettyPrinter.lean | 31 ++++++++++++++-------------- src/Lean/ResolveName.lean | 2 +- src/Lean/Util/PPExt.lean | 5 +++++ src/Lean/Widget/UserWidget.lean | 2 +- src/lake/Lake/DSL/DeclUtil.lean | 2 +- 16 files changed, 78 insertions(+), 51 deletions(-) diff --git a/src/Lean/Class.lean b/src/Lean/Class.lean index f26c478fbd96..e591e7805d25 100644 --- a/src/Lean/Class.lean +++ b/src/Lean/Class.lean @@ -87,7 +87,7 @@ def hasOutParams (env : Environment) (declName : Name) : Bool := incorrect. This transformation would be counterintuitive to users since we would implicitly treat these regular parameters as `outParam`s. -/ -private partial def checkOutParam (i : Nat) (outParamFVarIds : Array FVarId) (outParams : Array Nat) (type : Expr) : Except String (Array Nat) := +private partial def checkOutParam (i : Nat) (outParamFVarIds : Array FVarId) (outParams : Array Nat) (type : Expr) : Except MessageData (Array Nat) := match type with | .forallE _ d b bi => let addOutParam (_ : Unit) := @@ -102,7 +102,7 @@ private partial def checkOutParam (i : Nat) (outParamFVarIds : Array FVarId) (ou /- See issue #1852 for a motivation for `bi.isInstImplicit` -/ addOutParam () else - Except.error s!"invalid class, parameter #{i+1} depends on `outParam`, but it is not an `outParam`" + Except.error m!"invalid class, parameter #{i+1} depends on `outParam`, but it is not an `outParam`" else checkOutParam (i+1) outParamFVarIds outParams b | _ => return outParams @@ -149,13 +149,13 @@ and it must be the name of constant in `env`. `declName` must be a inductive datatype or axiom. Recall that all structures are inductive datatypes. -/ -def addClass (env : Environment) (clsName : Name) : Except String Environment := do +def addClass (env : Environment) (clsName : Name) : Except MessageData Environment := do if isClass env clsName then - throw s!"class has already been declared '{clsName}'" + throw m!"class has already been declared '{.ofConstName clsName true}'" let some decl := env.find? clsName - | throw s!"unknown declaration '{clsName}'" + | throw m!"unknown declaration '{clsName}'" unless decl matches .inductInfo .. | .axiomInfo .. do - throw s!"invalid 'class', declaration '{clsName}' must be inductive datatype, structure, or constant" + throw m!"invalid 'class', declaration '{.ofConstName clsName}' must be inductive datatype, structure, or constant" let outParams ← checkOutParam 0 #[] #[] decl.type return classExtension.addEntry env { name := clsName, outParams } diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean index a6c86a04e744..043e41885377 100644 --- a/src/Lean/Elab/DeclModifiers.lean +++ b/src/Lean/Elab/DeclModifiers.lean @@ -25,19 +25,19 @@ def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadError m] [MonadInfo if env.contains declName then addInfo declName match privateToUserName? declName with - | none => throwError "'{declName}' has already been declared" - | some declName => throwError "private declaration '{declName}' has already been declared" + | none => throwError "'{.ofConstName declName true}' has already been declared" + | some declName => throwError "private declaration '{.ofConstName declName true}' has already been declared" if isReservedName env declName then throwError "'{declName}' is a reserved name" if env.contains (mkPrivateName env declName) then addInfo (mkPrivateName env declName) - throwError "a private declaration '{declName}' has already been declared" + throwError "a private declaration '{.ofConstName declName true}' has already been declared" match privateToUserName? declName with | none => pure () | some declName => if env.contains declName then addInfo declName - throwError "a non-private declaration '{declName}' has already been declared" + throwError "a non-private declaration '{.ofConstName declName true}' has already been declared" /-- Declaration visibility modifier. That is, whether a declaration is regular, protected or private. -/ inductive Visibility where diff --git a/src/Lean/Elab/Deriving/TypeName.lean b/src/Lean/Elab/Deriving/TypeName.lean index 671ddad1021b..09ec048de53f 100644 --- a/src/Lean/Elab/Deriving/TypeName.lean +++ b/src/Lean/Elab/Deriving/TypeName.lean @@ -14,7 +14,7 @@ private def deriveTypeNameInstance (declNames : Array Name) : CommandElabM Bool for declName in declNames do let cinfo ← getConstInfo declName unless cinfo.levelParams.isEmpty do - throwError m!"{mkConst declName} has universe level parameters" + throwError m!"{.ofConstName declName} has universe level parameters" elabCommand <| ← withFreshMacroScope `( unsafe def instImpl : TypeName @$(mkCIdent declName) := .mk _ $(quote declName) @[implemented_by instImpl] opaque inst : TypeName @$(mkCIdent declName) diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean index 531f0e1ed616..a895c7dc04db 100644 --- a/src/Lean/Elab/Print.lean +++ b/src/Lean/Elab/Print.lean @@ -11,7 +11,7 @@ import Lean.Elab.Command namespace Lean.Elab.Command private def throwUnknownId (id : Name) : CommandElabM Unit := - throwError "unknown identifier '{mkConst id}'" + throwError "unknown identifier '{.ofConstName id}'" private def levelParamsToMessageData (levelParams : List Name) : MessageData := match levelParams with diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean index 4cda4f3d66e2..c1c81e3d9e84 100644 --- a/src/Lean/Elab/Structure.lean +++ b/src/Lean/Elab/Structure.lean @@ -318,7 +318,7 @@ where if h : i < subfieldNames.size then let subfieldName := subfieldNames.get ⟨i, h⟩ if containsFieldName infos subfieldName then - throwError "field '{subfieldName}' from '{parentStructName}' has already been declared" + throwError "field '{subfieldName}' from '{.ofConstName parentStructName}' has already been declared" let val ← mkProjection parentFVar subfieldName let type ← inferType val withLetDecl subfieldName type val fun subfieldFVar => do @@ -428,7 +428,7 @@ private partial def copyDefaultValue? (fieldMap : FieldMap) (expandedStructNames go? (← instantiateValueLevelParams cinfo us) where failed : TermElabM (Option Expr) := do - logWarning s!"ignoring default value for field '{fieldName}' defined at '{structName}'" + logWarning m!"ignoring default value for field '{fieldName}' defined at '{.ofConstName structName}'" return none go? (e : Expr) : TermElabM (Option Expr) := do @@ -464,7 +464,7 @@ where | some existingFieldInfo => let existingFieldType ← inferType existingFieldInfo.fvar unless (← isDefEq fieldType existingFieldType) do - throwError "parent field type mismatch, field '{fieldName}' from parent '{parentStructName}' {← mkHasTypeButIsExpectedMsg fieldType existingFieldType}" + throwError "parent field type mismatch, field '{fieldName}' from parent '{.ofConstName parentStructName}' {← mkHasTypeButIsExpectedMsg fieldType existingFieldType}" /- Remark: if structure has a default value for this field, it will be set at the `processOveriddenDefaultValues` below. -/ copy (i+1) infos (fieldMap.insert fieldName existingFieldInfo.fvar) expandedStructNames | none => @@ -543,10 +543,10 @@ where let parentType ← whnf type let parentStructName ← getStructureName parentType if parents.any (fun info => info.structName == parentStructName) then - logWarningAt parent m!"duplicate parent structure '{parentStructName}'" + logWarningAt parent m!"duplicate parent structure '{.ofConstName parentStructName}'" if let some existingFieldName ← findExistingField? infos parentStructName then if structureDiamondWarning.get (← getOptions) then - logWarning s!"field '{existingFieldName}' from '{parentStructName}' has already been declared" + logWarning m!"field '{existingFieldName}' from '{.ofConstName parentStructName}' has already been declared" let parents := parents.push { ref := parent, fvar? := none, subobject := false, structName := parentStructName, type := parentType } copyNewFieldsFrom view.declName infos parentType fun infos => go (i+1) infos parents -- TODO: if `class`, then we need to create a let-decl that stores the local instance for the `parentStructure` diff --git a/src/Lean/Exception.lean b/src/Lean/Exception.lean index 7b212572aaab..896052f998aa 100644 --- a/src/Lean/Exception.lean +++ b/src/Lean/Exception.lean @@ -71,7 +71,7 @@ protected def throwError [Monad m] [MonadError m] (msg : MessageData) : m α := /-- Throw an unknown constant error message. -/ def throwUnknownConstant [Monad m] [MonadError m] (constName : Name) : m α := - Lean.throwError m!"unknown constant '{mkConst constName}'" + Lean.throwError m!"unknown constant '{.ofConstName constName}'" /-- Throw an error exception using the given message data and reference syntax. -/ protected def throwErrorAt [Monad m] [MonadError m] (ref : Syntax) (msg : MessageData) : m α := do @@ -81,10 +81,10 @@ protected def throwErrorAt [Monad m] [MonadError m] (ref : Syntax) (msg : Messag Convert an `Except` into a `m` monadic action, where `m` is any monad that implements `MonadError`. -/ -def ofExcept [Monad m] [MonadError m] [ToString ε] (x : Except ε α) : m α := +def ofExcept [Monad m] [MonadError m] [ToMessageData ε] (x : Except ε α) : m α := match x with | .ok a => return a - | .error e => Lean.throwError <| toString e + | .error e => Lean.throwError <| toMessageData e /-- Throw an error exception for the given kernel exception. diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index af4a6b422d08..7753311bc60e 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -168,8 +168,31 @@ def ofLevel (l : Level) : MessageData := return Dynamic.mk msg) (fun _ => false) +/-- +Simply formats the name. +See `MessageData.ofConstName` for richer messages. +-/ def ofName (n : Name) : MessageData := ofFormat (format n) +/-- +Represents a constant name such that hovering and "go to definition" works. +If there is no such constant in the environment, the name is simply formatted, but sanitized if it is a hygienic name. +Use `MessageData.ofName` if hovers are undesired. + +If `fullNames` is true, then pretty prints as if `pp.fullNames` is true. +Otherwise, pretty prints using the current user setting for `pp.fullNames`. +-/ +def ofConstName (constName : Name) (fullNames : Bool := false) : MessageData := + .ofLazy + (fun ctx? => do + let msg ← ofFormatWithInfos <$> match ctx? with + | .none => pure (format constName) + | .some ctx => + let ctx := if fullNames then { ctx with opts := ctx.opts.insert `pp.fullNames fullNames } else ctx + ppConstNameWithInfos ctx constName + return Dynamic.mk msg) + (fun _ => false) + partial def hasSyntheticSorry (msg : MessageData) : Bool := visit none msg where @@ -490,7 +513,7 @@ private def mkCtx (env : Environment) (lctx : LocalContext) (opts : Options) (ms def toMessageData (e : KernelException) (opts : Options) : MessageData := match e with | unknownConstant env constName => mkCtx env {} opts m!"(kernel) unknown constant '{constName}'" - | alreadyDeclared env constName => mkCtx env {} opts m!"(kernel) constant has already been declared '{constName}'" + | alreadyDeclared env constName => mkCtx env {} opts m!"(kernel) constant has already been declared '{.ofConstName constName true}'" | declTypeMismatch env decl givenType => mkCtx env {} opts <| let process (n : Name) (expectedType : Expr) : MessageData := @@ -499,8 +522,8 @@ def toMessageData (e : KernelException) (opts : Options) : MessageData := | Declaration.defnDecl { name := n, type := type, .. } => process n type | Declaration.thmDecl { name := n, type := type, .. } => process n type | _ => "(kernel) declaration type mismatch" -- TODO fix type checker, type mismatch for mutual decls does not have enough information - | declHasMVars env constName _ => mkCtx env {} opts m!"(kernel) declaration has metavariables '{constName}'" - | declHasFVars env constName _ => mkCtx env {} opts m!"(kernel) declaration has free variables '{constName}'" + | declHasMVars env constName _ => mkCtx env {} opts m!"(kernel) declaration has metavariables '{.ofConstName constName true}'" + | declHasFVars env constName _ => mkCtx env {} opts m!"(kernel) declaration has free variables '{.ofConstName constName true}'" | funExpected env lctx e => mkCtx env lctx opts m!"(kernel) function expected{indentExpr e}" | typeExpected env lctx e => mkCtx env lctx opts m!"(kernel) type expected{indentExpr e}" | letTypeMismatch env lctx n _ _ => mkCtx env lctx opts m!"(kernel) let-declaration type mismatch '{n}'" @@ -508,7 +531,7 @@ def toMessageData (e : KernelException) (opts : Options) : MessageData := | appTypeMismatch env lctx e fnType argType => mkCtx env lctx opts m!"application type mismatch{indentExpr e}\nargument has type{indentExpr argType}\nbut function has type{indentExpr fnType}" | invalidProj env lctx e => mkCtx env lctx opts m!"(kernel) invalid projection{indentExpr e}" - | thmTypeIsNotProp env constName type => mkCtx env {} opts m!"(kernel) type of theorem '{constName}' is not a proposition{indentExpr type}" + | thmTypeIsNotProp env constName type => mkCtx env {} opts m!"(kernel) type of theorem '{.ofConstName constName true}' is not a proposition{indentExpr type}" | other msg => m!"(kernel) {msg}" | deterministicTimeout => "(kernel) deterministic timeout" | excessiveMemory => "(kernel) excessive memory consumption detected" diff --git a/src/Lean/Meta/Match/Basic.lean b/src/Lean/Meta/Match/Basic.lean index 14bd8854d619..287dd9da0870 100644 --- a/src/Lean/Meta/Match/Basic.lean +++ b/src/Lean/Meta/Match/Basic.lean @@ -280,7 +280,7 @@ partial def varsToUnderscore : Example → Example partial def toMessageData : Example → MessageData | var fvarId => mkFVar fvarId | ctor ctorName [] => mkConst ctorName - | ctor ctorName exs => m!"({mkConst ctorName}{exs.foldl (fun msg pat => m!"{msg} {toMessageData pat}") Format.nil})" + | ctor ctorName exs => m!"({.ofConstName ctorName}{exs.foldl (fun msg pat => m!"{msg} {toMessageData pat}") Format.nil})" | arrayLit exs => "#" ++ MessageData.ofList (exs.map toMessageData) | val e => e | underscore => "_" diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean index 42c973b08178..1bb9a68026c1 100644 --- a/src/Lean/Meta/Tactic/Simp/Main.lean +++ b/src/Lean/Meta/Tactic/Simp/Main.lean @@ -200,7 +200,7 @@ private def reduceStep (e : Expr) : SimpM Expr := do return e.letBody!.instantiate1 e.letValue! match (← unfold? e) with | some e' => - trace[Meta.Tactic.simp.rewrite] "unfold {mkConst e.getAppFn.constName!}, {e} ==> {e'}" + trace[Meta.Tactic.simp.rewrite] "unfold {.ofConst e.getAppFn}, {e} ==> {e'}" recordSimpTheorem (.decl e.getAppFn.constName!) return e' | none => foldRawNatLit e diff --git a/src/Lean/Meta/Tactic/UnifyEq.lean b/src/Lean/Meta/Tactic/UnifyEq.lean index b1a5760ac70c..f535956c8ff6 100644 --- a/src/Lean/Meta/Tactic/UnifyEq.lean +++ b/src/Lean/Meta/Tactic/UnifyEq.lean @@ -116,7 +116,7 @@ def unifyEq? (mvarId : MVarId) (eqFVarId : FVarId) (subst : FVarSubst := {}) else match caseName? with | none => throwError "dependent elimination failed, failed to solve equation{indentExpr eqDecl.type}" - | some caseName => throwError "dependent elimination failed, failed to solve equation{indentExpr eqDecl.type}\nat case {mkConst caseName}" + | some caseName => throwError "dependent elimination failed, failed to solve equation{indentExpr eqDecl.type}\nat case {.ofConstName caseName}" let a ← instantiateMVars a let b ← instantiateMVars b match a, b with diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean index 82c529cb6eb1..35aeaeac98ee 100644 --- a/src/Lean/MonadEnv.lean +++ b/src/Lean/MonadEnv.lean @@ -92,7 +92,7 @@ def mkAuxName [Monad m] [MonadEnv m] (baseName : Name) (idx : Nat) : m Name := d def getConstInfo [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m ConstantInfo := do match (← getEnv).find? constName with | some info => pure info - | none => throwError "unknown constant '{mkConst constName}'" + | none => throwError "unknown constant '{.ofConstName constName}'" def mkConstWithLevelParams [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m Expr := do let info ← getConstInfo constName @@ -101,22 +101,22 @@ def mkConstWithLevelParams [Monad m] [MonadEnv m] [MonadError m] (constName : Na def getConstInfoDefn [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m DefinitionVal := do match (← getConstInfo constName) with | ConstantInfo.defnInfo v => pure v - | _ => throwError "'{mkConst constName}' is not a definition" + | _ => throwError "'{.ofConstName constName}' is not a definition" def getConstInfoInduct [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m InductiveVal := do match (← getConstInfo constName) with | ConstantInfo.inductInfo v => pure v - | _ => throwError "'{mkConst constName}' is not a inductive type" + | _ => throwError "'{.ofConstName constName}' is not a inductive type" def getConstInfoCtor [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m ConstructorVal := do match (← getConstInfo constName) with | ConstantInfo.ctorInfo v => pure v - | _ => throwError "'{mkConst constName}' is not a constructor" + | _ => throwError "'{.ofConstName constName}' is not a constructor" def getConstInfoRec [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m RecursorVal := do match (← getConstInfo constName) with | ConstantInfo.recInfo v => pure v - | _ => throwError "'{mkConst constName}' is not a recursor" + | _ => throwError "'{.ofConstName constName}' is not a recursor" @[inline] def matchConstStruct [Monad m] [MonadEnv m] [MonadError m] (e : Expr) (failK : Unit → m α) (k : InductiveVal → List Level → ConstructorVal → m α) : m α := matchConstInduct e failK fun ival us => do diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean index 672bd4a178f8..4d0500c854e1 100644 --- a/src/Lean/PrettyPrinter.lean +++ b/src/Lean/PrettyPrinter.lean @@ -63,6 +63,17 @@ def ppExprWithInfos (e : Expr) (optsPerPos : Delaborator.OptionsPerPos := {}) (d let fmt ← ppTerm stx >>= maybePrependExprSizes e return ⟨fmt, infos⟩ +open Delaborator in +def ppConstNameWithInfos (constName : Name) : MetaM FormatWithInfos := do + if let some info := (← getEnv).find? constName then + let delab := withOptionAtCurrPos `pp.tagAppFns true <| delabConst + PrettyPrinter.ppExprWithInfos (delab := delab) (.const constName <| info.levelParams.map mkLevelParam) + else + -- Still, let's sanitize the name. + let stx := mkIdent constName + let stx := (sanitizeSyntax stx).run' { options := (← getOptions) } + formatCategory `term stx + @[export lean_pp_expr] def ppExprLegacy (env : Environment) (mctx : MetavarContext) (lctx : LocalContext) (opts : Options) (e : Expr) : IO Format := Prod.fst <$> ((withOptions (fun _ => opts) <| ppExpr e).run' { lctx := lctx } { mctx := mctx }).toIO @@ -103,9 +114,10 @@ private def withoutContext {m} [MonadExcept Exception m] (x : m α) : m α := builtin_initialize ppFnsRef.set { - ppExprWithInfos := fun ctx e => ctx.runMetaM <| withoutContext <| ppExprWithInfos e, - ppTerm := fun ctx stx => ctx.runCoreM <| withoutContext <| ppTerm stx, - ppLevel := fun ctx l => return l.format (mvars := getPPMVarsLevels ctx.opts), + ppExprWithInfos := fun ctx e => ctx.runMetaM <| withoutContext <| ppExprWithInfos e + ppConstNameWithInfos := fun ctx n => ctx.runMetaM <| withoutContext <| ppConstNameWithInfos n + ppTerm := fun ctx stx => ctx.runCoreM <| withoutContext <| ppTerm stx + ppLevel := fun ctx l => return l.format (mvars := getPPMVarsLevels ctx.opts) ppGoal := fun ctx mvarId => ctx.runMetaM <| withoutContext <| Meta.ppGoal mvarId } @@ -155,19 +167,6 @@ def ofConst (e : Expr) : MessageData := else panic! "not a constant" -/-- -Pretty print a constant given its name, similar to `Lean.MessageData.ofConst`. -Uses the constant's universe level parameters when pretty printing. -If there is no such constant in the environment, the name is simply formatted. --/ -def ofConstName (constName : Name) : MessageData := - .ofFormatWithInfosM do - if let some info := (← getEnv).find? constName then - let delab : Delab := withOptionAtCurrPos `pp.tagAppFns true delabConst - PrettyPrinter.ppExprWithInfos (delab := delab) (.const constName <| info.levelParams.map mkLevelParam) - else - return format constName - /-- Generates `MessageData` for a declaration `c` as `c.{} : `, with terminfo. -/ def signature (c : Name) : MessageData := .ofFormatWithInfosM (PrettyPrinter.ppSignature c) diff --git a/src/Lean/ResolveName.lean b/src/Lean/ResolveName.lean index 7a5ebd978129..d932da357c46 100644 --- a/src/Lean/ResolveName.lean +++ b/src/Lean/ResolveName.lean @@ -20,7 +20,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 `{reservedName}` has already been declared" + throwError "failed to declare `{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/src/Lean/Util/PPExt.lean b/src/Lean/Util/PPExt.lean index fa32137b7c07..f1fb03cbbf61 100644 --- a/src/Lean/Util/PPExt.lean +++ b/src/Lean/Util/PPExt.lean @@ -52,6 +52,7 @@ instance : Coe Format FormatWithInfos where structure PPFns where ppExprWithInfos : PPContext → Expr → IO FormatWithInfos + ppConstNameWithInfos : PPContext → Name → IO FormatWithInfos ppTerm : PPContext → Term → IO Format ppLevel : PPContext → Level → IO Format ppGoal : PPContext → MVarId → IO Format @@ -60,6 +61,7 @@ structure PPFns where builtin_initialize ppFnsRef : IO.Ref PPFns ← IO.mkRef { ppExprWithInfos := fun _ e => return format (toString e) + ppConstNameWithInfos := fun _ n => return format n ppTerm := fun ctx stx => return stx.raw.formatStx (some <| pp.raw.maxDepth.get ctx.opts) ppLevel := fun _ l => return format l ppGoal := fun _ _ => return "goal" @@ -81,6 +83,9 @@ def ppExprWithInfos (ctx : PPContext) (e : Expr) : IO FormatWithInfos := do else pure f!"failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)" +def ppConstNameWithInfos (ctx : PPContext) (n : Name) : IO FormatWithInfos := + ppExt.getState ctx.env |>.ppConstNameWithInfos ctx n + def ppTerm (ctx : PPContext) (stx : Term) : IO Format := let fmtRaw := fun () => stx.raw.formatStx (some <| pp.raw.maxDepth.get ctx.opts) (pp.raw.showInfo.get ctx.opts) if pp.raw.get ctx.opts then diff --git a/src/Lean/Widget/UserWidget.lean b/src/Lean/Widget/UserWidget.lean index 37cf0f25c3e7..f4debf21abd1 100644 --- a/src/Lean/Widget/UserWidget.lean +++ b/src/Lean/Widget/UserWidget.lean @@ -96,7 +96,7 @@ builtin_initialize widgetModuleAttrImpl : AttributeImpl ← if let some _ := (← builtinModulesRef.get).find? mod.javascriptHash then logWarning m!"A builtin widget module with the same hash(JS source code) was already registered." if let some (n, _) := moduleRegistry.getState env |>.find? mod.javascriptHash then - logWarning m!"A widget module with the same hash(JS source code) was already registered at {Expr.const n []}." + logWarning m!"A widget module with the same hash(JS source code) was already registered at {.ofConstName n true}." let env ← getEnv if builtin then let h := mkConst decl diff --git a/src/lake/Lake/DSL/DeclUtil.lean b/src/lake/Lake/DSL/DeclUtil.lean index 20bf1c179953..ce098a62d9b4 100644 --- a/src/lake/Lake/DSL/DeclUtil.lean +++ b/src/lake/Lake/DSL/DeclUtil.lean @@ -107,7 +107,7 @@ def elabConfigDecl if findField? (← getEnv) tyName fieldName |>.isSome then m := m.insert fieldName {ref := id, val} else - logWarningAt id m!"unknown '{mkConst tyName}' field '{fieldName}'" + logWarningAt id m!"unknown '{.ofConstName tyName}' field '{fieldName}'" let fs ← m.foldM (init := #[]) fun a k {ref, val} => withRef ref do return a.push <| ← `(Term.structInstField| $(← mkIdentFromRef k true):ident := $val) let ty := mkCIdentFrom (← getRef) tyName