From 5f4e6a86d577b9beedc29f1366d5aa36c0fa1a30 Mon Sep 17 00:00:00 2001 From: jrr6 <7482866+jrr6@users.noreply.github.com> Date: Fri, 18 Jul 2025 15:20:31 -0400 Subject: [PATCH] feat: update and explain "unknown constant" and "failed to infer type" errors (#9423) This PR updates the formatting of, and adds explanations for, "unknown identifier" errors as well as "failed to infer type" errors for binders and definitions. It attempts to ameliorate some of the confusion encountered in #1592 by modifying the wording of the "header is elaborated before body is processed" note and adding further discussion and examples of this behavior in the corresponding error explanation. --- src/Init/Notation.lean | 2 +- src/Lean/Attributes.lean | 2 +- src/Lean/Elab/App.lean | 2 +- src/Lean/Elab/Binders.lean | 10 +- src/Lean/Elab/MutualDef.lean | 20 +- src/Lean/Elab/Print.lean | 2 +- src/Lean/Elab/Quotation/Precheck.lean | 3 +- src/Lean/Elab/Term.lean | 4 +- src/Lean/Environment.lean | 2 +- src/Lean/ErrorExplanations.lean | 3 + .../InferBinderTypeFailed.lean | 159 +++++++++++++++ .../ErrorExplanations/InferDefTypeFailed.lean | 82 ++++++++ .../ErrorExplanations/UnknownIdentifier.lean | 186 ++++++++++++++++++ src/Lean/Exception.lean | 4 +- src/Lean/Linter/MissingDocs.lean | 2 +- src/Lean/Linter/UnusedVariables.lean | 2 +- src/Lean/Message.lean | 8 +- src/Lean/Meta/Instances.lean | 2 +- src/Lean/Meta/Tactic/Simp/Simproc.lean | 2 +- src/Lean/MonadEnv.lean | 6 +- src/Lean/Parser/Extension.lean | 2 +- tests/lean/1011.lean.expected.out | 2 +- tests/lean/1038.lean.expected.out | 2 +- tests/lean/1074b.lean.expected.out | 2 +- tests/lean/1569.lean.expected.out | 2 +- tests/lean/1576.lean.expected.out | 4 +- tests/lean/1707.lean.expected.out | 2 +- tests/lean/255.lean.expected.out | 4 +- tests/lean/277a.lean.expected.out | 2 +- tests/lean/331.lean.expected.out | 8 +- tests/lean/346.lean.expected.out | 2 +- tests/lean/435.lean.expected.out | 4 +- tests/lean/586.lean.expected.out | 4 +- tests/lean/593.lean.expected.out | 4 +- tests/lean/StxQuot.lean.expected.out | 10 +- .../autoBoundImplicits1.lean.expected.out | 14 +- ...toImplicitCtorParamIssue.lean.expected.out | 6 +- .../autoImplicitForbidden.lean.expected.out | 12 +- ...utobound_and_macroscopes.lean.expected.out | 4 +- .../lean/binopQuotPrecheck.lean.expected.out | 12 +- tests/lean/deprecated.lean.expected.out | 4 +- .../lean/ellipsisProjIssue.lean.expected.out | 2 +- tests/lean/evalLeak.lean.expected.out | 4 +- tests/lean/funind_errors.lean.expected.out | 8 +- tests/lean/holeErrors.lean.expected.out | 20 +- tests/lean/holes.lean.expected.out | 8 +- tests/lean/hygienicIntro.lean.expected.out | 6 +- tests/lean/implicitTypePos.lean.expected.out | 10 +- tests/lean/inductionErrors.lean.expected.out | 2 +- tests/lean/inductive1.lean.expected.out | 2 +- .../editAfterError.lean.expected.out | 11 +- .../incrementalMutual.lean.expected.out | 12 +- .../incrementalTactic.lean.expected.out | 11 +- tests/lean/letrec1.lean.expected.out | 2 +- tests/lean/macroStack.lean.expected.out | 4 +- tests/lean/moduleOf.lean.expected.out | 2 +- .../lean/multiConstantError.lean.expected.out | 12 +- tests/lean/notationPrecheck.lean.expected.out | 12 +- tests/lean/openExport.lean.expected.out | 4 +- tests/lean/openScoped.lean.expected.out | 6 +- tests/lean/parserRecovery.lean.expected.out | 2 +- tests/lean/protected.lean.expected.out | 10 +- tests/lean/protectedAlias.lean.expected.out | 2 +- tests/lean/renameBug.lean.expected.out | 2 +- tests/lean/root.lean.expected.out | 4 +- tests/lean/run/2044.lean | 4 +- tests/lean/run/2961.lean | 4 +- tests/lean/run/5667.lean | 2 +- tests/lean/run/6199.lean | 2 +- tests/lean/run/6694.lean | 38 ++-- tests/lean/run/8815.lean | 4 +- tests/lean/run/eval.lean | 2 +- tests/lean/run/funind_tests.lean | 6 +- tests/lean/run/guard_msgs.lean | 8 +- tests/lean/run/inferTypeFailure.lean | 4 +- tests/lean/run/invalidProjection.lean | 9 - tests/lean/run/issue8213.lean | 2 +- tests/lean/run/partial_fixpoint.lean | 2 +- tests/lean/run/partial_fixpoint_induct.lean | 4 +- tests/lean/run/reserved.lean | 4 +- tests/lean/run/rwWithElabError.lean | 2 +- tests/lean/run/showTactic.lean | 2 +- tests/lean/run/simp-elab-recover.lean | 6 +- tests/lean/run/sorry.lean | 8 +- tests/lean/run/structureElab.lean | 8 +- tests/lean/run/tactic_config.lean | 2 +- tests/lean/run/type_as_hole.lean | 10 +- tests/lean/run/valueOfTerm.lean | 2 +- tests/lean/run/variable.lean | 2 +- tests/lean/run/wfEqns2.lean | 4 +- tests/lean/run/wfEqns3.lean | 2 +- tests/lean/run/wfEqns4.lean | 4 +- tests/lean/run/wfEqns5.lean | 4 +- tests/lean/run/wfUnfold.lean | 2 +- tests/lean/scientific.lean.expected.out | 8 +- tests/lean/scopedMacros.lean.expected.out | 4 +- tests/lean/scopedTokens.lean.expected.out | 2 +- tests/lean/structSorryBug.lean.expected.out | 2 +- tests/lean/theoremType.lean.expected.out | 4 +- tests/lean/unknownId.lean.expected.out | 6 +- tests/pkg/module/Module/Basic.lean | 2 +- tests/pkg/module/Module/Imported.lean | 14 +- tests/pkg/module/Module/ImportedAll.lean | 2 +- .../Module/ImportedPrivateImported.lean | 2 +- tests/pkg/module/Module/PrivateImported.lean | 4 +- tests/pkg/prv/Prv.lean | 4 +- 106 files changed, 721 insertions(+), 253 deletions(-) create mode 100644 src/Lean/ErrorExplanations/InferBinderTypeFailed.lean create mode 100644 src/Lean/ErrorExplanations/InferDefTypeFailed.lean create mode 100644 src/Lean/ErrorExplanations/UnknownIdentifier.lean 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"