diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index a2e0d3532b..b480ea0f3d 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -763,7 +763,7 @@ and checks that they match the contents of the docstring. Basic example: ```lean /-- -error: unknown identifier 'x' +error: Unknown identifier `x` -/ #guard_msgs in example : α := x diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index f4c412c8d2..e5eea058e2 100644 --- a/src/Lean/Attributes.lean +++ b/src/Lean/Attributes.lean @@ -364,7 +364,7 @@ private def AttributeExtension.mkInitial : IO AttributeExtensionState := do unsafe def mkAttributeImplOfConstantUnsafe (env : Environment) (opts : Options) (declName : Name) : Except String AttributeImpl := match env.find? declName with - | none => throw ("unknown constant '" ++ toString declName ++ "'") + | none => throw ("Unknown constant `" ++ toString declName ++ "`") | some info => match info.type with | Expr.const `Lean.AttributeImpl _ => env.evalConst AttributeImpl opts declName diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean index 86d398ca3d..7fe52d329a 100644 --- a/src/Lean/Elab/App.lean +++ b/src/Lean/Elab/App.lean @@ -1667,7 +1667,7 @@ where return fvar else throwUnknownIdentifierAt id <| m!"Unknown identifier `{idNew}`" - ++ .note m!"Inferred this identifier from the expected type of `.{id}`:{indentExpr expectedType}" + ++ .note m!"Inferred this name from the expected resulting type of `.{id}`:{indentExpr expectedType}" | .sort .. => throwNamedError lean.invalidDottedIdent "Invalid dotted identifier notation: Not supported on type universe{indentExpr resultTypeFn}" | _ => diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean index cd0b75cba2..742175beb1 100644 --- a/src/Lean/Elab/Binders.lean +++ b/src/Lean/Elab/Binders.lean @@ -178,12 +178,20 @@ private def toBinderViews (stx : Syntax) : TermElabM (Array BinderView) := do else throwUnsupportedSyntax +/-- +The error name for "failed to infer binder type" errors. + +We cannot use `logNamedError` here because the error is logged later, after attempting to synthesize +metavariables, in `logUnassignedUsingErrorInfos`. +-/ +def failedToInferBinderTypeErrorName := `lean.inferBinderTypeFailed + private def registerFailedToInferBinderTypeInfo (type : Expr) (view : BinderView) : TermElabM Unit := do let msg := if view.id.getId.hasMacroScopes then m!"binder type" else m!"type of binder `{view.id.getId}`" - registerCustomErrorIfMVar type view.ref m!"Failed to infer {msg}" + registerCustomErrorIfMVar type view.ref (m!"Failed to infer {msg}".tagWithErrorName failedToInferBinderTypeErrorName) registerLevelMVarErrorExprInfo type view.ref m!"Failed to infer universe levels in {msg}" def addLocalVarInfo (stx : Syntax) (fvar : Expr) : TermElabM Unit := diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 40d8f97277..03b97ce1ba 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -124,6 +124,14 @@ private def check (prevHeaders : Array DefViewElabHeader) (newHeader : DefViewEl else pure () +/-- +The error name for "failed to infer definition type" errors. + +We cannot use `logNamedError` here because the error is logged later, after attempting to synthesize +metavariables, in `logUnassignedUsingErrorInfos`. +-/ +def failedToInferDefTypeErrorName := `lean.inferDefTypeFailed + private def registerFailedToInferDefTypeInfo (type : Expr) (view : DefView) : TermElabM Unit := let ref := view.type?.getD <| match view.kind with @@ -138,7 +146,7 @@ private def registerFailedToInferDefTypeInfo (type : Expr) (view : DefView) : else m!"instance" | .theorem => m!"theorem `{view.declId}`" | _ => m!"definition `{view.declId}`" - registerCustomErrorIfMVar type ref m!"Failed to infer type of {msg}" + registerCustomErrorIfMVar type ref (m!"Failed to infer type of {msg}".tagWithErrorName failedToInferDefTypeErrorName) /-- Return `some [b, c]` if the given `views` are representing a declaration of the form @@ -159,12 +167,16 @@ private def getPendingMVarErrorMessage (views : Array DefView) : MessageData := | some ids => let idsStr := ", ".intercalate <| ids.map fun id => s!"`{id}`" let paramsStr := ", ".intercalate <| ids.map fun id => s!"`({id} : _)`" - MessageData.note m!"Recall that you cannot declare multiple constants in a single declaration. The identifier(s) {idsStr} are being interpreted as parameters {paramsStr}." + MessageData.note m!"Multiple constants cannot be declared in a single declaration. \ + The identifier(s) {idsStr} are being interpreted as parameters {paramsStr}." | none => if views.all fun view => view.kind.isTheorem then - MessageData.note "All holes (e.g., `_`) in the header of a theorem are resolved before the proof is processed; information from the proof cannot be used to infer what these values should be" + MessageData.note "All parameter types and holes (e.g., `_`) in the header of a theorem are resolved \ + before the proof is processed; information from the proof cannot be used to infer what these values should be" else - MessageData.note "When the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed" + MessageData.note "Because this declaration's type has been explicitly provided, all parameter \ + types and holes (e.g., `_`) in its header are resolved before its body is processed; \ + information from the declaration body cannot be used to infer what these values should be" /-- Convert terms of the form `OfNat (OfNat.ofNat Nat ..)` into `OfNat `. diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean index a6ddc86bb3..7ee9432e0f 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 '{.ofConstName id}'" + throwError "Unknown identifier `{.ofConstName id}`" private def levelParamsToMessageData (levelParams : List Name) : MessageData := match levelParams with diff --git a/src/Lean/Elab/Quotation/Precheck.lean b/src/Lean/Elab/Quotation/Precheck.lean index 872202e34e..49d85f7c8f 100644 --- a/src/Lean/Elab/Quotation/Precheck.lean +++ b/src/Lean/Elab/Quotation/Precheck.lean @@ -107,7 +107,8 @@ private def isSectionVariable (e : Expr) : TermElabM Bool := do if quotPrecheck.allowSectionVars.get (← getOptions) && (← isSectionVariable e) then return | _ => pure () - throwError "unknown identifier '{val}' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check." + throwError m!"Unknown identifier `{val}` at quotation precheck" + ++ .note "You can use `set_option quotPrecheck false` to disable this check." | _ => throwUnsupportedSyntax @[builtin_quot_precheck Lean.Parser.Term.app] def precheckApp : Precheck diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean index 5e4c59f966..19ca391cd4 100644 --- a/src/Lean/Elab/Term.lean +++ b/src/Lean/Elab/Term.lean @@ -822,7 +822,7 @@ where appendExtra (msg : MessageData) : MessageData := match extraMsg? with | none => msg - | some extraMsg => msg ++ extraMsg + | some extraMsg => msg.composePreservingKind extraMsg /-- Try to log errors for the unassigned metavariables `pendingMVarIds`. @@ -1998,7 +1998,7 @@ where isValidAutoBoundImplicitName n (relaxedAutoImplicit.get (← getOptions)) then throwAutoBoundImplicitLocal n else - throwUnknownIdentifierAt stx m!"unknown identifier '{Lean.mkConst n}'" + throwUnknownIdentifierAt stx m!"Unknown identifier `{Lean.mkConst n}`" mkConsts candidates explicitLevels /-- diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean index e9d7b63bce..8bbb573419 100644 --- a/src/Lean/Environment.lean +++ b/src/Lean/Environment.lean @@ -2366,7 +2366,7 @@ where Note that this function cannot guarantee that `typeName` is in fact the name of the type `α`. -/ unsafe def evalConstCheck (α) (env : Environment) (opts : Options) (typeName : Name) (constName : Name) : ExceptT String Id α := match env.find? constName with - | none => throw ("unknown constant '" ++ toString constName ++ "'") + | none => throw ("Unknown constant `" ++ toString constName ++ "`") | some info => match info.type with | Expr.const c _ => diff --git a/src/Lean/ErrorExplanations.lean b/src/Lean/ErrorExplanations.lean index ab4fff8d9d..dd4dd62d6e 100644 --- a/src/Lean/ErrorExplanations.lean +++ b/src/Lean/ErrorExplanations.lean @@ -8,5 +8,8 @@ import Lean.ErrorExplanations.CtorResultingTypeMismatch import Lean.ErrorExplanations.DependsOnNoncomputable import Lean.ErrorExplanations.InductiveParamMismatch import Lean.ErrorExplanations.InductiveParamMissing +import Lean.ErrorExplanations.InferBinderTypeFailed +import Lean.ErrorExplanations.InferDefTypeFailed import Lean.ErrorExplanations.InvalidDottedIdent import Lean.ErrorExplanations.RedundantMatchAlt +import Lean.ErrorExplanations.UnknownIdentifier diff --git a/src/Lean/ErrorExplanations/InferBinderTypeFailed.lean b/src/Lean/ErrorExplanations/InferBinderTypeFailed.lean new file mode 100644 index 0000000000..24f0ab71f3 --- /dev/null +++ b/src/Lean/ErrorExplanations/InferBinderTypeFailed.lean @@ -0,0 +1,159 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Rotella +-/ +prelude +import Lean.ErrorExplanation + +/-- +This error occurs when the type of a binder in a declaration header or local binding is not fully +specified and cannot be inferred by Lean. Generally, this can be resolved by providing more +information to help Lean determine the type of the binder, either by explicitly annotating its type +or by providing additional type information at sites where it is used. When the binder in question +occurs in the header of a declaration, this error is often accompanied by +[`lean.inferDefTypeFailed`](lean-manual://errorExplanation/lean.inferDefTypeFailed). + +Note that if a declaration is annotated with an explicit resulting type—even one that contains +holes—Lean will not use information from the definition body to infer parameter types. It may +therefore be necessary to explicitly specify the types of parameters whose types would otherwise be +inferable without the resulting-type annotation; see the "uninferred binder due to resulting type +annotation" example below for a demonstration. In `theorem` declarations, the body is never used to +infer the types of binders, so any binders whose types cannot be inferred from the rest of the +theorem type must include a type annotation. + +This error may also arise when identifiers that were intended to be declaration names are +inadvertently written in binder position instead. In these cases, the erroneous identifiers are +treated as binders with unspecified type, leading to a type inference failure. This frequently +occurs when attempting to simultaneously define multiple constants of the same type using syntax +that does not support this. Such situations include: +* Attempting to name an example by writing an identifier after the `example` keyword; +* Attempting to define multiple constants with the same type and (if applicable) value by listing + them sequentially after `def`, `opaque`, or another declaration keyword; +* Attempting to define multiple fields of a structure of the same type by sequentially listing their + names on the same line of a structure declaration; and +* Omitting vertical bars between inductive constructor names. + +The first three cases are demonstrated in examples below. + +# Examples + +## Binder type requires new type variable + +```lean broken +def identity x := + x +``` +```output +Failed to infer type of binder `x` +``` +```lean fixed +def identity (x : α) := + x +``` + +In the code above, the type of `x` is unconstrained; as this example demonstrates, Lean does not +automatically generate fresh type variables for such binders. Instead, the type `α` of `x` must be +specified explicitly. Note that if automatic implicit parameter insertion is enabled (as it is by +default), a binder for `α` itself need not be provided; Lean will insert an implicit binder for this +parameter automatically. + +## Uninferred binder type due to resulting type annotation + +```lean broken +def plusTwo x : Nat := + x + 2 +``` +```output +Failed to infer type of binder `x` + +Note: Because this declaration's type has been explicitly provided, all parameter types and holes (e.g., `_`) in its header are resolved before its body is processed; information from the declaration body cannot be used to infer what these values should be +``` +```lean fixed +def plusTwo (x : Nat) : Nat := + x + 2 +``` + +Even though `x` is inferred to have type `Nat` in the body of `plusTwo`, this information is not +available when elaborating the type of the definition because its resulting type (`Nat`) has been +explicitly specified. Considering only the information in the header, the type of `x` cannot be +determined, resulting in the shown error. It is therefore necessary to include the type of `x` in +its binder. + + +## Attempting to name an example declaration + +```lean broken +example trivial_proof : True := + trivial +``` +```output +Failed to infer type of binder `trivial_proof` + +Note: Because this declaration's type has been explicitly provided, all parameter types and holes (e.g., `_`) in its header are resolved before its body is processed; information from the declaration body cannot be used to infer what these values should be +``` +```lean fixed +example : True := + trivial +``` +This code is invalid because it attempts to give a name to an `example` declaration. Examples cannot +be named, and an identifier written where a name would appear in other declaration forms is instead +elaborated as a binder, whose type cannot be inferred. If a declaration must be named, it should be +defined using a declaration form that supports naming, such as `def` or `theorem`. + +## Attempting to define multiple opaque constants at once + +```lean broken +opaque m n : Nat +``` +```output +Failed to infer type of binder `n` + +Note: Multiple constants cannot be declared in a single declaration. The identifier(s) `n` are being interpreted as parameters `(n : _)`. +``` +```lean fixed +opaque m : Nat +opaque n : Nat +``` + +This example incorrectly attempts to define multiple constants with a single `opaque` declaration. +Such a declaration can define only one constant: it is not possible to list multiple identifiers +after `opaque` or `def` to define them all to have the same type (or value). Such a declaration is +instead elaborated as defining a single constant (e.g., `m` above) with parameters given by the +subsequent identifiers (`n`), whose types are unspecified and cannot be inferred. To define multiple +global constants, it is necessary to declare each separately. + +## Attempting to define multiple structure fields on the same line + +```lean broken +structure Person where + givenName familyName : String + age : Nat +``` +```output +Failed to infer type of binder `familyName` +``` +```lean fixed (title := "Fixed (separate lines)") +structure Person where + givenName : String + familyName : String + age : Nat +``` +```lean fixed (title := "Fixed (parenthesized)") +structure Person where + (givenName familyName : String) + age : Nat +``` + +This example incorrectly attempts to define multiple structure fields (`givenName` and `familyName`) +of the same type by listing them consecutively on the same line. Lean instead interprets this as +defining a single field, `givenName`, parametrized by a binder `familyName` with no specified type. +The intended behavior can be achieved by either listing each field on a separate line, or enclosing +the line specifying multiple field names in parentheses (see the manual section on +[Inductive Types](lean-manual://section/inductive-types) for further details about structure +declarations). +-/ +register_error_explanation lean.inferBinderTypeFailed { + summary := "The type of a binder could not be inferred." + sinceVersion := "4.23.0" +} diff --git a/src/Lean/ErrorExplanations/InferDefTypeFailed.lean b/src/Lean/ErrorExplanations/InferDefTypeFailed.lean new file mode 100644 index 0000000000..2f0c4f033b --- /dev/null +++ b/src/Lean/ErrorExplanations/InferDefTypeFailed.lean @@ -0,0 +1,82 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Rotella +-/ +prelude +import Lean.ErrorExplanation + +/-- +This error occurs when the type of a definition is not fully specified and Lean is unable to infer +its type from the available information. If the definition has parameters, this error refers only to +the resulting type after the colon (the error +[`lean.inferBinderTypeFailed`](lean-manual://errorExplanation/lean.inferBinderTypeFailed) indicates +that a parameter type could not be inferred). + +To resolve this error, provide additional type information in the definition. This can be done +straightforwardly by providing an explicit resulting type after the colon in the definition +header. Alternatively, if an explicit resulting type is not provided, adding further type +information to the definition's body—such as by specifying implicit type arguments or giving +explicit types to `let` binders—may allow Lean to infer the type of the definition. Look for type +inference or implicit argument synthesis errors that arise alongside this one to identify +ambiguities that may be contributing to this error. + +Note that when an explicit resulting type is provided—even if that type contains holes—Lean will not +use information from the definition body to help infer the type of the definition or its parameters. +Thus, adding an explicit resulting type may also necessitate adding type annotations to parameters +whose types were previously inferrable. Additionally, it is always necessary to provide an explicit +type in a `theorem` declaration: the `theorem` syntax requires a type annotation, and the elaborator +will never attempt to use the theorem body to infer the proposition being proved. + +# Examples + +## Implicit argument cannot be inferred + +```lean broken +def emptyNats := + [] +``` +```output +Failed to infer type of definition `emptyNats` +``` + +```lean fixed (title := "Fixed (type annotation)") +def emptyNats : List Nat := + [] +``` +```lean fixed (title := "Fixed (implicit argument)") +def emptyNats := + List.nil (α := Nat) +``` + +Here, Lean is unable to infer the value of the parameter `α` of the `List` type constructor, which +in turn prevents it from inferring the type of the definition. Two fixes are possible: specifying +the expected type of the definition allows Lean to infer the appropriate implicit argument to the +`List.nil` constructor; alternatively, making this implicit argument explicit in the function body +provides sufficient information for Lean to infer the definition's type. + +## Definition type uninferrable due to unknown parameter type + +```lean broken +def identity x := + x +``` +```output +Failed to infer type of definition `identity` +``` +```lean fixed +def identity (x : α) := + x +``` + +In this example, the type of `identity` is determined by the type of `x`, which cannot be inferred. +Both the indicated error and +[lean.inferBinderTypeFailed](lean-manual://errorExplanation/lean.inferBinderTypeFailed) therefore +appear (see that explanation for additional discussion of this example). Resolving the latter—by +explicitly specifying the type of `x`—provides Lean with sufficient information to infer the +definition type. +-/ +register_error_explanation lean.inferDefTypeFailed { + summary := "The type of a definition could not be inferred." + sinceVersion := "4.23.0" +} diff --git a/src/Lean/ErrorExplanations/UnknownIdentifier.lean b/src/Lean/ErrorExplanations/UnknownIdentifier.lean new file mode 100644 index 0000000000..86461cf3c4 --- /dev/null +++ b/src/Lean/ErrorExplanations/UnknownIdentifier.lean @@ -0,0 +1,186 @@ +/- +Copyright (c) 2025 Lean FRO, LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Rotella +-/ +prelude +import Lean.ErrorExplanation + +/-- +This error means that Lean was unable to find a variable or constant matching the given name. More +precisely, this means that the name could not be *resolved*, as described in the manual section on +[Identifiers](lean-manual://section/identifiers-and-resolution): no interpretation of the input as +the name of a local or section variable (if applicable), a previously declared global constant, or a +projection of either of the preceding was valid. ("If applicable" refers to the fact that in some +cases—e.g., the `#print` command's argument—names are resolved only to global constants.) + +Note that this error message will display only one possible resolution of the identifier, but the +presence of this error indicates failures for *all* possible names to which it might refer. For +example, if the identifier `x` is entered with the namespaces `A` and `B` are open, the error +message "Unknown identifier \`x\`" indicates that none of `x`, `A.x`, or `B.x` could be found (or +that `A.x` or `B.x`, if either exists, is a protected declaration). + +Common causes of this error include forgetting to import the module in which a constant is defined, +omitting a constant's namespace when that namespace is not open, or attempting to refer to a local +variable that is not in scope. + +To help resolve some of these common issues, this error message is accompanied by a code action that +suggests constant names similar to the one provided. These include constants in the environment as +well as those that can be imported from other modules. Note that these suggestions are available +only through supported code editors' built-in code action mechanisms and not as a hint in the error +message itself. + +# Examples + +## Missing import + +```lean broken +def inventory := + Std.HashSet.ofList [("apples", 3), ("bananas", 4)] +``` +```output +Unknown constant `Std.HashSet.ofList` +``` +```lean fixed +import Std.Data.HashSet.Basic + +def inventory := + Std.HashSet.ofList [("apples", 3), ("bananas", 4)] +``` +The constant `Std.HashSet.ofList` is defined in the `Std.Data.HashSet.Basic` module, which has not +been imported in the original example. This import is suggested by the unknown identifier code +action; once it is added, this example compiles. + +## Variable not in scope + +```lean broken +example (s : IO.FS.Stream) := do + IO.withStdout s do + let text := "Hello" + IO.println text + IO.println s!"Wrote '{text}' to stream" +``` +```output +Unknown identifier `text` +``` +```lean fixed +example (s : IO.FS.Stream) := do + let text := "Hello" + IO.withStdout s do + IO.println text + IO.println s!"Wrote '{text}' to stream" +``` +An unknown identifier error occurs on the last line of this example because the variable `text` is +not in scope. The `let`-binding on the third line is scoped to the inner `do` block and cannot be +accessed in the outer `do` block. Moving this binding to the outer `do` block—from which it remains +in scope in the inner block as well—resolves the issue. + +## Missing namespace + +```lean broken +inductive Color where + | rgb (r g b : Nat) + | grayscale (k : Nat) + +def red : Color := + rgb 255 0 0 +``` +```output +Unknown identifier `rgb` +``` +```lean fixed (title := "Fixed (qualified name)") +inductive Color where + | rgb (r g b : Nat) + | grayscale (k : Nat) + +def red : Color := + Color.rgb 255 0 0 +``` +```lean fixed (title := "Fixed (open namespace)") +inductive Color where + | rgb (r g b : Nat) + | grayscale (k : Nat) + +open Color in +def red : Color := + rgb 255 0 0 +``` + +In this example, the identifier `rgb` on the last line does not resolve to the `Color` constructor +of that name. This is because the constructor's name is actually `Color.rgb`: all constructors of an +inductive type have names in that type's namespace. Because the `Color` namespace is not open, the +identifier `rgb` cannot be used without its namespace prefix. + +One way to resolve this error is to provide the fully qualified constructor name `Color.rgb`; the +dotted-identifier notation `.rgb` can also be used, since the expected type of `.rgb 255 0 0` is +`Color`. Alternatively, one can open the `Color` namespace and continue to omit the `Color` prefix +from the identifier. + +## Protected constant name without namespace prefix + +```lean broken +protected def A.x := () + +open A + +example := x +``` +```output +Unknown identifier `x` +``` +```lean fixed (title := "Fixed (qualified name)") +protected def A.x := () + +open A + +example := A.x +``` +```lean fixed (title := "Fixed (restricted open)") +protected def A.x := () + +open A (x) + +example := x +``` + +In this example, because the constant `A.x` is `protected`, it cannot be referred to by the suffix +`x` even with the namespace `A` open. Therefore, the identifier `x` fails to resolve. Instead, to +refer to a `protected` constant, it is necessary to include at least its innermost namespace—in this +case, `A`. Alternatively, the *restricted opening* syntax—demonstrated in the second corrected +example—allows a `protected` constant to be referred to by its unqualified name, without opening the +remainder of the namespace in which it occurs (see the manual section on +[Namespaces and Sections](lean-manual://section/namespaces-sections) for details). + +## Unresolvable name inferred by dotted-identifier notation + +```lean broken +def disjoinToNat (b₁ b₂ : Bool) : Nat := + .toNat (b₁ || b₂) +``` +```output +Unknown identifier `Nat.toNat` + +Note: Inferred this name from the expected resulting type of `.toNat`: + Nat +``` +```lean fixed (title := "Fixed (generalized field notation)") +def disjoinToNat (b₁ b₂ : Bool) : Nat := + (b₁ || b₂).toNat +``` +```lean fixed (title := "Fixed (qualified name)") +def disjoinToNat (b₁ b₂ : Bool) : Nat := + Bool.toNat (b₁ || b₂) +``` + +In this example, the dotted-identifier notation `.toNat` causes Lean to infer an unresolvable +name (`Nat.toNat`). The namespace used by dotted-identifier notation is always inferred from +the expected type of the expression in which it occurs, which—due to the type annotation on +`disjoinToNat`—is `Nat` in this example. To use the namespace of an argument's type—as the author of +this code seemingly intended—use *generalized field notation* as shown in the first corrected +example. Alternatively, the correct namespace can be explicitly specified by writing the fully +qualified function name. +-/ +register_error_explanation lean.unknownIdentifier { + summary := "Failed to resolve identifier to variable or constant." + sinceVersion := "4.23.0" +} diff --git a/src/Lean/Exception.lean b/src/Lean/Exception.lean index 732fbd9d65..cc4c6adda7 100644 --- a/src/Lean/Exception.lean +++ b/src/Lean/Exception.lean @@ -77,7 +77,7 @@ Tag used for `unknown identifier` messages. This tag is used by the 'import unknown identifier' code action to detect messages that should prompt the code action. -/ -def unknownIdentifierMessageTag : Name := `unknownIdentifier +def unknownIdentifierMessageTag : Name := kindOfErrorName `lean.unknownIdentifier /-- 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 @@ -128,7 +128,7 @@ The end position of the range of `ref` should point at the unknown identifier. See also `mkUnknownIdentifierMessage`. -/ def throwUnknownConstantAt [Monad m] [MonadError m] (ref : Syntax) (constName : Name) : m α := do - throwUnknownIdentifierAt ref m!"unknown constant '{.ofConstName constName}'" + throwUnknownIdentifierAt ref m!"Unknown constant `{.ofConstName constName}`" /-- Throw an unknown constant error message. diff --git a/src/Lean/Linter/MissingDocs.lean b/src/Lean/Linter/MissingDocs.lean index bbe82a2887..ff0c813be4 100644 --- a/src/Lean/Linter/MissingDocs.lean +++ b/src/Lean/Linter/MissingDocs.lean @@ -34,7 +34,7 @@ unsafe def mkHandlerUnsafe (constName : Name) : ImportM Handler := do let env := (← read).env let opts := (← read).opts match env.find? constName with - | none => throw ↑s!"unknown constant '{constName}'" + | none => throw ↑s!"Unknown constant `{constName}`" | some info => match info.type with | Expr.const ``SimpleHandler _ => do let h ← IO.ofExcept $ env.evalConst SimpleHandler opts constName diff --git a/src/Lean/Linter/UnusedVariables.lean b/src/Lean/Linter/UnusedVariables.lean index ac495504c9..9307929566 100644 --- a/src/Lean/Linter/UnusedVariables.lean +++ b/src/Lean/Linter/UnusedVariables.lean @@ -132,7 +132,7 @@ abbrev IgnoreFunction := Syntax → Syntax.Stack → LinterOptions → Bool unsafe def mkIgnoreFnImpl (constName : Name) : ImportM IgnoreFunction := do let { env, opts, .. } ← read match env.find? constName with - | none => throw ↑s!"unknown constant '{constName}'" + | none => throw ↑s!"Unknown constant `{constName}`" | some info => unless info.type.isConstOf ``IgnoreFunction do throw ↑s!"unexpected unused_variables_ignore_fn at '{constName}', must be of type `Lean.Linter.IgnoreFunction`" diff --git a/src/Lean/Message.lean b/src/Lean/Message.lean index d3ce0d7eee..e74a3ea6f0 100644 --- a/src/Lean/Message.lean +++ b/src/Lean/Message.lean @@ -441,6 +441,12 @@ code. -/ def errorNameSuffix := "_namedError" +/-- +Creates a tag (i.e., message kind) for an error message with (user-facing) name `errorName`. +-/ +def kindOfErrorName (errorName : Name) : Name := + .str errorName errorNameSuffix + /-- Produces a `MessageData` tagged with an identifier for error `name`. @@ -448,7 +454,7 @@ Note: this function generally should not be called directly; instead, use the ma and `throwNamedError`. -/ def MessageData.tagWithErrorName (msg : MessageData) (name : Name) : MessageData := - .tagged (.str name errorNameSuffix) msg + .tagged (kindOfErrorName name) msg /-- If the provided name is labeled as a diagnostic name, removes the label and returns the diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean index 4534c4748b..1c807ae81a 100644 --- a/src/Lean/Meta/Instances.lean +++ b/src/Lean/Meta/Instances.lean @@ -307,7 +307,7 @@ 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 `{declName}`" | some info => forallTelescopeReducing info.type fun _ type => do match type.getAppFn with diff --git a/src/Lean/Meta/Tactic/Simp/Simproc.lean b/src/Lean/Meta/Tactic/Simp/Simproc.lean index ac6c1002f9..fc6fac4e71 100644 --- a/src/Lean/Meta/Tactic/Simp/Simproc.lean +++ b/src/Lean/Meta/Tactic/Simp/Simproc.lean @@ -121,7 +121,7 @@ abbrev SimprocExtension := ScopedEnvExtension SimprocOLeanEntry SimprocEntry Sim unsafe def getSimprocFromDeclImpl (declName : Name) : ImportM (Sum Simproc DSimproc) := do let ctx ← read match ctx.env.find? declName with - | none => throw <| IO.userError ("unknown constant '" ++ toString declName ++ "'") + | none => throw <| IO.userError ("Unknown constant `" ++ toString declName ++ "`") | some info => match info.type with | .const ``Simproc _ => diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean index 344ae70b88..18dae86c57 100644 --- a/src/Lean/MonadEnv.lean +++ b/src/Lean/MonadEnv.lean @@ -82,17 +82,17 @@ def hasConst [Monad m] [MonadEnv m] (constName : Name) (skipRealize := true) : m 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 '{.ofConstName constName}'" + | none => throwError "Unknown constant `{.ofConstName constName}`" def getConstVal [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m ConstantVal := do match (← getEnv).findConstVal? constName with | some val => pure val - | none => throwError "unknown constant '{mkConst constName}'" + | none => throwError "Unknown constant `{mkConst constName}`" def getAsyncConstInfo [Monad m] [MonadEnv m] [MonadError m] (constName : Name) (skipRealize := false) : m AsyncConstantInfo := do match (← getEnv).findAsync? (skipRealize := skipRealize) constName with | some val => pure val - | none => throwError "unknown constant '{mkConst constName}'" + | none => throwError "Unknown constant `{mkConst constName}`" def mkConstWithLevelParams [Monad m] [MonadEnv m] [MonadError m] (constName : Name) : m Expr := do let info ← getConstVal constName diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 87acbcfe34..78965aaca8 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -252,7 +252,7 @@ unsafe def mkParserOfConstantUnsafe (constName : Name) (compileParserDescr : Par let env := (← read).env let opts := (← read).opts match env.find? constName with - | none => throw ↑s!"unknown constant '{constName}'" + | none => throw ↑s!"Unknown constant `{constName}`" | some info => match info.type with | Expr.const `Lean.Parser.TrailingParser _ => diff --git a/tests/lean/1011.lean.expected.out b/tests/lean/1011.lean.expected.out index 234d13e2d6..2d742d2730 100644 --- a/tests/lean/1011.lean.expected.out +++ b/tests/lean/1011.lean.expected.out @@ -1 +1 @@ -1011.lean:6:11-6:13: error: unknown identifier 'AA' +1011.lean:6:11-6:13: error(lean.unknownIdentifier): Unknown identifier `AA` diff --git a/tests/lean/1038.lean.expected.out b/tests/lean/1038.lean.expected.out index b4673f5605..906a8da50a 100644 --- a/tests/lean/1038.lean.expected.out +++ b/tests/lean/1038.lean.expected.out @@ -1 +1 @@ -1038.lean:1:7-1:21: error: unknown constant 'IO.FS.realpath' +1038.lean:1:7-1:21: error(lean.unknownIdentifier): Unknown constant `IO.FS.realpath` diff --git a/tests/lean/1074b.lean.expected.out b/tests/lean/1074b.lean.expected.out index 8cc7a50dba..5f52a4cc9f 100644 --- a/tests/lean/1074b.lean.expected.out +++ b/tests/lean/1074b.lean.expected.out @@ -1,4 +1,4 @@ -1074b.lean:10:30-10:31: error: unknown identifier 'z' +1074b.lean:10:30-10:31: error(lean.unknownIdentifier): Unknown identifier `z` 1074b.lean:11:43-11:53: error: tactic 'assumption' failed a n z✝ : Term a✝ : Brx z✝ diff --git a/tests/lean/1569.lean.expected.out b/tests/lean/1569.lean.expected.out index ce606f7a1f..2d0c4617f1 100644 --- a/tests/lean/1569.lean.expected.out +++ b/tests/lean/1569.lean.expected.out @@ -1 +1 @@ -1569.lean:2:26-2:30: error: unknown identifier 'typo' +1569.lean:2:26-2:30: error(lean.unknownIdentifier): Unknown identifier `typo` diff --git a/tests/lean/1576.lean.expected.out b/tests/lean/1576.lean.expected.out index d4986a6607..41da073363 100644 --- a/tests/lean/1576.lean.expected.out +++ b/tests/lean/1576.lean.expected.out @@ -1,4 +1,4 @@ -1576.lean:1:35-1:38: error: unknown identifier 'non' -1576.lean:1:41-1:46: error: unknown identifier 'sense' +1576.lean:1:35-1:38: error(lean.unknownIdentifier): Unknown identifier `non` +1576.lean:1:41-1:46: error(lean.unknownIdentifier): Unknown identifier `sense` 1576.lean:1:18-1:50: error: unsolved goals ⊢ True diff --git a/tests/lean/1707.lean.expected.out b/tests/lean/1707.lean.expected.out index 5ca8427907..bbd7a3fc8c 100644 --- a/tests/lean/1707.lean.expected.out +++ b/tests/lean/1707.lean.expected.out @@ -1,2 +1,2 @@ -1707.lean:1:9-1:10: error: unknown identifier 'c' +1707.lean:1:9-1:10: error(lean.unknownIdentifier): Unknown identifier `c` 1707.lean:1:12: error: expected token diff --git a/tests/lean/255.lean.expected.out b/tests/lean/255.lean.expected.out index d9978a70dd..096ab9c2f0 100644 --- a/tests/lean/255.lean.expected.out +++ b/tests/lean/255.lean.expected.out @@ -1,6 +1,6 @@ A : α id x✝ : α -255.lean:16:7-16:8: error: unknown constant 'x✝' +255.lean:16:7-16:8: error: Unknown constant `x✝` id sorry : ?m -255.lean:20:9-20:10: error: unknown constant 'x✝' +255.lean:20:9-20:10: error: Unknown constant `x✝` id sorry : ?m diff --git a/tests/lean/277a.lean.expected.out b/tests/lean/277a.lean.expected.out index 37aa68a463..39d2a4fab3 100644 --- a/tests/lean/277a.lean.expected.out +++ b/tests/lean/277a.lean.expected.out @@ -1 +1 @@ -277a.lean:4:7-4:15: error: unknown identifier 'nonexistent' +277a.lean:4:7-4:15: error(lean.unknownIdentifier): Unknown identifier `nonexistent` diff --git a/tests/lean/331.lean.expected.out b/tests/lean/331.lean.expected.out index 953ec1be0a..3963e1cc94 100644 --- a/tests/lean/331.lean.expected.out +++ b/tests/lean/331.lean.expected.out @@ -1,6 +1,6 @@ -331.lean:6:9-6:10: error: Failed to infer type of binder `x` +331.lean:6:9-6:10: error(lean.inferBinderTypeFailed): Failed to infer type of binder `x` -Note: When the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed -331.lean:7:9-7:10: error: Failed to infer type of binder `x` +Note: Because this declaration's type has been explicitly provided, all parameter types and holes (e.g., `_`) in its header are resolved before its body is processed; information from the declaration body cannot be used to infer what these values should be +331.lean:7:9-7:10: error(lean.inferBinderTypeFailed): Failed to infer type of binder `x` -Note: When the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed +Note: Because this declaration's type has been explicitly provided, all parameter types and holes (e.g., `_`) in its header are resolved before its body is processed; information from the declaration body cannot be used to infer what these values should be diff --git a/tests/lean/346.lean.expected.out b/tests/lean/346.lean.expected.out index 0b1ea4b101..10f5e04728 100644 --- a/tests/lean/346.lean.expected.out +++ b/tests/lean/346.lean.expected.out @@ -1,4 +1,4 @@ -346.lean:10:6-10:16: error: unknown constant 'SomeType.b' +346.lean:10:6-10:16: error(lean.unknownIdentifier): Unknown constant `SomeType.b` 346.lean:13:2-13:5: error: Invalid field `z`: The environment does not contain `Nat.z` x has type diff --git a/tests/lean/435.lean.expected.out b/tests/lean/435.lean.expected.out index bba3989fdc..8260965b93 100644 --- a/tests/lean/435.lean.expected.out +++ b/tests/lean/435.lean.expected.out @@ -1,2 +1,4 @@ 435.lean:3:0-3:7: warning: declaration uses 'sorry' -435.lean:5:21-5:23: error: unknown identifier 'op' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check. +435.lean:5:21-5:23: error: Unknown identifier `op` at quotation precheck + +Note: You can use `set_option quotPrecheck false` to disable this check. diff --git a/tests/lean/586.lean.expected.out b/tests/lean/586.lean.expected.out index 4ff6ac93cd..466a3f97db 100644 --- a/tests/lean/586.lean.expected.out +++ b/tests/lean/586.lean.expected.out @@ -1,4 +1,4 @@ Nat.zero : Nat `Nat.succ : Lean.Name -586.lean:13:0-13:3: error: unknown identifier 'zero✝' -586.lean:13:0-13:3: error: unknown constant 'succ✝' +586.lean:13:0-13:3: error(lean.unknownIdentifier): Unknown identifier `zero✝` +586.lean:13:0-13:3: error(lean.unknownIdentifier): Unknown constant `succ✝` diff --git a/tests/lean/593.lean.expected.out b/tests/lean/593.lean.expected.out index fdaa9b7591..80aeea1bff 100644 --- a/tests/lean/593.lean.expected.out +++ b/tests/lean/593.lean.expected.out @@ -1,8 +1,8 @@ Foo.Bar.bar : Nat Foo.Bar.bar : Nat Foo.Bar.bar : Nat -593.lean:21:7-21:10: error: unknown identifier 'boo' -593.lean:26:7-26:10: error: unknown identifier 'bar' +593.lean:21:7-21:10: error(lean.unknownIdentifier): Unknown identifier `boo` +593.lean:26:7-26:10: error(lean.unknownIdentifier): Unknown identifier `bar` Foo.boo : Nat Foo.Bar.bar : Nat Foo.Bar.bar : Nat diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out index d24c1f4c28..a8bba34230 100644 --- a/tests/lean/StxQuot.lean.expected.out +++ b/tests/lean/StxQuot.lean.expected.out @@ -40,19 +40,23 @@ StxQuot.lean:19:15-19:16: error: unexpected token ']'; expected term "(Term.match\n \"match\"\n []\n []\n [(Term.matchDiscr [] `a._@.UnhygienicMain._hyg.1)]\n \"with\"\n (Term.matchAlts\n [(Term.matchAlt \"|\" [[`a._@.UnhygienicMain._hyg.1]] \"=>\" `b._@.UnhygienicMain._hyg.1)\n (Term.matchAlt\n \"|\"\n [[(«term_+_» `a._@.UnhygienicMain._hyg.1 \"+\" (num \"1\"))]]\n \"=>\"\n («term_+_» `b._@.UnhygienicMain._hyg.1 \"+\" (num \"1\")))]))" "#[`a._@.UnhygienicMain._hyg.1, `b._@.UnhygienicMain._hyg.1]" "1" -StxQuot.lean:83:7-83:19: error: unknown identifier 'sufficesDecl' +StxQuot.lean:83:7-83:19: error(lean.unknownIdentifier): Unknown identifier `sufficesDecl` "(Term.sufficesDecl\n (hygieneInfo `_@.UnhygienicMain._hyg.1)\n `x._@.UnhygienicMain._hyg.1\n (Term.fromTerm \"from\" `x._@.UnhygienicMain._hyg.1))" "#[(num \"1\"), [(num \"2\") (num \"3\")], (num \"4\")]" "#[(num \"2\")]" StxQuot.lean:97:39-97:44: error: unexpected antiquotation splice fun x => sorry : (x : ?m) → ?m x "#[(some 1), (some 2)]" -StxQuot.lean:104:13-104:14: error: unknown identifier 'x' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check. +StxQuot.lean:104:13-104:14: error: Unknown identifier `x` at quotation precheck + +Note: You can use `set_option quotPrecheck false` to disable this check. "`id._@.UnhygienicMain._hyg.1" "`pure._@.UnhygienicMain._hyg.1" "(termFoo_ \"foo\" )" "(Term.fun \"fun\" (Term.basicFun [`x._@.UnhygienicMain._hyg.1] [] \"=>\" `x._@.UnhygienicMain._hyg.1))" -StxQuot.lean:110:22-110:23: error: unknown identifier 'y' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check. +StxQuot.lean:110:22-110:23: error: Unknown identifier `y` at quotation precheck + +Note: You can use `set_option quotPrecheck false` to disable this check. "(Term.fun\n \"fun\"\n (Term.basicFun\n [`x._@.UnhygienicMain._hyg.1 `y._@.UnhygienicMain._hyg.1]\n []\n \"=>\"\n (Term.app `x._@.UnhygienicMain._hyg.1 [`y._@.UnhygienicMain._hyg.1])))" "(Term.fun\n \"fun\"\n (Term.basicFun\n [(Term.anonymousCtor \"⟨\" [`x._@.UnhygienicMain._hyg.1 \",\" `y._@.UnhygienicMain._hyg.1] \"⟩\")]\n []\n \"=>\"\n `x._@.UnhygienicMain._hyg.1))" "1" diff --git a/tests/lean/autoBoundImplicits1.lean.expected.out b/tests/lean/autoBoundImplicits1.lean.expected.out index 746bc0f04a..5534524e25 100644 --- a/tests/lean/autoBoundImplicits1.lean.expected.out +++ b/tests/lean/autoBoundImplicits1.lean.expected.out @@ -1,13 +1,13 @@ myid 10 : Nat myid true : Bool autoBoundImplicits1.lean:16:4-16:11: warning: declaration uses 'sorry' -autoBoundImplicits1.lean:20:25-20:29: error: unknown identifier 'size' -autoBoundImplicits1.lean:24:23-24:24: error: unknown identifier 'α' -autoBoundImplicits1.lean:24:25-24:26: error: unknown identifier 'n' -autoBoundImplicits1.lean:24:33-24:34: error: unknown identifier 'α' -autoBoundImplicits1.lean:24:37-24:38: error: unknown identifier 'β' -autoBoundImplicits1.lean:24:46-24:47: error: unknown identifier 'β' -autoBoundImplicits1.lean:24:48-24:49: error: unknown identifier 'n' +autoBoundImplicits1.lean:20:25-20:29: error(lean.unknownIdentifier): Unknown identifier `size` +autoBoundImplicits1.lean:24:23-24:24: error(lean.unknownIdentifier): Unknown identifier `α` +autoBoundImplicits1.lean:24:25-24:26: error(lean.unknownIdentifier): Unknown identifier `n` +autoBoundImplicits1.lean:24:33-24:34: error(lean.unknownIdentifier): Unknown identifier `α` +autoBoundImplicits1.lean:24:37-24:38: error(lean.unknownIdentifier): Unknown identifier `β` +autoBoundImplicits1.lean:24:46-24:47: error(lean.unknownIdentifier): Unknown identifier `β` +autoBoundImplicits1.lean:24:48-24:49: error(lean.unknownIdentifier): Unknown identifier `n` f {α : Type} {n : Nat} (xs : Vec α n) : Vec α n f mkVec : Vec ?m 0 f mkVec : Vec Nat 0 diff --git a/tests/lean/autoImplicitCtorParamIssue.lean.expected.out b/tests/lean/autoImplicitCtorParamIssue.lean.expected.out index ccc35cd50a..fec9391aa8 100644 --- a/tests/lean/autoImplicitCtorParamIssue.lean.expected.out +++ b/tests/lean/autoImplicitCtorParamIssue.lean.expected.out @@ -1,3 +1,3 @@ -autoImplicitCtorParamIssue.lean:1:9-1:10: error: Failed to infer type of binder `x` -autoImplicitCtorParamIssue.lean:4:9-4:10: error: Failed to infer type of binder `x` -autoImplicitCtorParamIssue.lean:7:7-7:8: error: Failed to infer type of binder `x` +autoImplicitCtorParamIssue.lean:1:9-1:10: error(lean.inferBinderTypeFailed): Failed to infer type of binder `x` +autoImplicitCtorParamIssue.lean:4:9-4:10: error(lean.inferBinderTypeFailed): Failed to infer type of binder `x` +autoImplicitCtorParamIssue.lean:7:7-7:8: error(lean.inferBinderTypeFailed): Failed to infer type of binder `x` diff --git a/tests/lean/autoImplicitForbidden.lean.expected.out b/tests/lean/autoImplicitForbidden.lean.expected.out index dc28113019..265bb98293 100644 --- a/tests/lean/autoImplicitForbidden.lean.expected.out +++ b/tests/lean/autoImplicitForbidden.lean.expected.out @@ -1,7 +1,7 @@ -autoImplicitForbidden.lean:1:8-1:9: error: unknown identifier 'f' -autoImplicitForbidden.lean:6:10-6:11: error: unknown identifier 'h' -autoImplicitForbidden.lean:13:24-13:27: error: unknown identifier 'Bla' -autoImplicitForbidden.lean:16:21-16:24: error: unknown identifier 'Foo' -autoImplicitForbidden.lean:20:18-20:21: error: unknown identifier 'Ex2' -autoImplicitForbidden.lean:28:14-28:20: error: unknown identifier 'foobar' +autoImplicitForbidden.lean:1:8-1:9: error(lean.unknownIdentifier): Unknown identifier `f` +autoImplicitForbidden.lean:6:10-6:11: error(lean.unknownIdentifier): Unknown identifier `h` +autoImplicitForbidden.lean:13:24-13:27: error(lean.unknownIdentifier): Unknown identifier `Bla` +autoImplicitForbidden.lean:16:21-16:24: error(lean.unknownIdentifier): Unknown identifier `Foo` +autoImplicitForbidden.lean:20:18-20:21: error(lean.unknownIdentifier): Unknown identifier `Ex2` +autoImplicitForbidden.lean:28:14-28:20: error(lean.unknownIdentifier): Unknown identifier `foobar` constructor Bar.mk.{u_1} : ({Na : Sort u_1} → Na) → Nat → Bar diff --git a/tests/lean/autobound_and_macroscopes.lean.expected.out b/tests/lean/autobound_and_macroscopes.lean.expected.out index 541c623c57..d50cd083e3 100644 --- a/tests/lean/autobound_and_macroscopes.lean.expected.out +++ b/tests/lean/autobound_and_macroscopes.lean.expected.out @@ -1,2 +1,2 @@ -autobound_and_macroscopes.lean:2:15-2:16: error: unknown identifier 'x✝' -autobound_and_macroscopes.lean:2:19-2:20: error: unknown identifier 'x✝' +autobound_and_macroscopes.lean:2:15-2:16: error(lean.unknownIdentifier): Unknown identifier `x✝` +autobound_and_macroscopes.lean:2:19-2:20: error(lean.unknownIdentifier): Unknown identifier `x✝` diff --git a/tests/lean/binopQuotPrecheck.lean.expected.out b/tests/lean/binopQuotPrecheck.lean.expected.out index d44244f04a..6ba6232408 100644 --- a/tests/lean/binopQuotPrecheck.lean.expected.out +++ b/tests/lean/binopQuotPrecheck.lean.expected.out @@ -1,3 +1,9 @@ -binopQuotPrecheck.lean:56:41-56:42: error: unknown identifier 'a' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check. -binopQuotPrecheck.lean:61:49-61:50: error: unknown identifier 'a' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check. -binopQuotPrecheck.lean:66:51-66:52: error: unknown identifier 'a' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check. +binopQuotPrecheck.lean:56:41-56:42: error: Unknown identifier `a` at quotation precheck + +Note: You can use `set_option quotPrecheck false` to disable this check. +binopQuotPrecheck.lean:61:49-61:50: error: Unknown identifier `a` at quotation precheck + +Note: You can use `set_option quotPrecheck false` to disable this check. +binopQuotPrecheck.lean:66:51-66:52: error: Unknown identifier `a` at quotation precheck + +Note: You can use `set_option quotPrecheck false` to disable this check. diff --git a/tests/lean/deprecated.lean.expected.out b/tests/lean/deprecated.lean.expected.out index 277e66a18c..92265c534e 100644 --- a/tests/lean/deprecated.lean.expected.out +++ b/tests/lean/deprecated.lean.expected.out @@ -5,8 +5,8 @@ deprecated.lean:11:6-11:7: warning: `f` has been deprecated: use `g` instead 2 deprecated.lean:13:6-13:7: warning: `h` has been deprecated 1 -deprecated.lean:15:13-15:15: error: unknown constant 'g1' -deprecated.lean:23:13-23:15: error: unknown constant 'g1' +deprecated.lean:15:13-15:15: error(lean.unknownIdentifier): Unknown constant `g1` +deprecated.lean:23:13-23:15: error(lean.unknownIdentifier): Unknown constant `g1` deprecated.lean:27:2-27:55: warning: `[deprecated]` attribute should specify the date or library version at which the deprecation was introduced, using `(since := "...")` deprecated.lean:30:6-30:8: warning: `f2` has been deprecated: use `Foo.g1` instead 2 diff --git a/tests/lean/ellipsisProjIssue.lean.expected.out b/tests/lean/ellipsisProjIssue.lean.expected.out index 9099e037a3..4727cff63d 100644 --- a/tests/lean/ellipsisProjIssue.lean.expected.out +++ b/tests/lean/ellipsisProjIssue.lean.expected.out @@ -1,4 +1,4 @@ -ellipsisProjIssue.lean:1:18-1:22: error: unknown identifier 'succ' +ellipsisProjIssue.lean:1:18-1:22: error(lean.unknownIdentifier): Unknown identifier `succ` { lower := Nat.add, upper := sorry } : Std.PRange { lower := Std.PRange.BoundShape.closed, upper := Std.PRange.BoundShape.open } diff --git a/tests/lean/evalLeak.lean.expected.out b/tests/lean/evalLeak.lean.expected.out index 002b338ead..95cc28dfd4 100644 --- a/tests/lean/evalLeak.lean.expected.out +++ b/tests/lean/evalLeak.lean.expected.out @@ -1,4 +1,4 @@ false foo : Bool -evalLeak.lean:22:7-22:20: error: unknown identifier '_eval.match_1' -evalLeak.lean:23:7-23:20: error: unknown identifier '_eval.match_2' +evalLeak.lean:22:7-22:20: error(lean.unknownIdentifier): Unknown identifier `_eval.match_1` +evalLeak.lean:23:7-23:20: error(lean.unknownIdentifier): Unknown identifier `_eval.match_2` diff --git a/tests/lean/funind_errors.lean.expected.out b/tests/lean/funind_errors.lean.expected.out index 6e9d9f21b7..93ac09e68a 100644 --- a/tests/lean/funind_errors.lean.expected.out +++ b/tests/lean/funind_errors.lean.expected.out @@ -1,5 +1,5 @@ -funind_errors.lean:4:7-4:26: error: unknown identifier 'doesNotExist.induct' -funind_errors.lean:22:7-22:23: error: unknown constant 'takeWhile.induct' +funind_errors.lean:4:7-4:26: error(lean.unknownIdentifier): Unknown identifier `doesNotExist.induct` +funind_errors.lean:22:7-22:23: error(lean.unknownIdentifier): Unknown constant `takeWhile.induct` takeWhile.foo.induct.{u_1} {α : Type u_1} (p : α → Bool) (as : Array α) (motive : Nat → Array α → Prop) (case1 : ∀ (i : Nat) (r : Array α) (h : i < as.size), @@ -10,5 +10,5 @@ takeWhile.foo.induct.{u_1} {α : Type u_1} (p : α → Bool) (as : Array α) (mo have a := as.get i h; ¬p a = true → motive i r) (case3 : ∀ (i : Nat) (r : Array α), ¬i < as.size → motive i r) (i : Nat) (r : Array α) : motive i r -funind_errors.lean:38:7-38:20: error: unknown constant 'idEven.induct' -funind_errors.lean:45:7-45:19: error: unknown constant 'idAcc.induct' +funind_errors.lean:38:7-38:20: error(lean.unknownIdentifier): Unknown constant `idEven.induct` +funind_errors.lean:45:7-45:19: error(lean.unknownIdentifier): Unknown constant `idAcc.induct` diff --git a/tests/lean/holeErrors.lean.expected.out b/tests/lean/holeErrors.lean.expected.out index 076f73d547..e2ed6d88f1 100644 --- a/tests/lean/holeErrors.lean.expected.out +++ b/tests/lean/holeErrors.lean.expected.out @@ -2,22 +2,22 @@ holeErrors.lean:3:14-3:20: error: don't know how to synthesize implicit argument @id ?m context: ⊢ Sort u -holeErrors.lean:3:4-3:10: error: Failed to infer type of definition `f1.{u}` -holeErrors.lean:5:9-5:10: error: Failed to infer type of definition `f2` +holeErrors.lean:3:4-3:10: error(lean.inferDefTypeFailed): Failed to infer type of definition `f1.{u}` +holeErrors.lean:5:9-5:10: error(lean.inferDefTypeFailed): Failed to infer type of definition `f2` -Note: When the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed +Note: Because this declaration's type has been explicitly provided, all parameter types and holes (e.g., `_`) in its header are resolved before its body is processed; information from the declaration body cannot be used to infer what these values should be holeErrors.lean:8:9-8:15: error: don't know how to synthesize implicit argument 'α' @id ?m context: ⊢ Sort u holeErrors.lean:8:4-8:5: error: failed to infer 'let' declaration type -holeErrors.lean:7:4-7:10: error: Failed to infer type of definition `f3.{u}` -holeErrors.lean:11:4-11:6: error: Failed to infer type of definition `f4` -holeErrors.lean:11:8-11:9: error: Failed to infer type of binder `x` -holeErrors.lean:13:4-13:6: error: Failed to infer type of definition `f5` -holeErrors.lean:13:8-13:9: error: Failed to infer type of binder `x` -holeErrors.lean:16:4-16:5: error: Failed to infer type of binder `x` -holeErrors.lean:15:4-15:6: error: Failed to infer type of definition `f6` +holeErrors.lean:7:4-7:10: error(lean.inferDefTypeFailed): Failed to infer type of definition `f3.{u}` +holeErrors.lean:11:4-11:6: error(lean.inferDefTypeFailed): Failed to infer type of definition `f4` +holeErrors.lean:11:8-11:9: error(lean.inferBinderTypeFailed): Failed to infer type of binder `x` +holeErrors.lean:13:4-13:6: error(lean.inferDefTypeFailed): Failed to infer type of definition `f5` +holeErrors.lean:13:8-13:9: error(lean.inferBinderTypeFailed): Failed to infer type of binder `x` +holeErrors.lean:16:4-16:5: error(lean.inferBinderTypeFailed): Failed to infer type of binder `x` +holeErrors.lean:15:4-15:6: error(lean.inferDefTypeFailed): Failed to infer type of definition `f6` holeErrors.lean:19:13-19:19: error: don't know how to synthesize implicit argument 'α' @id ?m context: diff --git a/tests/lean/holes.lean.expected.out b/tests/lean/holes.lean.expected.out index 1a5ebfdffe..fde68929d6 100644 --- a/tests/lean/holes.lean.expected.out +++ b/tests/lean/holes.lean.expected.out @@ -20,14 +20,14 @@ holes.lean:10:9-10:12: error: don't know how to synthesize implicit argument 'β context: x : Nat ⊢ Type -holes.lean:13:10-13:11: error: Failed to infer type of binder `β` -holes.lean:15:12-15:13: error: Failed to infer type of binder `β` +holes.lean:13:10-13:11: error(lean.inferBinderTypeFailed): Failed to infer type of binder `β` +holes.lean:15:12-15:13: error(lean.inferBinderTypeFailed): Failed to infer type of binder `β` holes.lean:19:0-19:3: error: don't know how to synthesize implicit argument 'β' @f Nat (?m a) a context: a : Nat f : {α : Type} → {β : ?m a} → α → α := ⋯ ⊢ ?m a -holes.lean:18:9-18:10: error: Failed to infer type of binder `β` -holes.lean:21:12-21:14: error: Failed to infer type of definition `f7` +holes.lean:18:9-18:10: error(lean.inferBinderTypeFailed): Failed to infer type of binder `β` +holes.lean:21:12-21:14: error(lean.inferDefTypeFailed): Failed to infer type of definition `f7` holes.lean:25:8-25:11: error: failed to infer 'let rec' declaration type diff --git a/tests/lean/hygienicIntro.lean.expected.out b/tests/lean/hygienicIntro.lean.expected.out index be671c9fc0..c13c3709e0 100644 --- a/tests/lean/hygienicIntro.lean.expected.out +++ b/tests/lean/hygienicIntro.lean.expected.out @@ -1,3 +1,3 @@ -hygienicIntro.lean:14:6-14:9: error: unknown identifier 'a_1' -hygienicIntro.lean:24:20-24:21: error: unknown identifier 'h' -hygienicIntro.lean:25:8-25:9: error: unknown identifier 'h' +hygienicIntro.lean:14:6-14:9: error(lean.unknownIdentifier): Unknown identifier `a_1` +hygienicIntro.lean:24:20-24:21: error(lean.unknownIdentifier): Unknown identifier `h` +hygienicIntro.lean:25:8-25:9: error(lean.unknownIdentifier): Unknown identifier `h` diff --git a/tests/lean/implicitTypePos.lean.expected.out b/tests/lean/implicitTypePos.lean.expected.out index ba2a3c3c6d..108055a1cd 100644 --- a/tests/lean/implicitTypePos.lean.expected.out +++ b/tests/lean/implicitTypePos.lean.expected.out @@ -1,5 +1,5 @@ -implicitTypePos.lean:1:8-1:9: error: Failed to infer type of binder `y` -implicitTypePos.lean:1:6-1:7: error: Failed to infer type of binder `x` -implicitTypePos.lean:3:9-3:10: error: Failed to infer type of binder `y` -implicitTypePos.lean:5:9-5:10: error: Failed to infer type of binder `β` -implicitTypePos.lean:7:10-7:11: error: Failed to infer type of binder `β` +implicitTypePos.lean:1:8-1:9: error(lean.inferBinderTypeFailed): Failed to infer type of binder `y` +implicitTypePos.lean:1:6-1:7: error(lean.inferBinderTypeFailed): Failed to infer type of binder `x` +implicitTypePos.lean:3:9-3:10: error(lean.inferBinderTypeFailed): Failed to infer type of binder `y` +implicitTypePos.lean:5:9-5:10: error(lean.inferBinderTypeFailed): Failed to infer type of binder `β` +implicitTypePos.lean:7:10-7:11: error(lean.inferBinderTypeFailed): Failed to infer type of binder `β` diff --git a/tests/lean/inductionErrors.lean.expected.out b/tests/lean/inductionErrors.lean.expected.out index c75460c21d..2be6752028 100644 --- a/tests/lean/inductionErrors.lean.expected.out +++ b/tests/lean/inductionErrors.lean.expected.out @@ -6,7 +6,7 @@ inductionErrors.lean:12:12-12:27: error: unsolved goals case upper.h q d : Nat ⊢ q + d.succ > q -inductionErrors.lean:16:19-16:26: error: unknown identifier 'elimEx2' +inductionErrors.lean:16:19-16:26: error(lean.unknownIdentifier): Unknown identifier `elimEx2` inductionErrors.lean:22:2-25:45: error: insufficient number of targets for 'elimEx' inductionErrors.lean:28:16-28:23: error: expected resulting type of eliminator to be an application of one of its parameters (the motive): Nat diff --git a/tests/lean/inductive1.lean.expected.out b/tests/lean/inductive1.lean.expected.out index f05dbe1f27..1ef7160fad 100644 --- a/tests/lean/inductive1.lean.expected.out +++ b/tests/lean/inductive1.lean.expected.out @@ -28,4 +28,4 @@ inductive1.lean:108:7-108:10: error(lean.ctorResultingTypeMismatch): Unexpected T1 but found Nat -inductive1.lean:118:7-118:11: error: unknown identifier 'cons' +inductive1.lean:118:7-118:11: error(lean.unknownIdentifier): Unknown identifier `cons` diff --git a/tests/lean/interactive/editAfterError.lean.expected.out b/tests/lean/interactive/editAfterError.lean.expected.out index 0fb95fcbee..7556d45552 100644 --- a/tests/lean/interactive/editAfterError.lean.expected.out +++ b/tests/lean/interactive/editAfterError.lean.expected.out @@ -5,14 +5,15 @@ "severity": 1, "range": {"start": {"line": 0, "character": 7}, "end": {"line": 0, "character": 10}}, - "message": "unknown identifier 'tru'", + "message": "Unknown identifier `tru`", "fullRange": - {"start": {"line": 0, "character": 7}, "end": {"line": 0, "character": 10}}}, + {"start": {"line": 0, "character": 7}, "end": {"line": 0, "character": 10}}, + "code": "lean.unknownIdentifier"}, {"source": "Lean 4", "severity": 1, "range": {"start": {"line": 1, "character": 7}, "end": {"line": 1, "character": 11}}, - "message": "unknown identifier 'fals'", + "message": "Unknown identifier `fals`", "fullRange": - {"start": {"line": 1, "character": 7}, - "end": {"line": 1, "character": 11}}}]} + {"start": {"line": 1, "character": 7}, "end": {"line": 1, "character": 11}}, + "code": "lean.unknownIdentifier"}]} diff --git a/tests/lean/interactive/incrementalMutual.lean.expected.out b/tests/lean/interactive/incrementalMutual.lean.expected.out index 1b5e9b20af..4b4a9c3e9d 100644 --- a/tests/lean/interactive/incrementalMutual.lean.expected.out +++ b/tests/lean/interactive/incrementalMutual.lean.expected.out @@ -36,15 +36,15 @@ so 1.5 "severity": 1, "range": {"start": {"line": 2, "character": 16}, "end": {"line": 2, "character": 28}}, - "message": "unknown identifier 'doesNotExist'", + "message": "Unknown identifier `doesNotExist`", "fullRange": - {"start": {"line": 2, "character": 16}, - "end": {"line": 2, "character": 28}}}, + {"start": {"line": 2, "character": 16}, "end": {"line": 2, "character": 28}}, + "code": "lean.unknownIdentifier"}, {"source": "Lean 4", "severity": 1, "range": {"start": {"line": 3, "character": 16}, "end": {"line": 3, "character": 28}}, - "message": "unknown identifier 'doesNotExist'", + "message": "Unknown identifier `doesNotExist`", "fullRange": - {"start": {"line": 3, "character": 16}, - "end": {"line": 3, "character": 28}}}]} + {"start": {"line": 3, "character": 16}, "end": {"line": 3, "character": 28}}, + "code": "lean.unknownIdentifier"}]} diff --git a/tests/lean/interactive/incrementalTactic.lean.expected.out b/tests/lean/interactive/incrementalTactic.lean.expected.out index 8574242a41..5944736e65 100644 --- a/tests/lean/interactive/incrementalTactic.lean.expected.out +++ b/tests/lean/interactive/incrementalTactic.lean.expected.out @@ -45,9 +45,10 @@ t 2 "severity": 1, "range": {"start": {"line": 2, "character": 9}, "end": {"line": 2, "character": 11}}, - "message": "unknown identifier 'no'", + "message": "Unknown identifier `no`", "fullRange": - {"start": {"line": 2, "character": 9}, "end": {"line": 2, "character": 11}}}, + {"start": {"line": 2, "character": 9}, "end": {"line": 2, "character": 11}}, + "code": "lean.unknownIdentifier"}, {"source": "Lean 4", "severity": 1, "range": @@ -121,7 +122,7 @@ s "severity": 1, "range": {"start": {"line": 3, "character": 8}, "end": {"line": 3, "character": 21}}, - "message": "unknown identifier 'noSuchTheorem'", + "message": "Unknown identifier `noSuchTheorem`", "fullRange": - {"start": {"line": 3, "character": 8}, - "end": {"line": 3, "character": 21}}}]} + {"start": {"line": 3, "character": 8}, "end": {"line": 3, "character": 21}}, + "code": "lean.unknownIdentifier"}]} diff --git a/tests/lean/letrec1.lean.expected.out b/tests/lean/letrec1.lean.expected.out index 048a8bbe8a..d876f4b465 100644 --- a/tests/lean/letrec1.lean.expected.out +++ b/tests/lean/letrec1.lean.expected.out @@ -1,4 +1,4 @@ letrec1.lean:6:0-9:7: error: 'f1.g' has already been declared -letrec1.lean:18:35-18:36: error: unknown identifier 'g' +letrec1.lean:18:35-18:36: error(lean.unknownIdentifier): Unknown identifier `g` letrec1.lean:27:8-27:9: error: invalid type in 'let rec', it uses 'f' which is being defined simultaneously letrec1.lean:37:10-37:11: error: invalid type in 'let rec', it uses 'g' which is being defined simultaneously diff --git a/tests/lean/macroStack.lean.expected.out b/tests/lean/macroStack.lean.expected.out index 54ddfbb8c8..3feaee8527 100644 --- a/tests/lean/macroStack.lean.expected.out +++ b/tests/lean/macroStack.lean.expected.out @@ -1,5 +1,5 @@ -macroStack.lean:4:5-4:6: error: unknown identifier 'x' -macroStack.lean:8:6-8:7: error: unknown identifier 'x' +macroStack.lean:4:5-4:6: error(lean.unknownIdentifier): Unknown identifier `x` +macroStack.lean:8:6-8:7: error: Unknown identifier `x` with resulting expansion binrel% GT.gt✝ x 0 while expanding diff --git a/tests/lean/moduleOf.lean.expected.out b/tests/lean/moduleOf.lean.expected.out index b635affac1..aa7317fb4e 100644 --- a/tests/lean/moduleOf.lean.expected.out +++ b/tests/lean/moduleOf.lean.expected.out @@ -4,4 +4,4 @@ (some Std.Data.HashMap.Basic) none none -moduleOf.lean:16:0-16:5: error: unknown constant 'foo' +moduleOf.lean:16:0-16:5: error: Unknown constant `foo` diff --git a/tests/lean/multiConstantError.lean.expected.out b/tests/lean/multiConstantError.lean.expected.out index f5fa211466..73400c4f8f 100644 --- a/tests/lean/multiConstantError.lean.expected.out +++ b/tests/lean/multiConstantError.lean.expected.out @@ -1,9 +1,9 @@ -multiConstantError.lean:1:11-1:12: error: Failed to infer type of binder `c` +multiConstantError.lean:1:11-1:12: error(lean.inferBinderTypeFailed): Failed to infer type of binder `c` -Note: Recall that you cannot declare multiple constants in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`. -multiConstantError.lean:1:9-1:10: error: Failed to infer type of binder `b` +Note: Multiple constants cannot be declared in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`. +multiConstantError.lean:1:9-1:10: error(lean.inferBinderTypeFailed): Failed to infer type of binder `b` -Note: Recall that you cannot declare multiple constants in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`. -multiConstantError.lean:3:9-3:10: error: Failed to infer type of binder `α` +Note: Multiple constants cannot be declared in a single declaration. The identifier(s) `b`, `c` are being interpreted as parameters `(b : _)`, `(c : _)`. +multiConstantError.lean:3:9-3:10: error(lean.inferBinderTypeFailed): Failed to infer type of binder `α` -Note: Recall that you cannot declare multiple constants in a single declaration. The identifier(s) `α`, `β` are being interpreted as parameters `(α : _)`, `(β : _)`. +Note: Multiple constants cannot be declared in a single declaration. The identifier(s) `α`, `β` are being interpreted as parameters `(α : _)`, `(β : _)`. diff --git a/tests/lean/notationPrecheck.lean.expected.out b/tests/lean/notationPrecheck.lean.expected.out index 5efe2b55c6..b468b6c3d7 100644 --- a/tests/lean/notationPrecheck.lean.expected.out +++ b/tests/lean/notationPrecheck.lean.expected.out @@ -1,4 +1,6 @@ -notationPrecheck.lean:1:25-1:26: error: unknown identifier 'a' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check. +notationPrecheck.lean:1:25-1:26: error: Unknown identifier `a` at quotation precheck + +Note: You can use `set_option quotPrecheck false` to disable this check. notationPrecheck.lean:4:16-4:19: error: no macro or `[quot_precheck]` instance for syntax kind 'termB_' found b x This means we cannot eagerly check your notation/quotation for unbound identifiers; you can use `set_option quotPrecheck false` to disable this check. @@ -6,7 +8,11 @@ notationPrecheck.lean:8:7-8:8: error: elaboration function for 'termB_' has not b x✝ notationPrecheck.lean:13:27-13:32: error: ambiguous notation with at least one interpretation that failed quotation precheck, possible interpretations («term_∧__1» `x "∧" `y) - unknown identifier 'y' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check. + Unknown identifier `y` at quotation precheck + + Note: You can use `set_option quotPrecheck false` to disable this check. («term_∧_» `x "∧" `y) - unknown identifier 'y' at quotation precheck; you can use `set_option quotPrecheck false` to disable this check. + Unknown identifier `y` at quotation precheck + + Note: You can use `set_option quotPrecheck false` to disable this check. diff --git a/tests/lean/openExport.lean.expected.out b/tests/lean/openExport.lean.expected.out index 298c8e9481..7d92ca0c85 100644 --- a/tests/lean/openExport.lean.expected.out +++ b/tests/lean/openExport.lean.expected.out @@ -3,8 +3,8 @@ B.y : Nat A.x : Nat A.x : Nat B.y : Nat -openExport.lean:19:7-19:8: error: unknown identifier 'x' -openExport.lean:20:7-20:8: error: unknown identifier 'y' +openExport.lean:19:7-19:8: error(lean.unknownIdentifier): Unknown identifier `x` +openExport.lean:20:7-20:8: error(lean.unknownIdentifier): Unknown identifier `y` A.x : Nat B.y : Nat A.x : Nat diff --git a/tests/lean/openScoped.lean.expected.out b/tests/lean/openScoped.lean.expected.out index 6e577a1b20..298c8e99d3 100644 --- a/tests/lean/openScoped.lean.expected.out +++ b/tests/lean/openScoped.lean.expected.out @@ -1,8 +1,8 @@ -openScoped.lean:1:7-1:14: error: unknown identifier 'epsilon' +openScoped.lean:1:7-1:14: error(lean.unknownIdentifier): Unknown identifier `epsilon` openScoped.lean:4:2-4:24: error: failed to synthesize Decidable (f = g) Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command. Classical.epsilon.{u} {α : Sort u} [h : Nonempty α] (p : α → Prop) : α -openScoped.lean:15:7-15:14: error: unknown identifier 'epsilon' -openScoped.lean:20:7-20:14: error: unknown identifier 'epsilon' +openScoped.lean:15:7-15:14: error(lean.unknownIdentifier): Unknown identifier `epsilon` +openScoped.lean:20:7-20:14: error(lean.unknownIdentifier): Unknown identifier `epsilon` diff --git a/tests/lean/parserRecovery.lean.expected.out b/tests/lean/parserRecovery.lean.expected.out index fa6cbd293d..038a161db2 100644 --- a/tests/lean/parserRecovery.lean.expected.out +++ b/tests/lean/parserRecovery.lean.expected.out @@ -27,7 +27,7 @@ parserRecovery.lean:42:9-42:12: error: unexpected token; expected identifier parserRecovery.lean:42:14: error: expected token parserRecovery.lean:44:9-44:11: error: unexpected token '!'; expected identifier parserRecovery.lean:45:4: error: expected token -parserRecovery.lean:47:6-47:11: error: unknown identifier 'Foo.a' +parserRecovery.lean:47:6-47:11: error(lean.unknownIdentifier): Unknown identifier `Foo.a` parserRecovery.lean:49:16-49:17: error: unexpected token; expected identifier parserRecovery.lean:49:18-49:20: error: unexpected token; expected identifier parserRecovery.lean:49:21-49:23: error: unexpected token; expected identifier diff --git a/tests/lean/protected.lean.expected.out b/tests/lean/protected.lean.expected.out index 76fa2adca3..bd5d89e310 100644 --- a/tests/lean/protected.lean.expected.out +++ b/tests/lean/protected.lean.expected.out @@ -1,11 +1,11 @@ -protected.lean:10:7-10:8: error: unknown identifier 'x' +protected.lean:10:7-10:8: error(lean.unknownIdentifier): Unknown identifier `x` Foo.x : Nat Bla.Foo.y : Nat -protected.lean:22:7-22:8: error: unknown identifier 'y' +protected.lean:22:7-22:8: error(lean.unknownIdentifier): Unknown identifier `y` Bla.Foo.z : Nat protected.lean:25:14-25:15: error: protected declarations must be in a namespace -protected.lean:28:14-28:15: error: unknown identifier 'f' +protected.lean:28:14-28:15: error(lean.unknownIdentifier): Unknown identifier `f` 8 -protected.lean:38:14-38:15: error: unknown identifier 'g' -protected.lean:47:6-47:7: error: unknown identifier 'g' +protected.lean:38:14-38:15: error(lean.unknownIdentifier): Unknown identifier `g` +protected.lean:47:6-47:7: error(lean.unknownIdentifier): Unknown identifier `g` 8 diff --git a/tests/lean/protectedAlias.lean.expected.out b/tests/lean/protectedAlias.lean.expected.out index 20030271b3..3ca813a344 100644 --- a/tests/lean/protectedAlias.lean.expected.out +++ b/tests/lean/protectedAlias.lean.expected.out @@ -1,2 +1,2 @@ Nat.double (x : Nat) : Nat -protectedAlias.lean:9:7-9:13: error: unknown identifier 'double' +protectedAlias.lean:9:7-9:13: error(lean.unknownIdentifier): Unknown identifier `double` diff --git a/tests/lean/renameBug.lean.expected.out b/tests/lean/renameBug.lean.expected.out index 20cff35631..1b77eafb72 100644 --- a/tests/lean/renameBug.lean.expected.out +++ b/tests/lean/renameBug.lean.expected.out @@ -1 +1 @@ -renameBug.lean:3:13-3:14: error: unknown identifier 'c' +renameBug.lean:3:13-3:14: error(lean.unknownIdentifier): Unknown identifier `c` diff --git a/tests/lean/root.lean.expected.out b/tests/lean/root.lean.expected.out index 7eac01396c..c03ae430e3 100644 --- a/tests/lean/root.lean.expected.out +++ b/tests/lean/root.lean.expected.out @@ -4,8 +4,8 @@ root.lean:29:4-29:10: error: invalid declaration name `_root_`, `_root_` is a pr root.lean:31:0-31:32: error: invalid namespace '_root_', '_root_' is a reserved namespace root.lean:33:0-33:34: error: invalid namespace 'f._root_', '_root_' is a reserved namespace root.lean:35:14-35:22: error: protected declarations must be in a namespace -root.lean:41:7-41:8: error: unknown identifier 'h' -root.lean:43:7-43:8: error: unknown identifier 'f' +root.lean:41:7-41:8: error(lean.unknownIdentifier): Unknown identifier `h` +root.lean:43:7-43:8: error(lean.unknownIdentifier): Unknown identifier `f` Bla.f (x : Nat) : Nat _private.root.0.prv : Nat -> Nat root.lean:90:89-90:93: error: unsolved goals diff --git a/tests/lean/run/2044.lean b/tests/lean/run/2044.lean index 0108cb1b93..8e4482b9b7 100644 --- a/tests/lean/run/2044.lean +++ b/tests/lean/run/2044.lean @@ -18,7 +18,7 @@ Example adapted from #2044 : CommandElabM Unit ) -/-- error: unknown identifier 'instNonemptyFoo' -/ +/-- error: Unknown identifier `instNonemptyFoo` -/ #guard_msgs in #check instNonemptyFoo -- Verify that `instNonemptyFoo` is the name it would generate if it weren't hygienic @@ -43,7 +43,7 @@ open Lean Elab Command elabCommand stx : CommandElabM Unit ) -/-- error: unknown identifier 'instToJsonFoo' -/ +/-- error: Unknown identifier `instToJsonFoo` -/ #guard_msgs in #check instToJsonFoo deriving instance ToJson for Foo diff --git a/tests/lean/run/2961.lean b/tests/lean/run/2961.lean index 7a82a734a7..e228195289 100644 --- a/tests/lean/run/2961.lean +++ b/tests/lean/run/2961.lean @@ -43,7 +43,7 @@ error: Failed to realize constant replace.eq_def: heq✝ : f t = some u ⊢ replace f t = u --- -error: unknown identifier 'replace.eq_def' +error: Unknown identifier `replace.eq_def` -/ #guard_msgs in #check replace.eq_def @@ -93,7 +93,7 @@ error: Failed to realize constant replace2.eq_def: heq✝ : f t1 = some u ⊢ replace2 f t1 t2 = u --- -error: unknown identifier 'replace2.eq_def' +error: Unknown identifier `replace2.eq_def` -/ #guard_msgs in #check replace2.eq_def diff --git a/tests/lean/run/5667.lean b/tests/lean/run/5667.lean index e70afad7a5..7254280010 100644 --- a/tests/lean/run/5667.lean +++ b/tests/lean/run/5667.lean @@ -52,7 +52,7 @@ error: Failed to realize constant optimize.eq_def: False ⊢ Expr.const 0 = Expr.op bop✝ (Expr.const 0) --- -error: unknown identifier 'optimize.eq_def' +error: Unknown identifier `optimize.eq_def` -/ #guard_msgs in #check optimize.eq_def diff --git a/tests/lean/run/6199.lean b/tests/lean/run/6199.lean index c0702cc118..5c28fae10a 100644 --- a/tests/lean/run/6199.lean +++ b/tests/lean/run/6199.lean @@ -31,7 +31,7 @@ Decimal tests #guard_msgs in #term "(1_00_)" -- Starting with `_` is an identifier: /-- -error: unknown identifier '_10' +error: Unknown identifier `_10` --- info: sorry : ?_ -/ diff --git a/tests/lean/run/6694.lean b/tests/lean/run/6694.lean index 47433596ed..029a5175db 100644 --- a/tests/lean/run/6694.lean +++ b/tests/lean/run/6694.lean @@ -18,7 +18,7 @@ def foo := () def foo := () end -/-- error: unknown identifier 'foo' -/ +/-- error: Unknown identifier `foo` -/ #guard_msgs in #check foo /-- @@ -32,7 +32,7 @@ private def foo := () def foo := () end -/-- error: unknown identifier 'foo' -/ +/-- error: Unknown identifier `foo` -/ #guard_msgs in #check foo /-- @@ -48,9 +48,9 @@ def y := def y.z := 42 end -/-- error: unknown identifier 'y' -/ +/-- error: Unknown identifier `y` -/ #guard_msgs in #check y -/-- error: unknown identifier 'y.z' -/ +/-- error: Unknown identifier `y.z` -/ #guard_msgs in #check y.z /-- @@ -66,9 +66,9 @@ where b := 4 def a.b := 42 end -/-- error: unknown identifier 'a' -/ +/-- error: Unknown identifier `a` -/ #guard_msgs in #check a -/-- error: unknown identifier 'a.b' -/ +/-- error: Unknown identifier `a.b` -/ #guard_msgs in #check a.b /-- @@ -84,11 +84,11 @@ mutual inductive Bar.foo | mk : Bar.foo end -/-- error: unknown identifier 'Bar' -/ +/-- error: Unknown identifier `Bar` -/ #guard_msgs in #check Bar -/-- error: unknown identifier 'Bar.foo' -/ +/-- error: Unknown identifier `Bar.foo` -/ #guard_msgs in #check Bar.foo -/-- error: unknown identifier 'Bar.foo.mk' -/ +/-- error: Unknown identifier `Bar.foo.mk` -/ #guard_msgs in #check Bar.foo.mk /-- @@ -104,9 +104,9 @@ mutual inductive Private | mk end -/-- error: unknown identifier 'Private' -/ +/-- error: Unknown identifier `Private` -/ #guard_msgs in #check Private -/-- error: unknown identifier 'Private.mk' -/ +/-- error: Unknown identifier `Private.mk` -/ #guard_msgs in #check Private.mk /-- @@ -122,9 +122,9 @@ mutual inductive PrivateConstructor.priv | mk end -/-- error: unknown identifier 'PrivateConstructor' -/ +/-- error: Unknown identifier `PrivateConstructor` -/ #guard_msgs in #check PrivateConstructor -/-- error: unknown identifier 'PrivateConstructor.priv' -/ +/-- error: Unknown identifier `PrivateConstructor.priv` -/ #guard_msgs in #check PrivateConstructor.priv /-- @@ -140,11 +140,11 @@ mutual inductive Baz.foo | mk : Baz.foo end -/-- error: unknown identifier 'Baz' -/ +/-- error: Unknown identifier `Baz` -/ #guard_msgs in #check Baz -/-- error: unknown identifier 'Baz.foo' -/ +/-- error: Unknown identifier `Baz.foo` -/ #guard_msgs in #check Baz.foo -/-- error: unknown identifier 'Baz.foo.mk' -/ +/-- error: Unknown identifier `Baz.foo.mk` -/ #guard_msgs in #check Baz.foo.mk /-- @@ -161,9 +161,9 @@ mutual | bar : Foo | foo : Foo → Foo end -/-- error: unknown identifier 'Foo' -/ +/-- error: Unknown identifier `Foo` -/ #guard_msgs in #check Foo -/-- error: unknown identifier 'Foo.bar' -/ +/-- error: Unknown identifier `Foo.bar` -/ #guard_msgs in #check Foo.bar -/-- error: unknown identifier 'Foo.foo' -/ +/-- error: Unknown identifier `Foo.foo` -/ #guard_msgs in #check Foo.foo diff --git a/tests/lean/run/8815.lean b/tests/lean/run/8815.lean index 22de009ed6..42dc9f9cdd 100644 --- a/tests/lean/run/8815.lean +++ b/tests/lean/run/8815.lean @@ -10,13 +10,13 @@ example (P Q : Prop) (hQ : Q) (hP : P) : P := by simp [*, -hQ] /-- error: simp made no progress -/ #guard_msgs in example (P Q : Prop) (hQ : Q) (hP : P) : P := by simp [*, -hP] -/-- error: unknown constant 'hQ' -/ +/-- error: Unknown constant `hQ` -/ #guard_msgs in example (P Q : Prop) (hQ : Q) (hP : P) : P := by simp [-hQ, *] #guard_msgs in example (P Q : Prop) (hQ : Q) (hP : P) : P := by simp_all [-hQ] /-- -error: unknown constant 'hQ' +error: Unknown constant `hQ` --- error: simp made no progress -/ diff --git a/tests/lean/run/eval.lean b/tests/lean/run/eval.lean index 3be84565e5..bd4d41648e 100644 --- a/tests/lean/run/eval.lean +++ b/tests/lean/run/eval.lean @@ -89,7 +89,7 @@ error: could not synthesize a 'ToExpr', 'Repr', or 'ToString' instance for type /-! Elaboration error, does not attempt to evaluate. -/ -/-- error: unknown identifier 'x' -/ +/-- error: Unknown identifier `x` -/ #guard_msgs in #eval 2 + x /-! diff --git a/tests/lean/run/funind_tests.lean b/tests/lean/run/funind_tests.lean index 3c0821ebd1..8d9c6b8be7 100644 --- a/tests/lean/run/funind_tests.lean +++ b/tests/lean/run/funind_tests.lean @@ -801,7 +801,7 @@ info: Mutual_Induct.even.mutual_induct (motive1 motive2 : Nat → Prop) (case1 : -- The .mutual_induct only exists on the first declaration: -/-- error: unknown constant 'Mutual_Induct.odd.mutual_induct' -/ +/-- error: Unknown constant `Mutual_Induct.odd.mutual_induct` -/ #guard_msgs in #check odd.mutual_induct @@ -815,11 +815,11 @@ def nonmutual : Nat → Bool | 0 => true | n+1 => nonmutual n -/-- error: unknown constant 'Mutual_Induct.nonmutual.mutual_induct' -/ +/-- error: Unknown constant `Mutual_Induct.nonmutual.mutual_induct` -/ #guard_msgs in #check nonmutual.mutual_induct -/-- error: unknown constant 'id.mutual_induct' -/ +/-- error: Unknown constant `id.mutual_induct` -/ #guard_msgs in set_option pp.mvars false in #check id.mutual_induct diff --git a/tests/lean/run/guard_msgs.lean b/tests/lean/run/guard_msgs.lean index 0faf6d4ce5..8e4827719f 100644 --- a/tests/lean/run/guard_msgs.lean +++ b/tests/lean/run/guard_msgs.lean @@ -3,16 +3,16 @@ import Lean.Elab.Command set_option guard_msgs.diff false #guard_msgs in -/-- error: unknown identifier 'x' -/ +/-- error: Unknown identifier `x` -/ #guard_msgs in example : α := x /-- -error: unknown identifier 'x' +error: Unknown identifier `x` --- error: ❌️ Docstring on `#guard_msgs` does not match generated message: -error: unknown identifier 'x' +error: Unknown identifier `x` -/ #guard_msgs in #guard_msgs in @@ -42,7 +42,7 @@ example : α := sorry example : α := sorry #guard_msgs in -/-- error: unknown identifier 'x' -/ +/-- error: Unknown identifier `x` -/ #guard_msgs(error, drop warning) in example : α := x diff --git a/tests/lean/run/inferTypeFailure.lean b/tests/lean/run/inferTypeFailure.lean index 0a9c1c2029..416e27cc92 100644 --- a/tests/lean/run/inferTypeFailure.lean +++ b/tests/lean/run/inferTypeFailure.lean @@ -21,7 +21,7 @@ def l2 := fun _ => 0 /-- error: Failed to infer type of theorem `t` -Note: All holes (e.g., `_`) in the header of a theorem are resolved before the proof is processed; information from the proof cannot be used to infer what these values should be +Note: All parameter types and holes (e.g., `_`) in the header of a theorem are resolved before the proof is processed; information from the proof cannot be used to infer what these values should be --- error: type of theorem 't' is not a proposition ?m.65 @@ -32,7 +32,7 @@ theorem t : _ := _ /-- error: Failed to infer type of example -Note: When the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed +Note: Because this declaration's type has been explicitly provided, all parameter types and holes (e.g., `_`) in its header are resolved before its body is processed; information from the declaration body cannot be used to infer what these values should be -/ #guard_msgs in example : _ := _ diff --git a/tests/lean/run/invalidProjection.lean b/tests/lean/run/invalidProjection.lean index 12b08dcaf7..975e67a752 100644 --- a/tests/lean/run/invalidProjection.lean +++ b/tests/lean/run/invalidProjection.lean @@ -85,12 +85,3 @@ which has propositional type -/ #guard_msgs in def foo (h : ∃ x: Nat, True) := h.1 - -/-- -error: unknown identifier 'foo' ---- -error: unknown identifier 'foo' --/ -#guard_msgs in -theorem contradiction : False := - (by decide : 0 ≠ 1) (show foo ⟨0, trivial⟩ = foo ⟨1, trivial⟩ from rfl) diff --git a/tests/lean/run/issue8213.lean b/tests/lean/run/issue8213.lean index e4c985696e..c3dfa35ce7 100644 --- a/tests/lean/run/issue8213.lean +++ b/tests/lean/run/issue8213.lean @@ -25,7 +25,7 @@ error: Failed to realize constant myTest.fun_cases: in the application motive x✝ h_1 --- -error: unknown identifier 'myTest.fun_cases' +error: Unknown identifier `myTest.fun_cases` -/ #guard_msgs in def foo := @myTest.fun_cases diff --git a/tests/lean/run/partial_fixpoint.lean b/tests/lean/run/partial_fixpoint.lean index 43e0740305..ef727dd57b 100644 --- a/tests/lean/run/partial_fixpoint.lean +++ b/tests/lean/run/partial_fixpoint.lean @@ -18,7 +18,7 @@ info: equations: #guard_msgs in #print equations loop -/-- error: unknown constant 'loop.induct' -/ +/-- error: Unknown constant `loop.induct` -/ #guard_msgs in #check loop.induct diff --git a/tests/lean/run/partial_fixpoint_induct.lean b/tests/lean/run/partial_fixpoint_induct.lean index 1ed636e09e..9acf1aef91 100644 --- a/tests/lean/run/partial_fixpoint_induct.lean +++ b/tests/lean/run/partial_fixpoint_induct.lean @@ -8,7 +8,7 @@ info: loop.fixpoint_induct (motive : (Nat → Unit) → Prop) (adm : Lean.Order. #guard_msgs in #check loop.fixpoint_induct -/-- error: unknown constant 'loop.partial_correctness' -/ +/-- error: Unknown constant `loop.partial_correctness` -/ #guard_msgs in #check loop.partial_correctness @@ -98,7 +98,7 @@ info: dependent2''a.fixpoint_induct (m : Nat) (b : Bool) (motive_1 : (Nat → if -/ #guard_msgs in #check dependent2''a.fixpoint_induct -/-- error: unknown constant 'dependent2''b.fixpoint_induct' -/ +/-- error: Unknown constant `dependent2''b.fixpoint_induct` -/ #guard_msgs in #check dependent2''b.fixpoint_induct diff --git a/tests/lean/run/reserved.lean b/tests/lean/run/reserved.lean index 8b8ba0de93..6f9a2858fe 100644 --- a/tests/lean/run/reserved.lean +++ b/tests/lean/run/reserved.lean @@ -27,7 +27,7 @@ def f.eq_2_ := 10 -- Should be ok #guard_msgs in #check f.eq_1 -/-- error: unknown identifier 'f.eq_2' -/ +/-- error: Unknown identifier `f.eq_2` -/ #guard_msgs (error) in #check f.eq_2 @@ -79,7 +79,7 @@ info: fact.eq_def (x✝ : Nat) : #guard_msgs in #check fact.eq_2 -/-- error: unknown identifier 'fact.eq_3' -/ +/-- error: Unknown identifier `fact.eq_3` -/ #guard_msgs (error) in #check fact.eq_3 diff --git a/tests/lean/run/rwWithElabError.lean b/tests/lean/run/rwWithElabError.lean index 6013eea931..03b38ef3e7 100644 --- a/tests/lean/run/rwWithElabError.lean +++ b/tests/lean/run/rwWithElabError.lean @@ -12,7 +12,7 @@ error: tactic 'rewrite' failed, equality or iff proof expected ``` -/ /-- -error: unknown identifier 'not_a_theorem' +error: Unknown identifier `not_a_theorem` --- error: unsolved goals ⊢ True diff --git a/tests/lean/run/showTactic.lean b/tests/lean/run/showTactic.lean index 51996ca5c1..cb0f88a569 100644 --- a/tests/lean/run/showTactic.lean +++ b/tests/lean/run/showTactic.lean @@ -103,7 +103,7 @@ The first goal is re-elaborated with error recovery. -/ /-- -error: unknown identifier 'a' +error: Unknown identifier `a` --- error: unsolved goals case refine_1 diff --git a/tests/lean/run/simp-elab-recover.lean b/tests/lean/run/simp-elab-recover.lean index a3539c3190..8cbc3b433d 100644 --- a/tests/lean/run/simp-elab-recover.lean +++ b/tests/lean/run/simp-elab-recover.lean @@ -4,7 +4,7 @@ when inside a tactic combinator. This checks that without the `recover` flag, `simp [invalid]` fails. -/ -/-- error: unknown identifier 'does_not_exist' -/ +/-- error: Unknown identifier `does_not_exist` -/ #guard_msgs in example : 0 + n = n := by simp only [does_not_exist, Nat.zero_add] @@ -20,13 +20,13 @@ example : 0 + n = n := by first | simp only [does_not_exist, Nat.zero_add] | skip done -/-- error: unknown identifier 'does_not_exist' -/ +/-- error: Unknown identifier `does_not_exist` -/ #guard_msgs in example : 0 + n = n := by skip <;> simp only [does_not_exist, Nat.zero_add] done -/-- error: unknown identifier 'does_not_exist' -/ +/-- error: Unknown identifier `does_not_exist` -/ #guard_msgs in example : 0 + n = n := by all_goals simp only [does_not_exist, Nat.zero_add] diff --git a/tests/lean/run/sorry.lean b/tests/lean/run/sorry.lean index 5cc7ee2fba..1b9435a461 100644 --- a/tests/lean/run/sorry.lean +++ b/tests/lean/run/sorry.lean @@ -80,9 +80,9 @@ but is expected to have type Elaboration errors are just labeled, not unique, to limit cascading errors. -/ /-- -error: unknown identifier 'a' +error: Unknown identifier `a` --- -error: unknown identifier 'b' +error: Unknown identifier `b` --- trace: ⊢ sorry = sorry -/ @@ -94,9 +94,9 @@ example : a = b := by trace_state; rfl Showing that the sorries in the previous test are labeled. -/ /-- -error: unknown identifier 'a' +error: Unknown identifier `a` --- -error: unknown identifier 'b' +error: Unknown identifier `b` --- trace: ⊢ sorry `«sorry:106:10» = sorry `«sorry:106:14» -/ diff --git a/tests/lean/run/structureElab.lean b/tests/lean/run/structureElab.lean index 86dfd2530b..10b4140049 100644 --- a/tests/lean/run/structureElab.lean +++ b/tests/lean/run/structureElab.lean @@ -75,7 +75,7 @@ info: def TestD1.D1.x._default : Nat := id 1 -/ #guard_msgs in #print D1.x._default -/-- error: unknown constant 'D2.x._default' -/ +/-- error: Unknown constant `D2.x._default` -/ #guard_msgs in #print D2.x._default /-- info: def TestD1.D2.x._inherited_default : Nat := @@ -87,7 +87,7 @@ info: def TestD1.D3.x._default : Nat := id 3 -/ #guard_msgs in #print D3.x._default -/-- error: unknown constant 'D4.x._default' -/ +/-- error: Unknown constant `D4.x._default` -/ #guard_msgs in #print D4.x._default /-- info: def TestD1.D4.x._inherited_default : Nat := @@ -112,14 +112,14 @@ info: def TestD2.D1.x._default : {α : Type} → {inst : Inhabited α} → α := fun {α} {inst} => id default -/ #guard_msgs in #print D1.x._default -/-- error: unknown constant 'D2.x._default' -/ +/-- error: Unknown constant `D2.x._default` -/ #guard_msgs in #print D2.x._default /-- info: def TestD2.D2.x._inherited_default : {α : Type} → {inst : Inhabited α} → α := fun {α} {inst} => id default -/ #guard_msgs in #print D2.x._inherited_default -/-- error: unknown constant 'D3.x._default' -/ +/-- error: Unknown constant `D3.x._default` -/ #guard_msgs in #print D3.x._default /-- info: def TestD2.D3.x._inherited_default : Nat := diff --git a/tests/lean/run/tactic_config.lean b/tests/lean/run/tactic_config.lean index 84a4f3a540..2260d83947 100644 --- a/tests/lean/run/tactic_config.lean +++ b/tests/lean/run/tactic_config.lean @@ -184,7 +184,7 @@ example : True := by Responds to recovery mode. In this, `ctac` fails, doesn't report anything, and then execution continues to `exact`. -/ -/-- error: unknown identifier 'blah' -/ +/-- error: Unknown identifier `blah` -/ #guard_msgs in example : True := by first | ctac +x | exact blah diff --git a/tests/lean/run/type_as_hole.lean b/tests/lean/run/type_as_hole.lean index a3c71dc0f7..f28c57e247 100644 --- a/tests/lean/run/type_as_hole.lean +++ b/tests/lean/run/type_as_hole.lean @@ -3,7 +3,7 @@ set_option pp.mvars false /-- error: Failed to infer type of theorem `foo` -Note: All holes (e.g., `_`) in the header of a theorem are resolved before the proof is processed; information from the proof cannot be used to infer what these values should be +Note: All parameter types and holes (e.g., `_`) in the header of a theorem are resolved before the proof is processed; information from the proof cannot be used to infer what these values should be --- error: type of theorem 'foo' is not a proposition ?_ @@ -15,7 +15,7 @@ theorem foo : _ := /-- error: Failed to infer type of example -Note: When the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed +Note: Because this declaration's type has been explicitly provided, all parameter types and holes (e.g., `_`) in its header are resolved before its body is processed; information from the declaration body cannot be used to infer what these values should be -/ #guard_msgs (error) in example : _ := @@ -24,7 +24,7 @@ example : _ := /-- error: Failed to infer type of definition `boo` -Note: When the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed +Note: Because this declaration's type has been explicitly provided, all parameter types and holes (e.g., `_`) in its header are resolved before its body is processed; information from the declaration body cannot be used to infer what these values should be -/ #guard_msgs (error) in def boo : _ := @@ -33,7 +33,7 @@ def boo : _ := /-- error: Failed to infer type of instance `boo` -Note: When the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed +Note: Because this declaration's type has been explicitly provided, all parameter types and holes (e.g., `_`) in its header are resolved before its body is processed; information from the declaration body cannot be used to infer what these values should be -/ #guard_msgs (error) in instance boo : _ := @@ -42,7 +42,7 @@ instance boo : _ := /-- error: Failed to infer type of instance -Note: When the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed +Note: Because this declaration's type has been explicitly provided, all parameter types and holes (e.g., `_`) in its header are resolved before its body is processed; information from the declaration body cannot be used to infer what these values should be -/ #guard_msgs (error) in instance : _ := diff --git a/tests/lean/run/valueOfTerm.lean b/tests/lean/run/valueOfTerm.lean index 0d98804d29..57b8e3cf3f 100644 --- a/tests/lean/run/valueOfTerm.lean +++ b/tests/lean/run/valueOfTerm.lean @@ -49,7 +49,7 @@ example : True := by Referring to a non-existent identifier, error. -/ /-- -error: unknown constant '_TESTS_LEAN_RUN_VALUETERM_not_used_in_Lean' +error: Unknown constant `_TESTS_LEAN_RUN_VALUETERM_not_used_in_Lean` --- error: unsolved goals ⊢ True diff --git a/tests/lean/run/variable.lean b/tests/lean/run/variable.lean index d7c4c983d4..4f48b75614 100644 --- a/tests/lean/run/variable.lean +++ b/tests/lean/run/variable.lean @@ -6,7 +6,7 @@ theorem t1 : n = n := by induction n <;> rfl /-! Variables mentioned only in the body should not be included. -/ variable {n : Nat} in -/-- error: unknown identifier 'n' -/ +/-- error: Unknown identifier `n` -/ #guard_msgs in theorem t2 : ∃ (n : Nat), n = n := by exists n diff --git a/tests/lean/run/wfEqns2.lean b/tests/lean/run/wfEqns2.lean index 98b47498b5..f1578550c3 100644 --- a/tests/lean/run/wfEqns2.lean +++ b/tests/lean/run/wfEqns2.lean @@ -41,7 +41,7 @@ info: g.eq_def (i j : Nat) : #guard_msgs in #check g.eq_def -/-- error: unknown identifier 'g.eq_3' -/ +/-- error: Unknown identifier `g.eq_3` -/ #guard_msgs in #check g.eq_3 @@ -63,7 +63,7 @@ info: h.eq_def (i j : Nat) : #guard_msgs in #check h.eq_def -/-- error: unknown identifier 'h.eq_3' -/ +/-- error: Unknown identifier `h.eq_3` -/ #guard_msgs in #check h.eq_3 diff --git a/tests/lean/run/wfEqns3.lean b/tests/lean/run/wfEqns3.lean index bfe99b7c21..927a3dfecc 100644 --- a/tests/lean/run/wfEqns3.lean +++ b/tests/lean/run/wfEqns3.lean @@ -15,6 +15,6 @@ decreasing_by #guard_msgs in #check f.eq_def -/-- error: unknown identifier 'f.eq_2' -/ +/-- error: Unknown identifier `f.eq_2` -/ #guard_msgs in #check f.eq_2 diff --git a/tests/lean/run/wfEqns4.lean b/tests/lean/run/wfEqns4.lean index 427b66138b..99d7988fc3 100644 --- a/tests/lean/run/wfEqns4.lean +++ b/tests/lean/run/wfEqns4.lean @@ -45,7 +45,7 @@ info: @f.eq_def : ∀ {α : Type u_1} (x : Nat) (x_1 x_2 : α), -/ #guard_msgs in #check @f.eq_def -/-- error: unknown identifier 'f.eq_3' -/ +/-- error: Unknown identifier `f.eq_3` -/ #guard_msgs in #check @f.eq_3 @@ -65,7 +65,7 @@ info: @h.eq_def : ∀ {α : Type u_1} (x x_1 : α) (x_2 : Nat), #guard_msgs in #check @h.eq_def -/-- error: unknown identifier 'h.eq_3' -/ +/-- error: Unknown identifier `h.eq_3` -/ #guard_msgs in #check @h.eq_3 diff --git a/tests/lean/run/wfEqns5.lean b/tests/lean/run/wfEqns5.lean index 9ae8f71151..b7bf133c6e 100644 --- a/tests/lean/run/wfEqns5.lean +++ b/tests/lean/run/wfEqns5.lean @@ -26,7 +26,7 @@ info: foo.eq_def (x✝ x✝¹ : Nat) : #guard_msgs in #check foo.eq_def -/-- error: unknown identifier 'foo.eq_4' -/ +/-- error: Unknown identifier `foo.eq_4` -/ #guard_msgs in #check foo.eq_4 @@ -107,7 +107,7 @@ info: Structural.foo.eq_def (x✝ x✝¹ : Nat) : #guard_msgs in #check foo.eq_def -/-- error: unknown identifier 'foo.eq_4' -/ +/-- error: Unknown identifier `foo.eq_4` -/ #guard_msgs in #check Structural.foo.eq_4 diff --git a/tests/lean/run/wfUnfold.lean b/tests/lean/run/wfUnfold.lean index c74e7c02b6..3552454d83 100644 --- a/tests/lean/run/wfUnfold.lean +++ b/tests/lean/run/wfUnfold.lean @@ -63,6 +63,6 @@ termination_by n -- This should not exist! -/-- error: unknown constant 'fib_eq_fib.eq_def' -/ +/-- error: Unknown constant `fib_eq_fib.eq_def` -/ #guard_msgs in #check fib_eq_fib.eq_def diff --git a/tests/lean/scientific.lean.expected.out b/tests/lean/scientific.lean.expected.out index cfa2939b67..9a7dd75db5 100644 --- a/tests/lean/scientific.lean.expected.out +++ b/tests/lean/scientific.lean.expected.out @@ -14,16 +14,16 @@ scientific.lean:15:6-15:7: error: invalid occurrence of `·` notation, it must b scientific.lean:15:7-15:12: error: unexpected token; expected command scientific.lean:16:6-16:7: error: invalid occurrence of `·` notation, it must be surrounded by parentheses (e.g. `(· + 1)`) scientific.lean:16:7-16:16: error: unexpected token; expected command -scientific.lean:19:6-19:7: error: unknown identifier 'e' +scientific.lean:19:6-19:7: error(lean.unknownIdentifier): Unknown identifier `e` scientific.lean:20:9: error: missing exponent digits in scientific literal scientific.lean:21:9: error: missing exponent digits in scientific literal scientific.lean:22:9: error: missing exponent digits in scientific literal scientific.lean:23:9: error: missing exponent digits in scientific literal scientific.lean:24:9: error: missing exponent digits in scientific literal scientific.lean:25:9: error: missing exponent digits in scientific literal -scientific.lean:26:7-26:8: error: Unknown identifier `Nat.E` +scientific.lean:26:7-26:8: error(lean.unknownIdentifier): Unknown identifier `Nat.E` -Note: Inferred this identifier from the expected type of `.E`: +Note: Inferred this name from the expected resulting type of `.E`: Nat -scientific.lean:27:7-27:9: error: unknown identifier 'E3' +scientific.lean:27:7-27:9: error(lean.unknownIdentifier): Unknown identifier `E3` scientific.lean:28:7: error: missing exponent digits in scientific literal diff --git a/tests/lean/scopedMacros.lean.expected.out b/tests/lean/scopedMacros.lean.expected.out index a5fd1a7919..feefc6564f 100644 --- a/tests/lean/scopedMacros.lean.expected.out +++ b/tests/lean/scopedMacros.lean.expected.out @@ -1,9 +1,9 @@ 10 + 1 : Nat -scopedMacros.lean:11:7-11:11: error: unknown identifier 'foo!' +scopedMacros.lean:11:7-11:11: error(lean.unknownIdentifier): Unknown identifier `foo!` 10 + 1 : Nat scopedMacros.lean:19:7-19:50: error: scoped attributes must be used inside namespaces scopedMacros.lean:19:7-19:50: error: invalid syntax node kind 'termBla!_' -scopedMacros.lean:29:7-29:11: error: unknown identifier 'bla!' +scopedMacros.lean:29:7-29:11: error(lean.unknownIdentifier): Unknown identifier `bla!` scopedMacros.lean:36:7-36:45: error: scoped attributes must be used inside namespaces 10 + 20 : Nat scopedMacros.lean:47:7-47:14: error: elaboration function for 'termBar!_' has not been implemented diff --git a/tests/lean/scopedTokens.lean.expected.out b/tests/lean/scopedTokens.lean.expected.out index 57dc077683..ddffa41a2b 100644 --- a/tests/lean/scopedTokens.lean.expected.out +++ b/tests/lean/scopedTokens.lean.expected.out @@ -1,4 +1,4 @@ 20 + 1 : Nat -scopedTokens.lean:14:7-14:11: error: unknown identifier 'foo!' +scopedTokens.lean:14:7-14:11: error(lean.unknownIdentifier): Unknown identifier `foo!` foo! : Nat 20 + 1 : Nat diff --git a/tests/lean/structSorryBug.lean.expected.out b/tests/lean/structSorryBug.lean.expected.out index 59a08396a9..bc8bdace75 100644 --- a/tests/lean/structSorryBug.lean.expected.out +++ b/tests/lean/structSorryBug.lean.expected.out @@ -1,3 +1,3 @@ -structSorryBug.lean:2:19-2:25: error: unknown identifier 'HasArr' +structSorryBug.lean:2:19-2:25: error(lean.unknownIdentifier): Unknown identifier `HasArr` structSorryBug.lean:4:17-4:32: error: invalid {...} notation, structure type expected Nat diff --git a/tests/lean/theoremType.lean.expected.out b/tests/lean/theoremType.lean.expected.out index 824cac97b0..ce3a57d37a 100644 --- a/tests/lean/theoremType.lean.expected.out +++ b/tests/lean/theoremType.lean.expected.out @@ -2,9 +2,9 @@ theoremType.lean:1:22-1:23: error: don't know how to synthesize placeholder context: ⊢ Nat -Note: All holes (e.g., `_`) in the header of a theorem are resolved before the proof is processed; information from the proof cannot be used to infer what these values should be +Note: All parameter types and holes (e.g., `_`) in the header of a theorem are resolved before the proof is processed; information from the proof cannot be used to infer what these values should be theoremType.lean:4:18-4:19: error: don't know how to synthesize placeholder context: ⊢ Nat -Note: When the resulting type of a declaration is explicitly provided, all holes (e.g., `_`) in the header are resolved before the declaration body is processed +Note: Because this declaration's type has been explicitly provided, all parameter types and holes (e.g., `_`) in its header are resolved before its body is processed; information from the declaration body cannot be used to infer what these values should be diff --git a/tests/lean/unknownId.lean.expected.out b/tests/lean/unknownId.lean.expected.out index 0bcf12387c..5b5a50839f 100644 --- a/tests/lean/unknownId.lean.expected.out +++ b/tests/lean/unknownId.lean.expected.out @@ -1,3 +1,3 @@ -unknownId.lean:3:7-3:10: error: unknown identifier 'bla✝' -unknownId.lean:6:2-6:5: error: unknown identifier 'bla✝' -unknownId.lean:11:6-11:9: error: unknown identifier 'bla✝' +unknownId.lean:3:7-3:10: error(lean.unknownIdentifier): Unknown identifier `bla✝` +unknownId.lean:6:2-6:5: error(lean.unknownIdentifier): Unknown identifier `bla✝` +unknownId.lean:11:6-11:9: error(lean.unknownIdentifier): Unknown identifier `bla✝` diff --git a/tests/pkg/module/Module/Basic.lean b/tests/pkg/module/Module/Basic.lean index 9c0ad9c79b..5b4eb5496c 100644 --- a/tests/pkg/module/Module/Basic.lean +++ b/tests/pkg/module/Module/Basic.lean @@ -105,7 +105,7 @@ def priv := 2 /-! Private decls should not be accessible in exported contexts. -/ -/-- error: unknown identifier 'priv' -/ +/-- error: Unknown identifier `priv` -/ #guard_msgs in public abbrev h := priv diff --git a/tests/pkg/module/Module/Imported.lean b/tests/pkg/module/Module/Imported.lean index 00c1e31afe..142e108329 100644 --- a/tests/pkg/module/Module/Imported.lean +++ b/tests/pkg/module/Module/Imported.lean @@ -74,31 +74,31 @@ has type #guard_msgs in #check f.eq_unfold -/-- error: unknown constant 'f_struct.eq_1' -/ +/-- error: Unknown constant `f_struct.eq_1` -/ #guard_msgs in #check f_struct.eq_1 -/-- error: unknown constant 'f_struct.eq_def' -/ +/-- error: Unknown constant `f_struct.eq_def` -/ #guard_msgs in #check f_struct.eq_def -/-- error: unknown constant 'f_struct.eq_unfold' -/ +/-- error: Unknown constant `f_struct.eq_unfold` -/ #guard_msgs in #check f_struct.eq_unfold -/-- error: unknown constant 'f_wfrec.eq_1' -/ +/-- error: Unknown constant `f_wfrec.eq_1` -/ #guard_msgs in #check f_wfrec.eq_1 -/-- error: unknown constant 'f_wfrec.eq_def' -/ +/-- error: Unknown constant `f_wfrec.eq_def` -/ #guard_msgs in #check f_wfrec.eq_def -/-- error: unknown constant 'f_wfrec.eq_unfold' -/ +/-- error: Unknown constant `f_wfrec.eq_unfold` -/ #guard_msgs in #check f_wfrec.eq_unfold -/-- error: unknown constant 'f_wfrec.induct_unfolding' -/ +/-- error: Unknown constant `f_wfrec.induct_unfolding` -/ #guard_msgs(pass trace, all) in #check f_wfrec.induct_unfolding diff --git a/tests/pkg/module/Module/ImportedAll.lean b/tests/pkg/module/Module/ImportedAll.lean index abce682460..790f64c7e3 100644 --- a/tests/pkg/module/Module/ImportedAll.lean +++ b/tests/pkg/module/Module/ImportedAll.lean @@ -129,6 +129,6 @@ info: theorem f_exp_wfrec.induct_unfolding : ∀ (motive : Nat → Nat → Nat public def pub := priv -/-- error: unknown identifier 'priv' -/ +/-- error: Unknown identifier `priv` -/ #guard_msgs in @[expose] public def pub' := priv diff --git a/tests/pkg/module/Module/ImportedPrivateImported.lean b/tests/pkg/module/Module/ImportedPrivateImported.lean index 00d3a32bfb..c611c10dc3 100644 --- a/tests/pkg/module/Module/ImportedPrivateImported.lean +++ b/tests/pkg/module/Module/ImportedPrivateImported.lean @@ -5,6 +5,6 @@ public import Module.PrivateImported /-! `private import` should not be transitive. -/ -/-- error: unknown identifier 'f' -/ +/-- error: Unknown identifier `f` -/ #guard_msgs in #check f diff --git a/tests/pkg/module/Module/PrivateImported.lean b/tests/pkg/module/Module/PrivateImported.lean index e872bb02b1..9ce47d3ce5 100644 --- a/tests/pkg/module/Module/PrivateImported.lean +++ b/tests/pkg/module/Module/PrivateImported.lean @@ -6,11 +6,11 @@ import Module.Basic public def g := f -/-- error: unknown identifier 'f' -/ +/-- error: Unknown identifier `f` -/ #guard_msgs in set_option autoImplicit false in public theorem t2 : f = 1 := sorry -/-- error: unknown identifier 'f' -/ +/-- error: Unknown identifier `f` -/ #guard_msgs in @[expose] public def h : True := f diff --git a/tests/pkg/prv/Prv.lean b/tests/pkg/prv/Prv.lean index a233c93329..995b87e8e8 100644 --- a/tests/pkg/prv/Prv.lean +++ b/tests/pkg/prv/Prv.lean @@ -6,7 +6,7 @@ import Prv.Foo #guard_msgs in #check { name := "leo", val := 15 : Foo }.val -/-- error: unknown identifier 'a' -/ +/-- error: Unknown identifier `a` -/ #guard_msgs in #check a @@ -26,6 +26,6 @@ def m1 : Name "hello" := {} #guard_msgs in def m2 : Name "hello" := ⟨"hello"⟩ -/-- error: unknown constant 'Name.mk' -/ +/-- error: Unknown constant `Name.mk` -/ #guard_msgs in def m3 : Name "hello" := Name.mk "hello"