From 13655d6ae739dbe3967e6a92413c62c142c810c6 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Mon, 15 Dec 2025 15:37:30 -0500 Subject: [PATCH 01/11] Removal --- src/Lean/Elab/ErrorExplanation.lean | 13 +-- src/Lean/ErrorExplanation.lean | 142 +--------------------------- 2 files changed, 3 insertions(+), 152 deletions(-) diff --git a/src/Lean/Elab/ErrorExplanation.lean b/src/Lean/Elab/ErrorExplanation.lean index b6cf62a9c002..50360fe2b3db 100644 --- a/src/Lean/Elab/ErrorExplanation.lean +++ b/src/Lean/Elab/ErrorExplanation.lean @@ -117,17 +117,6 @@ open Command in ++ .note m!"The first component of an error explanation name identifies the package from \ which the error originates, and the second identifies the error itself." runTermElabM fun _ => validateDocComment docStx - let doc ← getDocStringText docStx - if errorExplanationExt.getState (← getEnv) |>.contains name then - throwErrorAt id m!"Cannot add explanation: An error explanation already exists for `{name}`" - if let .error (lineOffset, msg) := ErrorExplanation.processDoc doc then - let some range := docStx.raw[1].getRange? | throwError msg - let fileMap ← getFileMap - let ⟨startLine, _⟩ := fileMap.toPosition range.start - let errLine := startLine + lineOffset - let synth := Syntax.ofRange { start := fileMap.ofPosition ⟨errLine, 0⟩, - stop := fileMap.ofPosition ⟨errLine + 1, 0⟩ } - throwErrorAt synth msg let (declLoc? : Option DeclarationLocation) ← do let map ← getFileMap let start := id.raw.getPos?.getD 0 @@ -136,5 +125,5 @@ open Command in module := (← getMainModule) range := .ofStringPositions map start fin } - modifyEnv (errorExplanationExt.addEntry · (name, { metadata, doc, declLoc? })) + modifyEnv (errorExplanationExt.addEntry · (name, { metadata, declLoc? })) | _ => throwUnsupportedSyntax diff --git a/src/Lean/ErrorExplanation.lean b/src/Lean/ErrorExplanation.lean index 4bb7fced2142..9e35b3606019 100644 --- a/src/Lean/ErrorExplanation.lean +++ b/src/Lean/ErrorExplanation.lean @@ -40,7 +40,6 @@ Error explanations are rendered in the manual; a link to the resulting manual pa the bottom of corresponding error messages thrown using `throwNamedError` or `throwNamedErrorAt`. -/ structure ErrorExplanation where - doc : String metadata : ErrorExplanation.Metadata declLoc? : Option DeclarationLocation @@ -185,140 +184,7 @@ private def ValidationM.run (p : ValidationM α) (input : String) : Except (Nat | .success _ res => Except.ok res | .error s err => Except.error (s.getLineNumber, toString err) -/-- -Matches `p` as many times as possible, followed by EOF. If `p` cannot be matched prior to the end -of the input, rethrows the corresponding error. --/ -private partial def manyThenEOF (p : ValidationM α) : ValidationM Unit := fun s => - match eof s with - | .success .. => .success s () - | .error .. => - match p s with - | .success s' _ => manyThenEOF p s' - | .error s' err => .error s' err - -/-- Repeatedly parses the next input as long as it satisfies `p`, and discards the result. -/ -private partial def manyD (p : ValidationM α) : ValidationM Unit := - Parsec.tryCatch p (fun _ => manyD p) (fun _ => pure ()) - -/-- Parses one or more inputs as long as they satisfy `p`, and discards the result. -/ -private def many1D (p : ValidationM α) : ValidationM Unit := - p *> manyD p - -/-- Repeatedly parses the next input as long as it fails to satisfy `p`, and discards the result. -/ -private def manyNotD (p : ValidationM α) : ValidationM Unit := - manyD (notFollowedBy p *> skip) - -/-- Parses an error explanation: a general description followed by an examples section. -/ -private def parseExplanation : ValidationM Unit := do - manyNotD examplesHeader - eof <|> (examplesHeader *> manyThenEOF singleExample) -where - /-- The top-level `# Examples` header -/ - examplesHeader := attempt do - let line ← any - if (matchHeader 1 "Examples" line).isSome then - return - else - fail s!"Expected level-1 'Examples' header, but found `{line}`" - - -- We needn't `attempt` examples because they never appear in a location where backtracking is - -- possible, and persisting the line index allows better error message placement - singleExample := do - let header ← exampleHeader - labelingExampleErrors header do - codeBlock "lean" (some .broken) - many1D (codeBlock "output") - many1D do - let leanBlock ← codeBlock "lean" (some .fixed) - let outputBlocks ← many (codeBlock "output") - return (leanBlock, outputBlocks) - manyNotD exampleEndingHeader - - /-- A level-2 header for a single example. -/ - exampleHeader := attempt do - let line ← any - if let some header := matchHeader 2 none line then - return header - else - fail s!"Expected level-2 header for an example section, but found `{line}`" - /-- A header capable of ending an example. -/ - exampleEndingHeader := attempt do - let line ← any - if (matchHeader 1 none line).isSome || (matchHeader 2 none line).isSome then - return - else - fail s!"Expected a level-1 or level-2 header, but found `{line}`" - - codeBlock (lang : String) (kind? : Option ErrorExplanation.CodeInfo.Kind := none) := attempt do - let (numTicks, infoString) ← fence - <|> fail s!"Expected a(n){kind?.map (s!" {·}") |>.getD ""} `{lang}` code block" - manyD (notFollowedBy (fence numTicks) *> any) - let (_, closing) ← fence numTicks - <|> fail s!"Missing closing code fence for block with header '{infoString}'" - -- Validate code block: - unless closing.trimAscii.isEmpty do - fail s!"Expected a closing code fence, but found the nonempty info string `{closing}`" - let info ← match ErrorExplanation.CodeInfo.parse infoString.copy with - | .ok i => pure i - | .error s => - fail s - let langMatches := info.lang == lang - let kindMatches := (kind?.map (some · == info.kind?)).getD true - unless langMatches && kindMatches do - let (expKind, actKind) := match kind? with - | some kind => - let actualKindStr := (info.kind?.map (s!" {·}")).getD " unspecified-kind" - (s!" {kind}", actualKindStr) - | none => ("", "") - fail s!"Expected a(n){expKind} `{lang}` code block, but found a(n){actKind} `{info.lang}` one" - - fence (ticksToClose : Option Nat := none) := attempt do - let line ← any - if line.startsWith "```" then - let numTicks := line.takeWhile (· == '`') |>.utf8ByteSize -- this makes sense because we know the slice consists only of ticks - match ticksToClose with - | none => return (numTicks, line.drop numTicks) - | some n => - if numTicks == n then - return (numTicks, line.drop numTicks) - else - fail s!"Expected a closing code fence with {n} ticks, but found:\n{line}" - else - -- Don't put `line` in backticks here because it might be a partial code fence - fail s!"Expected a code fence, but found:\n{line}" - - /-- Prepends an error raised by `x` to indicate that it arose in example `header`. -/ - labelingExampleErrors {α} (header : String) (x : ValidationM α) : ValidationM α := fun s => - match x s with - | res@(.success ..) => res - | .error s' msg => .error s' (.other s!"Example '{header}' is malformed: {msg}") - - /-- - If `line` is a level-`level` header and, if `title?` is non-`none`, its title is `title?`, - then returns the contents of the header at `line` (i.e., stripping the leading `#`). Returns - `none` if `line` is not a header of the appropriate form. - -/ - matchHeader (level : Nat) (title? : Option String) (line : String) : Option String := do - let octsEndPos := String.Pos.Raw.nextWhile line (· == '#') 0 - guard (octsEndPos.byteIdx == level) - guard (octsEndPos.get line == ' ') - let titleStartPos := octsEndPos.next line - let title := Substring.Raw.mk line titleStartPos line.rawEndPos |>.toString - let titleMatches : Bool := match title? with - | some expectedTitle => title == expectedTitle - | none => true - guard titleMatches - some title - -/-- -Validates that the given error explanation has the expected structure. If an error is found, it is -represented as a pair `(lineNumber, errorMessage)` where `lineNumber` gives the 0-based offset from -the first line of `doc` at which the error occurs. --/ -def processDoc (doc : String) : Except (Nat × String) Unit := - parseExplanation.run doc end ErrorExplanation @@ -334,9 +200,7 @@ builtin_initialize errorExplanationExt : SimplePersistentEnvExtension (Name × E /-- Returns an error explanation for the given name if one exists, rewriting manual links. -/ def getErrorExplanation? [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] (name : Name) : m (Option ErrorExplanation) := do - let explan? := errorExplanationExt.getState (← getEnv) |>.find? name - explan?.mapM fun explan => - return { explan with doc := (← rewriteManualLinks explan.doc) } + return errorExplanationExt.getState (← getEnv) |>.find? name /-- Returns an error explanation for the given name if one exists *without* rewriting manual links. @@ -362,9 +226,7 @@ def getErrorExplanationsRaw (env : Environment) : Array (Name × ErrorExplanatio /-- Returns all error explanations with their names, rewriting manual links. -/ def getErrorExplanations [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] : m (Array (Name × ErrorExplanation)) := do - let entries := errorExplanationExt.getState (← getEnv) |>.toArray - entries - |>.mapM fun (n, e) => return (n, { e with doc := (← rewriteManualLinks e.doc) }) + return errorExplanationExt.getState (← getEnv) |>.toArray /-- Returns all error explanations with their names as a sorted array, rewriting manual links. From c97ea84387ff12b58e30915af40dcd4d6c0aac99 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Mon, 15 Dec 2025 15:48:30 -0500 Subject: [PATCH 02/11] Modify tests, most lint tests are accepted now if we ignore docstrings, parser will rely on stage2 update --- src/Lean/Elab/ErrorExplanation.lean | 5 ++- src/Lean/Parser/Command.lean | 2 +- tests/lean/run/errorExplanationLinting.lean | 42 ++++++++------------- 3 files changed, 20 insertions(+), 29 deletions(-) diff --git a/src/Lean/Elab/ErrorExplanation.lean b/src/Lean/Elab/ErrorExplanation.lean index 50360fe2b3db..f7981ccf5214 100644 --- a/src/Lean/Elab/ErrorExplanation.lean +++ b/src/Lean/Elab/ErrorExplanation.lean @@ -96,7 +96,7 @@ def elabCheckedNamedError : TermElab := fun stx expType? => do open Command in @[builtin_command_elab registerErrorExplanationStx] def elabRegisterErrorExplanation : CommandElab -| `(registerErrorExplanationStx| $docStx:docComment register_error_explanation%$cmd $id:ident $t:term) => withRef cmd do +| `(registerErrorExplanationStx| $_docStx register_error_explanation%$cmd $id:ident $t:term) => withRef cmd do unless (← getEnv).contains ``ErrorExplanation.Metadata do throwError "To use this command, add `import Lean.ErrorExplanation` to the header of this file" recordExtraModUseFromDecl ``ErrorExplanation.Metadata (isMeta := true) @@ -116,7 +116,8 @@ open Command in throwErrorAt id m!"Invalid name `{name}`: Error explanation names must have two components" ++ .note m!"The first component of an error explanation name identifies the package from \ which the error originates, and the second identifies the error itself." - runTermElabM fun _ => validateDocComment docStx + if errorExplanationExt.getState (← getEnv) |>.contains name then + throwErrorAt id m!"Cannot add explanation: An error explanation already exists for `{name}`" let (declLoc? : Option DeclarationLocation) ← do let map ← getFileMap let start := id.raw.getPos?.getD 0 diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 7b6a657120db..e7ca5cd63db8 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -964,7 +964,7 @@ Registers an error explanation. Note that the error name is not relativized to the current namespace. -/ @[builtin_command_parser] def registerErrorExplanationStx := leading_parser - docComment >> "register_error_explanation " >> ident >> termParser + optional docComment >> "register_error_explanation " >> ident >> termParser /-- Returns syntax for `private` or `public` visibility depending on `isPublic`. This function should be diff --git a/tests/lean/run/errorExplanationLinting.lean b/tests/lean/run/errorExplanationLinting.lean index d5237b064611..efb3e14ad71e 100644 --- a/tests/lean/run/errorExplanationLinting.lean +++ b/tests/lean/run/errorExplanationLinting.lean @@ -8,7 +8,13 @@ command. open Lean Meta -/-- error: Example 'Bar' is malformed: Expected a(n) `output` code block -/ +#guard_msgs in +register_error_explanation Lean.Example1 { + summary := "" + sinceVersion := "" +} + + #guard_msgs in /-- # Examples @@ -24,14 +30,11 @@ open Lean Meta ```lean broken ``` -/ -register_error_explanation Lean.Example { +register_error_explanation Lean.Example2 { summary := "" sinceVersion := "" } -/-- -error: Example 'Foo' is malformed: Expected a(n) `output` code block, but found a(n) `lean` one --/ #guard_msgs in /-- Foo @@ -43,27 +46,23 @@ Foo ```lean fixed ``` -/ -register_error_explanation Lean.Example { +register_error_explanation Lean.Example3 { summary := "" sinceVersion := "" } -/-- error: Expected level-2 header for an example section, but found `# End of Examples` -/ #guard_msgs in /-- # Examples # End of Examples -/ -register_error_explanation Lean.Example { +register_error_explanation Lean.Example4 { summary := "" sinceVersion := "" } -/-- -error: Example 'Example' is malformed: Expected a(n) broken `lean` code block, but found a(n) fixed `lean` one --/ #guard_msgs in /-- # Examples @@ -77,14 +76,11 @@ error: Example 'Example' is malformed: Expected a(n) broken `lean` code block, b ```lean broken ``` -/ -register_error_explanation Lean.Example { +register_error_explanation Lean.Example5 { summary := "" sinceVersion := "" } -/-- -error: Example 'Example' is malformed: Expected a(n) `output` code block, but found a(n) `lean` one --/ #guard_msgs in /-- # Examples @@ -100,12 +96,11 @@ error: Example 'Example' is malformed: Expected a(n) `output` code block, but fo ```lean fixed ``` -/ -register_error_explanation Lean.Example { +register_error_explanation Lean.Example6 { summary := "" sinceVersion := "" } -/-- error: Example 'Example' is malformed: Expected a(n) fixed `lean` code block -/ #guard_msgs in /-- # Examples @@ -120,14 +115,11 @@ register_error_explanation Lean.Example { ```lean fixed ``` -/ -register_error_explanation Lean.Example { +register_error_explanation Lean.Example7 { summary := "" sinceVersion := "" } -/-- -error: Example 'Example' is malformed: Invalid code block info string `lean broken_or_fixed`: offset 20: Invalid attribute `broken_or_fixed` --/ #guard_msgs in /-- # Examples @@ -141,13 +133,12 @@ error: Example 'Example' is malformed: Invalid code block info string `lean brok ```lean fixed ``` -/ -register_error_explanation Lean.Example { +register_error_explanation Lean.Example8 { summary := "" sinceVersion := "" } -/-- error: Expected level-2 header for an example section, but found `# Examples` -/ #guard_msgs in /-- This is an explanation. @@ -166,12 +157,11 @@ This is an explanation. Should fail -/ -register_error_explanation Lean.Example { +register_error_explanation Lean.Example9 { summary := "" sinceVersion := "" } -/-- error: Expected level-2 header for an example section, but found `# New Section` -/ #guard_msgs in /-- Pre-example @@ -214,7 +204,7 @@ Explanation of second example. Foo -/ -register_error_explanation Lean.Example { +register_error_explanation Lean.ExampleA { summary := "" sinceVersion := "" } From f4cda282d2589bd66cf146eff3cd6b502279b340 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Mon, 15 Dec 2025 17:53:39 -0500 Subject: [PATCH 03/11] make tests pass --- src/Lean/Parser/Command.lean | 2 +- tests/lean/run/errorExplanationLinting.lean | 6 ------ 2 files changed, 1 insertion(+), 7 deletions(-) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index e7ca5cd63db8..7b6a657120db 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -964,7 +964,7 @@ Registers an error explanation. Note that the error name is not relativized to the current namespace. -/ @[builtin_command_parser] def registerErrorExplanationStx := leading_parser - optional docComment >> "register_error_explanation " >> ident >> termParser + docComment >> "register_error_explanation " >> ident >> termParser /-- Returns syntax for `private` or `public` visibility depending on `isPublic`. This function should be diff --git a/tests/lean/run/errorExplanationLinting.lean b/tests/lean/run/errorExplanationLinting.lean index efb3e14ad71e..3dbd417c22bd 100644 --- a/tests/lean/run/errorExplanationLinting.lean +++ b/tests/lean/run/errorExplanationLinting.lean @@ -8,12 +8,6 @@ command. open Lean Meta -#guard_msgs in -register_error_explanation Lean.Example1 { - summary := "" - sinceVersion := "" -} - #guard_msgs in /-- From 166bd81219b172c942310857294bc578b9194206 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Mon, 15 Dec 2025 18:59:13 -0500 Subject: [PATCH 04/11] make doc comment on error explanation optional --- src/Lean/Parser/Command.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 7b6a657120db..e7ca5cd63db8 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -964,7 +964,7 @@ Registers an error explanation. Note that the error name is not relativized to the current namespace. -/ @[builtin_command_parser] def registerErrorExplanationStx := leading_parser - docComment >> "register_error_explanation " >> ident >> termParser + optional docComment >> "register_error_explanation " >> ident >> termParser /-- Returns syntax for `private` or `public` visibility depending on `isPublic`. This function should be From 4efb350de191cf34ff37d9e96452d292c2706fc5 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 16 Dec 2025 20:38:40 -0500 Subject: [PATCH 05/11] Delete separate error explanation files --- src/Lean/Elab/Tactic/Induction.lean | 1 - src/Lean/ErrorExplanations.lean | 99 ++++++-- .../CtorResultingTypeMismatch.lean | 72 ------ .../DependsOnNoncomputable.lean | 122 --------- .../InductionWithNoAlts.lean | 51 ---- .../InductiveParamMismatch.lean | 62 ----- .../InductiveParamMissing.lean | 71 ------ .../InferBinderTypeFailed.lean | 164 ------------ .../ErrorExplanations/InferDefTypeFailed.lean | 87 ------- .../ErrorExplanations/InvalidDottedIdent.lean | 78 ------ src/Lean/ErrorExplanations/InvalidField.lean | 99 -------- .../ProjNonPropFromProp.lean | 62 ----- .../ErrorExplanations/PropRecLargeElim.lean | 131 ---------- src/Lean/ErrorExplanations/README.md | 95 ------- .../ErrorExplanations/RedundantMatchAlt.lean | 120 --------- .../SynthInstanceFailed.lean | 125 ---------- .../ErrorExplanations/UnknownIdentifier.lean | 236 ------------------ 17 files changed, 85 insertions(+), 1590 deletions(-) delete mode 100644 src/Lean/ErrorExplanations/CtorResultingTypeMismatch.lean delete mode 100644 src/Lean/ErrorExplanations/DependsOnNoncomputable.lean delete mode 100644 src/Lean/ErrorExplanations/InductionWithNoAlts.lean delete mode 100644 src/Lean/ErrorExplanations/InductiveParamMismatch.lean delete mode 100644 src/Lean/ErrorExplanations/InductiveParamMissing.lean delete mode 100644 src/Lean/ErrorExplanations/InferBinderTypeFailed.lean delete mode 100644 src/Lean/ErrorExplanations/InferDefTypeFailed.lean delete mode 100644 src/Lean/ErrorExplanations/InvalidDottedIdent.lean delete mode 100644 src/Lean/ErrorExplanations/InvalidField.lean delete mode 100644 src/Lean/ErrorExplanations/ProjNonPropFromProp.lean delete mode 100644 src/Lean/ErrorExplanations/PropRecLargeElim.lean delete mode 100644 src/Lean/ErrorExplanations/README.md delete mode 100644 src/Lean/ErrorExplanations/RedundantMatchAlt.lean delete mode 100644 src/Lean/ErrorExplanations/SynthInstanceFailed.lean delete mode 100644 src/Lean/ErrorExplanations/UnknownIdentifier.lean diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean index a7fb99d70ac7..a82191b06213 100644 --- a/src/Lean/Elab/Tactic/Induction.lean +++ b/src/Lean/Elab/Tactic/Induction.lean @@ -12,7 +12,6 @@ public import Lean.Elab.Tactic.ElabTerm import Lean.Meta.Tactic.FunIndCollect import Lean.Elab.App import Lean.Elab.Tactic.Generalize -import Lean.ErrorExplanations.InductionWithNoAlts public section diff --git a/src/Lean/ErrorExplanations.lean b/src/Lean/ErrorExplanations.lean index 6e48cc7482aa..a0d4c611d28b 100644 --- a/src/Lean/ErrorExplanations.lean +++ b/src/Lean/ErrorExplanations.lean @@ -6,17 +6,88 @@ Authors: Joseph Rotella module prelude -public import Lean.ErrorExplanations.CtorResultingTypeMismatch -public import Lean.ErrorExplanations.DependsOnNoncomputable -public import Lean.ErrorExplanations.InductionWithNoAlts -public import Lean.ErrorExplanations.InductiveParamMismatch -public import Lean.ErrorExplanations.InductiveParamMissing -public import Lean.ErrorExplanations.InferBinderTypeFailed -public import Lean.ErrorExplanations.InferDefTypeFailed -public import Lean.ErrorExplanations.InvalidDottedIdent -public import Lean.ErrorExplanations.InvalidField -public import Lean.ErrorExplanations.ProjNonPropFromProp -public import Lean.ErrorExplanations.PropRecLargeElim -public import Lean.ErrorExplanations.RedundantMatchAlt -public import Lean.ErrorExplanations.SynthInstanceFailed -public import Lean.ErrorExplanations.UnknownIdentifier +public import Lean.ErrorExplanation + +/-- -/ +register_error_explanation lean.ctorResultingTypeMismatch { + summary := "Resulting type of constructor was not the inductive type being declared." + sinceVersion := "4.22.0" +} + +/-- -/ +register_error_explanation lean.dependsOnNoncomputable { + summary := "Declaration depends on noncomputable definitions but is not marked as noncomputable" + sinceVersion := "4.22.0" +} + +/-- -/ +register_error_explanation lean.inductionWithNoAlts { + summary := "Induction pattern with nontactic in natural-number-game-style `with` clause." + sinceVersion := "4.26.0" +} + +/-- -/ +register_error_explanation lean.inductiveParamMismatch { + summary := " Invalid parameter in an occurrence of an inductive type in one of its constructors." + sinceVersion := "4.22.0" +} + +/-- -/ +register_error_explanation lean.inductiveParamMissing { + summary := "Parameter not present in an occurrence of an inductive type in one of its constructors." + sinceVersion := "4.22.0" +} + +/-- -/ +register_error_explanation lean.inferBinderTypeFailed { + summary := "The type of a binder could not be inferred." + sinceVersion := "4.23.0" +} + +/-- -/ +register_error_explanation lean.inferDefTypeFailed { + summary := "The type of a definition could not be inferred." + sinceVersion := "4.23.0" +} + +/-- -/ +register_error_explanation lean.invalidDottedIdent { + summary := "Dotted identifier notation used with invalid or non-inferrable expected type." + sinceVersion := "4.22.0" +} + +/-- -/ +register_error_explanation lean.invalidField { + summary := "Generalized field notation used in a potentially ambiguous way." + sinceVersion := "4.22.0" +} + +/-- -/ +register_error_explanation lean.projNonPropFromProp { + summary := "Tried to project data from a proof." + sinceVersion := "4.23.0" +} + +/-- -/ +register_error_explanation lean.propRecLargeElim { + summary := "Attempted to eliminate a proof into a higher type universe." + sinceVersion := "4.23.0" +} + +/-- -/ +register_error_explanation lean.redundantMatchAlt { + summary := "Match alternative will never be reached." + sinceVersion := "4.22.0" +} + +/-- -/ +register_error_explanation lean.synthInstanceFailed { + summary := "Failed to synthesize instance of type class." + sinceVersion := "4.26.0" +} + +/-- -/ +register_error_explanation lean.unknownIdentifier { + summary := "Failed to resolve identifier to variable or constant." + sinceVersion := "4.23.0" +} diff --git a/src/Lean/ErrorExplanations/CtorResultingTypeMismatch.lean b/src/Lean/ErrorExplanations/CtorResultingTypeMismatch.lean deleted file mode 100644 index 447a5985b1d8..000000000000 --- a/src/Lean/ErrorExplanations/CtorResultingTypeMismatch.lean +++ /dev/null @@ -1,72 +0,0 @@ -/- -Copyright (c) 2025 Lean FRO, LLC. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joseph Rotella --/ -module - -prelude -public import Lean.ErrorExplanation -meta import Lean.ErrorExplanation - -public section - -/-- -In an inductive declaration, the resulting type of each constructor must match the type being -declared; if it does not, this error is raised. That is, every constructor of an inductive type must -return a value of that type. See the [Inductive Types](lean-manual://section/inductive-types) manual -section for additional details. Note that it is possible to omit the resulting type for a -constructor if the inductive type being defined has no indices. - -# Examples - -## Typo in Resulting Type -```lean broken -inductive Tree (α : Type) where - | leaf : Tree α - | node : α → Tree α → Treee α -``` -```output -Unexpected resulting type for constructor `Tree.node`: Expected an application of - Tree -but found - ?m.2 -``` -```lean fixed -inductive Tree (α : Type) where - | leaf : Tree α - | node : α → Tree α → Tree α -``` - -## Missing Resulting Type After Constructor Parameter - -```lean broken -inductive Credential where - | pin : Nat - | password : String -``` -```output -Unexpected resulting type for constructor `Credential.pin`: Expected - Credential -but found - Nat -``` -```lean fixed (title := "Fixed (resulting type)") -inductive Credential where - | pin : Nat → Credential - | password : String → Credential -``` -```lean fixed (title := "Fixed (named parameter)") -inductive Credential where - | pin (num : Nat) - | password (str : String) -``` - -If the type of a constructor is annotated, the full type—including the resulting type—must be -provided. Alternatively, constructor parameters can be written using named binders; this allows the -omission of the constructor's resulting type because it contains no indices. --/ -register_error_explanation lean.ctorResultingTypeMismatch { - summary := "Resulting type of constructor was not the inductive type being declared." - sinceVersion := "4.22.0" -} diff --git a/src/Lean/ErrorExplanations/DependsOnNoncomputable.lean b/src/Lean/ErrorExplanations/DependsOnNoncomputable.lean deleted file mode 100644 index 6b8904b7c89e..000000000000 --- a/src/Lean/ErrorExplanations/DependsOnNoncomputable.lean +++ /dev/null @@ -1,122 +0,0 @@ -/- -Copyright (c) 2025 Lean FRO, LLC. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joseph Rotella --/ -module - -prelude -public import Lean.ErrorExplanation -meta import Lean.ErrorExplanation - -public section - -/-- -This error indicates that the specified definition depends on one or more definitions that do not -contain executable code and is therefore required to be marked as `noncomputable`. Such definitions -can be type-checked but do not contain code that can be executed by Lean. - -If you intended for the definition named in the error message to be noncomputable, marking it as -`noncomputable` will resolve this error. If you did not, inspect the noncomputable definitions on -which it depends: they may be noncomputable because they failed to compile, are `axiom`s, or were -themselves marked as `noncomputable`. Making all of your definition's noncomputable dependencies -computable will also resolve this error. See the manual section on -[Modifiers](lean-manual://section/declaration-modifiers) for more information about noncomputable -definitions. - -# Examples - -## Necessarily Noncomputable Function Not Appropriately Marked - -```lean broken -axiom transform : Nat → Nat - -def transformIfZero : Nat → Nat - | 0 => transform 0 - | n => n -``` -```output -`transform` not supported by code generator; consider marking definition as `noncomputable` -``` -```lean fixed -axiom transform : Nat → Nat - -noncomputable def transformIfZero : Nat → Nat - | 0 => transform 0 - | n => n -``` -In this example, `transformIfZero` depends on the axiom `transform`. Because `transform` is an -axiom, it does not contain any executable code; although the value `transform 0` has type `Nat`, -there is no way to compute its value. Thus, `transformIfZero` must be marked `noncomputable` because -its execution would depend on this axiom. - -## Noncomputable Dependency Can Be Made Computable - -```lean broken -noncomputable def getOrDefault [Nonempty α] : Option α → α - | some x => x - | none => Classical.ofNonempty - -def endsOrDefault (ns : List Nat) : Nat × Nat := - let head := getOrDefault ns.head? - let tail := getOrDefault ns.getLast? - (head, tail) -``` -```output -failed to compile definition, consider marking it as 'noncomputable' because it depends on 'getOrDefault', which is 'noncomputable' -``` -```lean fixed (title := "Fixed (computable)") -def getOrDefault [Inhabited α] : Option α → α - | some x => x - | none => default - -def endsOrDefault (ns : List Nat) : Nat × Nat := - let head := getOrDefault ns.head? - let tail := getOrDefault ns.getLast? - (head, tail) -``` -The original definition of `getOrDefault` is noncomputable due to its use of `Classical.choice`. -Unlike in the preceding example, however, it is possible to implement a similar but computable -version of `getOrDefault` (using the `Inhabited` type class), allowing `endsOrDefault` to be -computable. (The differences between `Inhabited` and `Nonempty` are described in the documentation -of inhabited types in the manual section on [Basic Classes](lean-manual://section/basic-classes).) - -## Noncomputable Instance in Namespace - -```lean broken -open Classical in -/-- -Returns `y` if it is in the image of `f`, -or an element of the image of `f` otherwise. --/ -def fromImage (f : Nat → Nat) (y : Nat) := - if ∃ x, f x = y then - y - else - f 0 -``` -```output -failed to compile definition, consider marking it as 'noncomputable' because it depends on 'propDecidable', which is 'noncomputable' -``` -```lean fixed -open Classical in -/-- -Returns `y` if it is in the image of `f`, -or an element of the image of `f` otherwise. --/ -noncomputable def fromImage (f : Nat → Nat) (y : Nat) := - if ∃ x, f x = y then - y - else - f 0 -``` -The `Classical` namespace contains `Decidable` instances that are not computable. These are a common -source of noncomputable dependencies that do not explicitly appear in the source code of a -definition. In the above example, for instance, a `Decidable` instance for the proposition -`∃ x, f x = y` is synthesized using a `Classical` decidability instance; therefore, `fromImage` must -be marked `noncomputable`. --/ -register_error_explanation lean.dependsOnNoncomputable { - summary := "Declaration depends on noncomputable definitions but is not marked as noncomputable" - sinceVersion := "4.22.0" -} diff --git a/src/Lean/ErrorExplanations/InductionWithNoAlts.lean b/src/Lean/ErrorExplanations/InductionWithNoAlts.lean deleted file mode 100644 index a82dc28bbd97..000000000000 --- a/src/Lean/ErrorExplanations/InductionWithNoAlts.lean +++ /dev/null @@ -1,51 +0,0 @@ -/- -Copyright (c) 2025 Lean FRO, LLC. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Rob Simmons --/ -module - -prelude -public import Lean.ErrorExplanation -meta import Lean.ErrorExplanation - -/-- -Tactic-based proofs using induction in Lean need to use a pattern-matching-like notation to describe -individual cases of the proof. However, the `induction'` tactic in Mathlib and the specialized -`induction` tactic for natural numbers used in the Natural Number Game follows a different pattern. - -# Examples - -## Adding Explicit Cases to an Induction Proof - -```lean broken -theorem zero_mul (m : Nat) : 0 * m = 0 := by - induction m with n n_ih - rw [Nat.mul_zero] - rw [Nat.mul_succ] - rw [Nat.add_zero] - rw [n_ih] -``` -```output -unknown tactic -``` -```lean fixed -theorem zero_mul (m : Nat) : 0 * m = 0 := by - induction m with - | zero => - rw [Nat.mul_zero] - | succ n n_ih => - rw [Nat.mul_succ] - rw [Nat.add_zero] - rw [n_ih] -``` -The broken example has the structure of a correct proof in the Natural Numbers Game, and this -proof will work if you `import Mathlib` and replace `induction` with `induction'`. Induction tactics -in basic Lean expect the `with` keyword to be followed by a series of cases, and the names for -the inductive case are provided in the `succ` case rather than being provided up-front. - --/ -register_error_explanation lean.inductionWithNoAlts { - summary := "Induction pattern with nontactic in natural-number-game-style `with` clause." - sinceVersion := "4.26.0" -} diff --git a/src/Lean/ErrorExplanations/InductiveParamMismatch.lean b/src/Lean/ErrorExplanations/InductiveParamMismatch.lean deleted file mode 100644 index e03664e647b2..000000000000 --- a/src/Lean/ErrorExplanations/InductiveParamMismatch.lean +++ /dev/null @@ -1,62 +0,0 @@ -/- -Copyright (c) 2025 Lean FRO, LLC. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joseph Rotella --/ -module - -prelude -public import Lean.ErrorExplanation -meta import Lean.ErrorExplanation - -public section - -/-- -This error occurs when a parameter of an inductive type is not uniform in an inductive -declaration. The parameters of an inductive type (i.e., those that appear before the colon following -the `inductive` keyword) must be identical in all occurrences of the type being defined in its -constructors' types. If a parameter of an inductive type must vary between constructors, make the -parameter an index by moving it to the right of the colon. See the manual section on -[Inductive Types](lean-manual://section/inductive-types) for additional details. - -Note that auto-implicit inlay hints always appear left of the colon in an inductive declaration -(i.e., as parameters), even when they are actually indices. This means that double-clicking on an -inlay hint to insert such parameters may result in this error. If it does, change the inserted -parameters to indices. - -# Examples - -## Vector Length Index as a Parameter - -```lean broken -inductive Vec (α : Type) (n : Nat) : Type where - | nil : Vec α 0 - | cons : α → Vec α n → Vec α (n + 1) -``` -```output broken -Mismatched inductive type parameter in - Vec α 0 -The provided argument - 0 -is not definitionally equal to the expected parameter - n - -Note: The value of parameter `n` must be fixed throughout the inductive declaration. Consider making this parameter an index if it must vary. -``` -```lean fixed -inductive Vec (α : Type) : Nat → Type where - | nil : Vec α 0 - | cons : α → Vec α n → Vec α (n + 1) -``` - -The length argument `n` of the `Vec` type constructor is declared as a parameter, but other values -for this argument appear in the `nil` and `cons` constructors (namely, `0` and `n + 1`). An error -therefore appears at the first occurrence of such an argument. To correct this, `n` cannot be a -parameter of the inductive declaration and must instead be an index, as in the corrected example. On -the other hand, `α` remains unchanged throughout all occurrences of `Vec` in the declaration and so -is a valid parameter. --/ -register_error_explanation lean.inductiveParamMismatch { - summary := "Invalid parameter in an occurrence of an inductive type in one of its constructors." - sinceVersion := "4.22.0" -} diff --git a/src/Lean/ErrorExplanations/InductiveParamMissing.lean b/src/Lean/ErrorExplanations/InductiveParamMissing.lean deleted file mode 100644 index 94742fd5f636..000000000000 --- a/src/Lean/ErrorExplanations/InductiveParamMissing.lean +++ /dev/null @@ -1,71 +0,0 @@ -/- -Copyright (c) 2025 Lean FRO, LLC. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joseph Rotella --/ -module - -prelude -public import Lean.ErrorExplanation -meta import Lean.ErrorExplanation - -public section - -/-- -This error occurs when an inductive type constructor is partially applied in the type of one of its -constructors such that one or more parameters of the type are omitted. The elaborator requires that -all parameters of an inductive type be specified everywhere that type is referenced in its -definition, including in the types of its constructors. - -If it is necessary to allow the type constructor to be partially applied, without specifying a given -type parameter, that parameter must be converted to an index. See the manual section on -[Inductive Types](lean-manual://section/inductive-types) for further explanation of the difference -between indices and parameters. - -# Examples - -## Omitting Parameter in Argument to Higher-Order Predicate - -```lean broken -inductive List.All {α : Type u} (P : α → Prop) : List α → Prop - | nil : All P [] - | cons {x xs} : P x → All P xs → All P (x :: xs) - -structure RoseTree (α : Type u) where - val : α - children : List (RoseTree α) - -inductive RoseTree.All {α : Type u} (P : α → Prop) (t : RoseTree α) : Prop - | intro : P t.val → List.All (All P) t.children → All P t -``` -```output -Missing parameter(s) in occurrence of inductive type: In the expression - List.All (All P) t.children -found - All P -but expected all parameters to be specified: - All P t - -Note: All occurrences of an inductive type in the types of its constructors must specify its fixed parameters. Only indices can be omitted in a partial application of the type constructor. -``` -```lean fixed -inductive List.All {α : Type u} (P : α → Prop) : List α → Prop - | nil : All P [] - | cons {x xs} : P x → All P xs → All P (x :: xs) - -structure RoseTree (α : Type u) where - val : α - children : List (RoseTree α) - -inductive RoseTree.All {α : Type u} (P : α → Prop) : RoseTree α → Prop - | intro : P t.val → List.All (All P) t.children → All P t -``` -Because the `RoseTree.All` type constructor must be partially applied in the argument to `List.All`, -the unspecified argument (`t`) must not be a parameter of the `RoseTree.All` predicate. Making it an -index to the right of the colon in the header of `RoseTree.All` allows this partial application to -succeed. --/ -register_error_explanation lean.inductiveParamMissing { - summary := "Parameter not present in an occurrence of an inductive type in one of its constructors." - sinceVersion := "4.22.0" -} diff --git a/src/Lean/ErrorExplanations/InferBinderTypeFailed.lean b/src/Lean/ErrorExplanations/InferBinderTypeFailed.lean deleted file mode 100644 index f6130475d1a2..000000000000 --- a/src/Lean/ErrorExplanations/InferBinderTypeFailed.lean +++ /dev/null @@ -1,164 +0,0 @@ -/- -Copyright (c) 2025 Lean FRO, LLC. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joseph Rotella --/ -module - -prelude -public import Lean.ErrorExplanation -meta import Lean.ErrorExplanation - -public section - -/-- -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 deleted file mode 100644 index fd5b7484b06f..000000000000 --- a/src/Lean/ErrorExplanations/InferDefTypeFailed.lean +++ /dev/null @@ -1,87 +0,0 @@ -/- -Copyright (c) 2025 Lean FRO, LLC. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joseph Rotella --/ -module - -prelude -public import Lean.ErrorExplanation -meta import Lean.ErrorExplanation - -public section - -/-- -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/InvalidDottedIdent.lean b/src/Lean/ErrorExplanations/InvalidDottedIdent.lean deleted file mode 100644 index 2f6b4badee33..000000000000 --- a/src/Lean/ErrorExplanations/InvalidDottedIdent.lean +++ /dev/null @@ -1,78 +0,0 @@ -/- -Copyright (c) 2025 Lean FRO, LLC. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joseph Rotella --/ -module - -prelude -public import Lean.ErrorExplanation -meta import Lean.ErrorExplanation - -public section - -/-- -This error indicates that dotted identifier notation was used in an invalid or unsupported context. -Dotted identifier notation allows an identifier's namespace to be omitted, provided that it can be -inferred by Lean based on type information. Details about this notation can be found in the manual -section on [identifiers](lean-manual://section/identifiers-and-resolution). - -This notation can only be used in a term whose type Lean is able to infer. If there is insufficient -type information for Lean to do so, this error will be raised. The inferred type must not be a type -universe (e.g., `Prop` or `Type`), as dotted-identifier notation is not supported on these types. - -# Examples - -## Insufficient Type Information - -```lean broken -def reverseDuplicate (xs : List α) := - .reverse (xs ++ xs) -``` -```output -Invalid dotted identifier notation: The expected type of `.reverse` could not be determined -``` -```lean fixed -def reverseDuplicate (xs : List α) : List α := - .reverse (xs ++ xs) -``` -Because the return type of `reverseDuplicate` is not specified, the expected type of `.reverse` -cannot be determined. Lean will not use the type of the argument `xs ++ xs` to infer the omitted -namespace. Adding the return type `List α` allows Lean to infer the type of `.reverse` and thus the -appropriate namespace (`List`) in which to resolve this identifier. - -Note that this means that changing the return type of `reverseDuplicate` changes how `.reverse` -resolves: if the return type is `T`, then Lean will (attempt to) resolve `.reverse` to a function -`T.reverse` whose return type is `T`—even if `T.reverse` does not take an argument of type -`List α`. - -## Dotted Identifier Where Type Universe Expected - -```lean broken -example (n : Nat) := - match n > 42 with - | .true => n - 1 - | .false => n + 1 -``` -```output -Invalid dotted identifier notation: Not supported on type universe - Prop -``` -```lean fixed -example (n : Nat) := - match decide (n > 42) with - | .true => n - 1 - | .false => n + 1 -``` - -The proposition `n > 42` has type `Prop`, which, being a type universe, does not support -dotted-identifier notation. As this example demonstrates, attempting to use this notation in such a -context is almost always an error. The intent in this example was for `.true` and `.false` to be -Booleans, not propositions; however, `match` expressions do not automatically perform this coercion -for decidable propositions. Explicitly adding `decide` makes the discriminant a `Bool` and allows -the dotted-identifier resolution to succeed. --/ -register_error_explanation lean.invalidDottedIdent { - summary := "Dotted identifier notation used with invalid or uninferrable expected type." - sinceVersion := "4.22.0" -} diff --git a/src/Lean/ErrorExplanations/InvalidField.lean b/src/Lean/ErrorExplanations/InvalidField.lean deleted file mode 100644 index 1942d10daa9c..000000000000 --- a/src/Lean/ErrorExplanations/InvalidField.lean +++ /dev/null @@ -1,99 +0,0 @@ -/- -Copyright (c) 2025 Lean FRO, LLC. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Rob Simmons --/ -module - -prelude -public import Lean.ErrorExplanation -meta import Lean.ErrorExplanation - -/-- -This error indicates that an expression containing a dot followed by an identifier was encountered, -and that it wasn't possible to understand the identifier as a field. - -Lean's field notation is very powerful, but this can also make it confusing: the expression -`color.value` can either be a single [identifier](lean-manual://section/identifiers-and-resolution), -it can be a reference to the [field of a structure](lean-manual://section/structure-fields), and it -and be a calling a function on the value `color` with -[generalized field notation](lean-manual://section/generalized-field-notation). - -# Examples - -## Incorrect Field Name - -```lean broken -#eval (4 + 2).suc -``` -```output -Invalid field `suc`: The environment does not contain `Nat.suc`, so it is not possible to project the field `suc` from an expression - 4 + 2 -of type `Nat` -``` -```lean fixed -#eval (4 + 1).succ -``` - -The simplest reason for an invalid field error is that the function being sought, like `Nat.suc`, -does not exist. - -## Projecting from the Wrong Expression - -```lean broken -#eval '>'.leftpad 10 ['a', 'b', 'c'] -``` -```output -Invalid field `leftpad`: The environment does not contain `Char.leftpad`, so it is not possible to project the field `leftpad` from an expression - '>' -of type `Char` -``` -```lean fixed -#eval ['a', 'b', 'c'].leftpad 10 '>' -``` - -The type of the expression before the dot entirely determines the function being called by the field -projection. There is no `Char.leftpad`, and the only way to invoke `List.leftpad` with generalized -field notation is to have the list come before the dot. - -## Type is Not Specific - -```lean broken -def double_plus_one {α} [Add α] (x : α) := - (x + x).succ -``` -```output -Invalid field notation: Field projection operates on types of the form `C ...` where C is a constant. The expression - x + x -has type `α` which does not have the necessary form. -``` -```lean fixed -def double_plus_one (x : Nat) := - (x + x).succ -``` - -The `Add` typeclass is sufficient for performing the addition `x + x`, but the `.succ` field notation -cannot operate without knowing more about the actual type from which `succ` is being projected. - -## Insufficient Type Information - -```lean broken -example := fun (n) => n.succ.succ -``` -```output -Invalid field notation: Type of - n -is not known; cannot resolve field `succ` -``` -```lean fixed -example := fun (n : Nat) => n.succ.succ -``` - -Generalized field notation can only be used when it is possible to determine the type that is being -projected. Type annotations may need to be added to make generalized field notation work. - --/ -register_error_explanation lean.invalidField { - summary := "Dotted identifier notation used without ." - sinceVersion := "4.22.0" -} diff --git a/src/Lean/ErrorExplanations/ProjNonPropFromProp.lean b/src/Lean/ErrorExplanations/ProjNonPropFromProp.lean deleted file mode 100644 index 7122651eaff6..000000000000 --- a/src/Lean/ErrorExplanations/ProjNonPropFromProp.lean +++ /dev/null @@ -1,62 +0,0 @@ -/- -Copyright (c) 2025 Lean FRO, LLC. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joseph Rotella --/ -module - -prelude -public import Lean.ErrorExplanation -meta import Lean.ErrorExplanation - -public section - -/-- -This error occurs when attempting to project a piece of data from a proof of a proposition using an -index projection. For example, if `h` is a proof of an existential proposition, attempting to -extract the witness `h.1` is an example of this error. Such projections are disallowed because they -may violate Lean's prohibition of large elimination from `Prop` (refer to the -[Propositions](lean-manual://section/propositions) manual section for further details). - -Instead of an index projection, consider using a pattern-matching `let`, `match` expression, or a -destructuring tactic like `cases` to eliminate from one propositional type to another. Note that -such elimination is only valid if the resulting value is also in `Prop`; if it is not, the error -[`lean.propRecLargeElim`](lean-manual://errorExplanation/lean.propRecLargeElim) will be raised. - -# Examples - -## Attempting to Use Index Projection on Existential Proof - -```lean broken -example (a : Nat) (h : ∃ x : Nat, x > a + 1) : ∃ x : Nat, x > 0 := - ⟨h.1, Nat.lt_of_succ_lt h.2⟩ -``` -```output -Invalid projection: Cannot project a value of non-propositional type - Nat -from the expression - h -which has propositional type - ∃ x, x > a + 1 -``` -```lean fixed (title := "Fixed (let)") -example (a : Nat) (h : ∃ x : Nat, x > a + 1) : ∃ x : Nat, x > a := - let ⟨w, hw⟩ := h - ⟨w, Nat.lt_of_succ_lt hw⟩ -``` -```lean (title := "Fixed (cases)") -example (a : Nat) (h : ∃ x : Nat, x > a + 1) : ∃ x : Nat, x > a := by - cases h with - | intro w hw => - exists w - omega -``` - -The witness associated with a proof of an existential proposition cannot be extracted using an -index projection. Instead, it is necessary to use a pattern match: either a term like a `let` -binding or a tactic like `cases`. --/ -register_error_explanation lean.projNonPropFromProp { - summary := "Tried to project data from a proof." - sinceVersion := "4.23.0" -} diff --git a/src/Lean/ErrorExplanations/PropRecLargeElim.lean b/src/Lean/ErrorExplanations/PropRecLargeElim.lean deleted file mode 100644 index d2d977d50c48..000000000000 --- a/src/Lean/ErrorExplanations/PropRecLargeElim.lean +++ /dev/null @@ -1,131 +0,0 @@ -/- -Copyright (c) 2025 Lean FRO, LLC. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joseph Rotella --/ -module - -prelude -public import Lean.ErrorExplanation -meta import Lean.ErrorExplanation - -public section - -/-- -This error occurs when attempting to eliminate a proof of a proposition into a higher type universe. -Because Lean's type theory does not allow large elimination from `Prop`, it is invalid to -pattern-match on such values—e.g., by using `let` or `match`—to produce a piece of data in a -non-propositional universe (i.e., `Type u`). More precisely, the motive of a propositional recursor -must be a proposition. (See the manual section on -[Subsingleton Elimination](lean-manual://section/subsingleton-elimination) for exceptions to this -rule.) - -Note that this error will arise in any expression that eliminates from a proof into a -non-propositional universe, even if that expression occurs within another expression of -propositional type (e.g., in a `let` binding in a proof). The "Defining an intermediate data value -within a proof" example below demonstrates such an occurrence. Errors of this kind can usually be -resolved by moving the recursor application "outward," so that its motive is the proposition being -proved rather than the type of data-valued term. - -# Examples - -## Defining an Intermediate Data Value Within a Proof - -```lean broken -example {α : Type} [inst : Nonempty α] (p : α → Prop) : - ∃ x, p x ∨ ¬ p x := - let val := - match inst with - | .intro x => x - ⟨val, Classical.em (p val)⟩ -``` -```output -Tactic `cases` failed with a nested error: -Tactic `induction` failed: recursor `Nonempty.casesOn` can only eliminate into `Prop` - -α : Type -motive : Nonempty α → Sort ?u.48 -h_1 : (x : α) → motive ⋯ -inst✝ : Nonempty α -⊢ motive inst✝ - after processing - _ -the dependent pattern matcher can solve the following kinds of equations -- = and = -- = where the terms are definitionally equal -- = , examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil -``` -```lean fixed -example {α : Type} [inst : Nonempty α] (p : α → Prop) : - ∃ x, p x ∨ ¬ p x := - match inst with - | .intro x => ⟨x, Classical.em (p x)⟩ -``` -Even though the `example` being defined has a propositional type, the body of `val` does not; it has -type `α : Type`. Thus, pattern-matching on the proof of `Nonempty α` (a proposition) to produce -`val` requires eliminating that proof into a non-propositional type and is disallowed. Instead, the -`match` expression must be moved to the top level of the `example`, where the result is a -`Prop`-valued proof of the existential claim stated in the example's header. This restructuring -could also be done using a pattern-matching `let` binding. - -## Extracting the Witness from an Existential Proof - -```lean broken -def getWitness {α : Type u} {p : α → Prop} (h : ∃ x, p x) : α := - match h with - | .intro x _ => x -``` -```output -Tactic `cases` failed with a nested error: -Tactic `induction` failed: recursor `Exists.casesOn` can only eliminate into `Prop` - -α : Type u -p : α → Prop -motive : (∃ x, p x) → Sort ?u.52 -h_1 : (x : α) → (h : p x) → motive ⋯ -h✝ : ∃ x, p x -⊢ motive h✝ - after processing - _ -the dependent pattern matcher can solve the following kinds of equations -- = and = -- = where the terms are definitionally equal -- = , examples: List.cons x xs = List.cons y ys, and List.cons x xs = List.nil -``` -```lean fixed (title := "Fixed (in Prop)") --- This is `Exists.elim` -theorem useWitness {α : Type u} {p : α → Prop} {q : Prop} - (h : ∃ x, p x) (hq : (x : α) → p x → q) : q := - match h with - | .intro x hx => hq x hx -``` -```lean fixed (title := "Fixed (in Type)") -def getWitness {α : Type u} {p : α → Prop} - (h : (x : α) ×' p x) : α := - match h with - | .mk x _ => x -``` -In this example, simply relocating the pattern-match is insufficient; the attempted definition -`getWitness` is fundamentally unsound. (Consider the case where `p` is `fun (n : Nat) => n > 0`: if -`h` and `h'` are proofs of `∃ x, x > 0`, with `h` using witness `1` and `h'` witness `2`, then since -`h = h'` by proof irrelevance, it follows that `getWitness h = getWitness h'`—i.e., `1 = 2`.) - -Instead, `getWitness` must be rewritten: either the resulting type of the function must be a -proposition (the first fixed example above), or `h` must not be a proposition (the second). - -In the first corrected example, the resulting type of `useWitness` is now a proposition `q`. This -allows us to pattern-match on `h`—since we are eliminating into a propositional type—and pass the -unpacked values to `hq`. From a programmatic perspective, one can view `useWitness` as rewriting -`getWitness` in continuation-passing style, restricting subsequent computations to use its result -only to construct values in `Prop`, as required by the prohibition on propositional large -elimination. Note that `useWitness` is the existential elimination principle `Exists.elim`. - -The second corrected example changes the type of `h` from an existential proposition to a -`Type`-valued dependent pair (corresponding to the `PSigma` type constructor). Since this type is -not propositional, eliminating into `α : Type u` is no longer invalid, and the previously attempted -pattern match now type-checks. --/ -register_error_explanation lean.propRecLargeElim { - summary := "Attempted to eliminate a proof into a higher type universe." - sinceVersion := "4.23.0" -} diff --git a/src/Lean/ErrorExplanations/README.md b/src/Lean/ErrorExplanations/README.md deleted file mode 100644 index 8cc96bdcc0f2..000000000000 --- a/src/Lean/ErrorExplanations/README.md +++ /dev/null @@ -1,95 +0,0 @@ -# Error Explanations - -## Overview - -This directory contains explanations for named errors in Lean core. -Explanations associate to each named error or warning a long-form -description of its meaning and causes, relevant background -information, and strategies for correcting erroneous code. They also -provide examples of incorrect and corrected code. While error -explanations are declared in source, they are viewed as part of -external documentation linked from error messages. - -Explanations straddle the line between diagnostics and documentation: -unlike the error messages they describe, explanations serve not only -to aid the debugging process but also to help users understand the -principles of the language that underlie the error. Accordingly, error -explanations should be written with both of these aims in mind. Refer -to existing explanations for examples of the formatting and content -conventions described here. - -Once an error explanation has been registered, use the macros -`throwNamedError`, `logNamedError`, `throwNamedErrorAt` and -`logNamedErrorAt` to tag error messages with the appropriate -explanation name. Doing so will display a widget in the Infoview with -the name of the error and a link to the corresponding explanation. - -## Registering Explanations - -New error explanations are declared using the -`register_error_explanation` command. Each explanation should -appear in a separate submodule of `Lean.ErrorExplanations` whose name -matches the error name being declared; the module should be marked -with `prelude` and import only `Lean.ErrorExplanation`. The -`register_error_explanation` keyword is preceded by a doc -comment containing the explanation (written in Markdown, following the -structure guidelines below) and is followed by the name of the -explanation and a `Lean.ErrorExplanation.Metadata` structure -describing the error. All errors have two-component names: the first -identifies the package or "domain" to which the error belongs (in -core, this will nearly always be `lean`); the second identifies the -error itself. Error names are written in upper camel case and should -be descriptive but not excessively verbose. Abbreviations in error -names are acceptable, but they should be reasonably clear (e.g., -abbreviations that are commonly used elsewhere in Lean, such as `Ctor` -for "constructor") and should not be ambiguous with other vocabulary -likely to appear in error names (e.g., use `Indep` rather than `Ind` -for "independent," since the latter could be confused with -"inductive"). - - -## Structure - -### Descriptions - -Error explanations consist of two parts: a prose description of the -error and code examples. The description should begin by explaining -the meaning of the error and why it occurs. It should also briefly -explain, if appropriate, any relevant context, such as related errors -or relevant entries in the reference manual. The latter is especially -useful for directing users to important concepts for understanding an -error: while it is appropriate to provide brief conceptual exposition -in an error explanation, avoid extensively duplicating content that -can be found elsewhere in the manual. General resolution or debugging -strategies not tied to specific examples can also be discussed in the -description portion of an explanation. - -### Examples - -The second half of an explanation (set off by the level-1 header -"Examples") contains annotated code examples. Each of these consists -of a level-2 header with the name of the example, followed immediately -by a sequence of code blocks containing self-contained minimal working -(or error-producing) examples (MWEs) and outputs. The first MWE should -have the Markdown info string `lean broken` and demonstrate the error -in question; it should be followed by an `output` code block with the -corresponding error message. Subsequent MWEs should have the info -string `lean fixed` and illustrate how to rewrite the code correctly. -Finally, after these MWEs, include explanatory text describing the -example and the cause and resolution of the error it demonstrates. - -Note that each MWE in an example will be rendered as a tab, and the -full example (including its explanatory text) will appear in a -collapsible "Example" block like those used elsewhere in the manual. -Include `(title := "Title")` in the info string of an MWE to assign it -a custom title (for instance, if there are multiple "fixed" MWEs). -Examples should center on code: prose not specific to the example -should generally appear in the initial half of the explanation. -However, an example should provide sufficient commentary for users to -understand how it illustrates relevant ideas from the preceding -description and what was done to resolve the exemplified error. - -Choose examples carefully: they should be relatively minimal, so as to -draw out the error itself, but not so contrived as to impede -comprehension. Each should contain a distinct, representative instance -of the error to avoid the need for excessively many. diff --git a/src/Lean/ErrorExplanations/RedundantMatchAlt.lean b/src/Lean/ErrorExplanations/RedundantMatchAlt.lean deleted file mode 100644 index 0dcc798c9385..000000000000 --- a/src/Lean/ErrorExplanations/RedundantMatchAlt.lean +++ /dev/null @@ -1,120 +0,0 @@ -/- -Copyright (c) 2025 Lean FRO, LLC. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joseph Rotella --/ -module - -prelude -public import Lean.ErrorExplanation -meta import Lean.ErrorExplanation - -public section - -/-- -This error occurs when an alternative in a pattern match can never be reached: any values that would -match the provided patterns would also match some preceding alternative. Refer to the -[Pattern Matching](lean-manual://section/pattern-matching) manual section for additional details -about pattern matching. - -This error may appear in any pattern matching expression, including `match` expressions, equational -function definitions, `if let` bindings, and monadic `let` bindings with fallback clauses. - -In pattern-matches with multiple arms, this error may occur if a less-specific pattern precedes a -more-specific one that it subsumes. Bear in mind that expressions are matched against patterns from -top to bottom, so specific patterns should precede generic ones. - -In `if let` bindings and monadic `let` bindings with fallback clauses, in which only one pattern is -specified, this error indicates that the specified pattern will always be matched. In this case, the -binding in question can be replaced with a standard pattern-matching `let`. - -One common cause of this error is that a pattern that was intended to match a constructor was -instead interpreted as a variable binding. This occurs, for instance, if a constructor -name (e.g., `cons`) is written without its prefix (`List`) outside of that type's namespace. The -constructor-name-as-variable linter, enabled by default, will display a warning on any variable -patterns that resemble constructor names. - -This error nearly always indicates an issue with the code where it appears. If needed, however, -`set_option match.ignoreUnusedAlts true` will disable the check for this error and allow pattern -matches with redundant alternatives to be compiled by discarding the unused arms. - -# Examples - -## Incorrect Ordering of Pattern Matches - -```lean broken -def seconds : List (List α) → List α - | [] => [] - | _ :: xss => seconds xss - | (_ :: x :: _) :: xss => x :: seconds xss -``` -```output -Redundant alternative: Any expression matching - (head✝ :: x :: tail✝) :: xss -will match one of the preceding alternatives -``` -```lean fixed -def seconds : List (List α) → List α - | [] => [] - | (_ :: x :: _) :: xss => x :: seconds xss - | _ :: xss => seconds xss -``` - -Since any expression matching `(_ :: x :: _) :: xss` will also match `_ :: xss`, the last -alternative in the broken implementation is never reached. We resolve this by moving the more -specific alternative before the more general one. - -## Unnecessary Fallback Clause - -```lean broken -example (p : Nat × Nat) : IO Nat := do - let (m, n) := p - | return 0 - return m + n -``` -```output -Redundant alternative: Any expression matching - x✝ -will match one of the preceding alternatives -``` -```lean fixed -example (p : Nat × Nat) : IO Nat := do - let (m, n) := p - return m + n -``` - -Here, the fallback clause serves as a catch-all for all values of `p` that do not match `(m, n)`. -However, no such values exist, so the fallback clause is unnecessary and can be removed. A similar -error arises when using `if let pat := e` when `e` will always match `pat`. - -## Pattern Treated as Variable, Not Constructor - -```lean broken -example (xs : List Nat) : Bool := - match xs with - | nil => false - | _ => true -``` -```output -Redundant alternative: Any expression matching - x✝ -will match one of the preceding alternatives -``` -```lean fixed -example (xs : List Nat) : Bool := - match xs with - | .nil => false - | _ => true -``` - -In the original example, `nil` is treated as a variable, not as a constructor name, since this -definition is not within the `List` namespace. Thus, all values of `xs` will match the first -pattern, rendering the second unused. Notice that the constructor-name-as-variable linter displays a -warning at `nil`, indicating its similarity to a valid constructor name. Using dot-prefix notation, -as shown in the fixed example, or specifying the full constructor name `List.nil` achieves the -intended behavior. --/ -register_error_explanation lean.redundantMatchAlt { - summary := "Match alternative will never be reached." - sinceVersion := "4.22.0" -} diff --git a/src/Lean/ErrorExplanations/SynthInstanceFailed.lean b/src/Lean/ErrorExplanations/SynthInstanceFailed.lean deleted file mode 100644 index 8709b5e8ab8c..000000000000 --- a/src/Lean/ErrorExplanations/SynthInstanceFailed.lean +++ /dev/null @@ -1,125 +0,0 @@ -/- -Copyright (c) 2025 Lean FRO, LLC. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Rob Simmons --/ -module - -prelude -public import Lean.ErrorExplanation -meta import Lean.ErrorExplanation - -public section - -/-- -[Type classes](lean-manual://section/type-class) are the mechanism that Lean and many other -programming languages use to handle overloaded operations. The code that handles a particular -overloaded operation is an _instance_ of a typeclass; deciding which instance to use for a given -overloaded operation is called _synthesizing_ an instance. - -As an example, when Lean encounters an expression `x + y` where `x` and `y` both have type `Int`, -it is necessary to look up how it should add two integers and also look up what the resulting type -will be. This is described as synthesizing an instance of the type class `HAdd Int Int t` for some -type `t`. - -Many failures to synthesize an instance of a type class are the result of using the wrong binary -operation. Both success and failure are not always straightforward, because some instances are -defined in terms of other instances, and Lean must recursively search to find appropriate instances. -It's possible to inspect Lean's instance synthesis](lean-manual://section/instance-search), and this -can be helpful for diagnosing tricky failures of type class instance synthesis. - -# Examples - -## Using the Wrong Binary Operation - -```lean broken -#eval "A" + "3" -``` -```output -failed to synthesize instance of type class - HAdd String String ?m.4 - -Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. -``` -```lean fixed -#eval "A" ++ "3" -``` - -The binary operation `+` is associated with the `HAdd` type class, and there's no way to add two -strings. The binary operation `++`, associated with the `HAppend` type class, is the correct way to -append strings. - -## Arguments Have the Wrong Type - -```lean broken -def x : Int := 3 -#eval x ++ "meters" -``` -```output -failed to synthesize instance of type class - HAppend Int String ?m.4 - -Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. -``` -```lean fixed -def x : Int := 3 -#eval ToString.toString x ++ "meters" -``` - -Lean does not allow integers and strings to be added directly. The function `ToString.toString` uses -type class overloading to convert values to strings; by successfully searching for an instance of -`ToString Int`, the second example will succeed. - -## Missing Type Class Instance - -```lean broken -inductive MyColor where - | chartreuse | sienna | thistle - -def forceColor (oc : Option MyColor) := - oc.get! -``` -```output -failed to synthesize instance of type class - Inhabited MyColor - -Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command. -``` -```lean fixed (title := "Fixed (derive instance when defining type)") -inductive MyColor where - | chartreuse | sienna | thistle -deriving Inhabited - -def forceColor (oc : Option MyColor) := - oc.get! -``` -```lean fixed (title := "Fixed (derive instance separately)") -inductive MyColor where - | chartreuse | sienna | thistle - -deriving instance Inhabited for MyColor - -def forceColor (oc : Option MyColor) := - oc.get! -``` -```lean fixed (title := "Fixed (define instance)") -inductive MyColor where - | chartreuse | sienna | thistle - -instance : Inhabited MyColor where - default := .sienna - -def forceColor (oc : Option MyColor) := - oc.get! -``` - -Type class synthesis can fail because an instance of the type class simply needs to be provided. -This commonly happens for type classes like `Repr`, `BEq`, `ToJson` and `Inhabited`. Lean can often -[automatically generate instances of the type class with the `deriving` keyword](lean-manual://section/type-class), -either when the type is defined or with the stand-alone `deriving` command. - --/ -register_error_explanation lean.synthInstanceFailed { - summary := "Failed to synthesize instance of type class" - sinceVersion := "4.26.0" -} diff --git a/src/Lean/ErrorExplanations/UnknownIdentifier.lean b/src/Lean/ErrorExplanations/UnknownIdentifier.lean deleted file mode 100644 index 351a1f5c4488..000000000000 --- a/src/Lean/ErrorExplanations/UnknownIdentifier.lean +++ /dev/null @@ -1,236 +0,0 @@ -/- -Copyright (c) 2025 Lean FRO, LLC. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joseph Rotella --/ -module - -prelude -public import Lean.ErrorExplanation -meta 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 identifier `Std.HashSet.ofList` -``` -```lean fixed -public import Std.Data.HashSet.Basic - -public section - -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 constant `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. - -## Auto-bound variables - -```lean broken -set_option relaxedAutoImplicit false in -def thisBreaks (x : α₁) (y : size₁) := () - -set_option autoImplicit false in -def thisAlsoBreaks (x : α₂) (y : size₂) := () -``` -```output -Unknown identifier `size₁` - -Note: It is not possible to treat `size₁` as an implicitly bound variable here because it has multiple characters while the `relaxedAutoImplicit` option is set to `false`. -Unknown identifier `α₂` - -Note: It is not possible to treat `α₂` as an implicitly bound variable here because the `autoImplicit` option is set to `false`. -Unknown identifier `size₂` - -Note: It is not possible to treat `size₂` as an implicitly bound variable here because the `autoImplicit` option is set to `false`. -``` -```lean fixed (title := "Fixed (modifying options)") -set_option relaxedAutoImplicit true in -def thisWorks (x : α₁) (y : size₁) := () - -set_option autoImplicit true in -def thisAlsoWorks (x : α₂) (y : size₂) := () -``` -```lean fixed (title := "Fixed (add implicit bindings for the unknown identifiers)") -set_option relaxedAutoImplicit false in -def thisWorks {size₁} (x : α₁) (y : size₁) := () - -set_option autoImplicit false in -def thisAlsoWorks {α₂ size₂} (x : α₂) (y : size₂) := () -``` - -Lean's default behavior, when it encounters an identifier it can't identify in the type of a -definition, is to add [automatic implicit parameters](lean-manual://section/automatic-implicit-parameters) -for those unknown identifiers. However, many files or projects disable this feature by setting the -`autoImplicit` or `relaxedAutoImplicit` options to `false`. - -Without re-enabling the `autoImplicit` or `relaxedAutoImplicit` options, the easiest way to fix -this error is to add the unknown identifiers as [ordinary implicit parameters](lean-manual://section/implicit-functions) -as shown in the example above. - --/ -register_error_explanation lean.unknownIdentifier { - summary := "Failed to resolve identifier to variable or constant." - sinceVersion := "4.23.0" -} From 6b104e0ca83013b65d1a5a8132268d1bb268d87a Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Tue, 16 Dec 2025 21:05:08 -0500 Subject: [PATCH 06/11] More deletion --- src/Lean.lean | 1 - src/Lean/Elab/ErrorExplanation.lean | 4 +- src/Lean/ErrorExplanation.lean | 240 ++++++++++++---------------- src/Lean/ErrorExplanations.lean | 93 ----------- src/Lean/Exception.lean | 2 +- src/Lean/Log.lean | 2 +- 6 files changed, 102 insertions(+), 240 deletions(-) delete mode 100644 src/Lean/ErrorExplanations.lean diff --git a/src/Lean.lean b/src/Lean.lean index c708d08fb755..d52a3488dc9c 100644 --- a/src/Lean.lean +++ b/src/Lean.lean @@ -44,7 +44,6 @@ public import Lean.LibrarySuggestions public import Lean.Namespace public import Lean.EnvExtension public import Lean.ErrorExplanation -public import Lean.ErrorExplanations public import Lean.DefEqAttrib public import Lean.Shell public import Lean.ExtraModUses diff --git a/src/Lean/Elab/ErrorExplanation.lean b/src/Lean/Elab/ErrorExplanation.lean index f7981ccf5214..160b8e9c226f 100644 --- a/src/Lean/Elab/ErrorExplanation.lean +++ b/src/Lean/Elab/ErrorExplanation.lean @@ -89,8 +89,8 @@ def elabCheckedNamedError : TermElab := fun stx expType? => do logWarningAt id m!"The error name `{name}` was removed in Lean version {removedVersion} and \ should not be used." else - logErrorAt id m!"There is no explanation associated with the name `{name}`. \ - Add an explanation of this error to the `Lean.ErrorExplanations` module." + logErrorAt id m!"There is no explanation registered with the name `{name}`. \ + Register an explanation for this error in the `Lean.ErrorExplanation` module." let stx' ← liftMacroM <| expandNamedErrorMacro stx elabTerm stx' expType? diff --git a/src/Lean/ErrorExplanation.lean b/src/Lean/ErrorExplanation.lean index 9e35b3606019..4ab04b6e9e2c 100644 --- a/src/Lean/ErrorExplanation.lean +++ b/src/Lean/ErrorExplanation.lean @@ -43,151 +43,13 @@ structure ErrorExplanation where metadata : ErrorExplanation.Metadata declLoc? : Option DeclarationLocation -namespace ErrorExplanation - /-- Returns the error explanation summary prepended with its severity. For use in completions and hovers. -/ -def summaryWithSeverity (explan : ErrorExplanation) : String := +def ErrorExplanation.summaryWithSeverity (explan : ErrorExplanation) : String := s!"({explan.metadata.severity}) {explan.metadata.summary}" -/-- -The kind of a code block in an error explanation example. `broken` blocks raise the diagnostic being -explained; `fixed` blocks must compile successfully. --/ -inductive CodeInfo.Kind - | broken | fixed - deriving Repr, Inhabited, BEq - -instance : ToString CodeInfo.Kind where - toString - | .broken => "broken" - | .fixed => "fixed" - -def CodeInfo.Kind.ofString : String → Option CodeInfo.Kind - | "broken" => some .broken - | "fixed" => some .fixed - | _ => none - -/-- Metadata about a code block in an error explanation, parsed from the block's info string. -/ -structure CodeInfo where - lang : String - kind? : Option CodeInfo.Kind - title? : Option String -deriving Repr - -open Std.Internal Parsec Parsec.String in -/-- Parse metadata for an error explanation code block from its info string. -/ -def CodeInfo.parse (s : String) : Except String CodeInfo := - infoString.run s |>.mapError (fun e => s!"Invalid code block info string `{s}`: {e}") -where - /-- Parses the contents of a string literal up to, but excluding, the closing quotation mark. -/ - stringContents : Parser String := attempt do - let escaped := pchar '\\' *> pchar '"' - let cs ← many (notFollowedBy (pchar '"') *> (escaped <|> any)) - return String.ofList cs.toList - - /-- - Parses all input up to the next whitespace. If `nonempty` is `true`, fails if there is no input - prior to the next whitespace. - -/ - upToWs (nonempty : Bool) : Parser String := fun it => - let it' := (it.2.find? fun (c : Char) => c.isWhitespace).getD it.1.endPos - if nonempty && it' == it.2 then - .error ⟨_, it'⟩ (.other "Expected a nonempty string") - else - .success ⟨_, it'⟩ (it.1.slice! it.2 it').copy - - /-- Parses a named attribute, and returns its name and value. -/ - namedAttr : Parser (String × String) := attempt do - let name ← skipChar '(' *> ws *> (upToWs true) - let contents ← ws *> skipString ":=" *> ws *> skipChar '"' *> stringContents - discard <| skipChar '"' *> ws *> skipChar ')' - return (name, contents) - - /-- - Parses an "attribute" in an info string, either a space-delineated identifier or a named - attribute of the form `(name := "value")`. - -/ - attr : Parser (String ⊕ String × String) := - .inr <$> namedAttr <|> .inl <$> (upToWs true) - - infoString : Parser CodeInfo := do - let lang ← upToWs false - let attrs ← many (attempt <| ws *> attr) - let mut kind? := Option.none - let mut title? := Option.none - for attr in attrs do - match attr with - | .inl atomicAttr => - match atomicAttr with - | "broken" | "fixed" => - match kind? with - | none => kind? := Kind.ofString atomicAttr - | some kind => - fail s!"Redundant kind specifications: previously `{kind}`; now `{atomicAttr}`" - | _ => fail s!"Invalid attribute `{atomicAttr}`" - | .inr (name, val) => - if name == "title" then - if title?.isNone then - title? := some val - else - fail "Redundant title specifications" - else - fail s!"Invalid named attribute `{name}`; expected `title`" - return { lang, title?, kind? } - -open Std.Internal Parsec - -/-- -An iterator storing nonempty lines in an error explanation together with their original line -numbers. --/ -private structure ValidationState where - lines : Array (String × Nat) - idx : Nat := 0 -deriving Repr, Inhabited - -/-- Creates an iterator for validation from the raw contents of an error explanation. -/ -private def ValidationState.ofSource (input : String) : ValidationState where - lines := input.split '\n' - |>.filter (!·.trimAscii.isEmpty) - |>.toStringArray - |>.zipIdx - --- Workaround to account for the fact that `Input` expects "EOF" to be a valid position -private def ValidationState.get (s : ValidationState) := - if _ : s.idx < s.lines.size then - s.lines[s.idx].1 - else - "" - -private def ValidationState.getLineNumber (s : ValidationState) := - if _ : s.lines.size = 0 then - 0 - else - s.lines[min s.idx (s.lines.size - 1)].2 - -private instance : Input ValidationState String Nat where - pos := ValidationState.idx - next := fun s => { s with idx := min (s.idx + 1) s.lines.size } - curr := ValidationState.get - hasNext := fun s => s.idx < s.lines.size - next' := fun s _ => { s with idx := s.idx + 1 } - curr' := fun s _ => s.get - -private abbrev ValidationM := Parsec ValidationState - -private def ValidationM.run (p : ValidationM α) (input : String) : Except (Nat × String) α := - match p (.ofSource input) with - | .success _ res => Except.ok res - | .error s err => Except.error (s.getLineNumber, toString err) - - - -end ErrorExplanation - /-- An environment extension that stores error explanations. -/ builtin_initialize errorExplanationExt : SimplePersistentEnvExtension (Name × ErrorExplanation) (NameMap ErrorExplanation) ← registerSimplePersistentEnvExtension { @@ -221,17 +83,111 @@ links. In general, use `Lean.getErrorExplanations` or `Lean.getErrorExplanationsSorted` instead of this function if the bodies of the fetched explanations will be used. -/ -def getErrorExplanationsRaw (env : Environment) : Array (Name × ErrorExplanation) := +public def getErrorExplanationsRaw (env : Environment) : Array (Name × ErrorExplanation) := errorExplanationExt.getState env |>.toArray /-- Returns all error explanations with their names, rewriting manual links. -/ -def getErrorExplanations [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] : m (Array (Name × ErrorExplanation)) := do +public def getErrorExplanations [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] : m (Array (Name × ErrorExplanation)) := do return errorExplanationExt.getState (← getEnv) |>.toArray /-- Returns all error explanations with their names as a sorted array, rewriting manual links. -/ -def getErrorExplanationsSorted [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] : m (Array (Name × ErrorExplanation)) := do +public def getErrorExplanationsSorted [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] : m (Array (Name × ErrorExplanation)) := do return (← getErrorExplanations).qsort fun e e' => e.1.toString < e'.1.toString end Lean + +/- +Error explanations registered in the compiler must be added to the manual and +referenced in the Manual.ErrorExplanations module here: + +https://github.com/leanprover/reference-manual/blob/main/Manual/ErrorExplanations.lean + +Details: +https://github.com/leanprover/reference-manual/blob/main/Manual/ErrorExplanations/README.md +-/ + +/-- -/ +register_error_explanation lean.ctorResultingTypeMismatch { + summary := "Resulting type of constructor was not the inductive type being declared." + sinceVersion := "4.22.0" +} + +/-- -/ +register_error_explanation lean.dependsOnNoncomputable { + summary := "Declaration depends on noncomputable definitions but is not marked as noncomputable" + sinceVersion := "4.22.0" +} + +/-- -/ +register_error_explanation lean.inductionWithNoAlts { + summary := "Induction pattern with nontactic in natural-number-game-style `with` clause." + sinceVersion := "4.26.0" +} + +/-- -/ +register_error_explanation lean.inductiveParamMismatch { + summary := " Invalid parameter in an occurrence of an inductive type in one of its constructors." + sinceVersion := "4.22.0" +} + +/-- -/ +register_error_explanation lean.inductiveParamMissing { + summary := "Parameter not present in an occurrence of an inductive type in one of its constructors." + sinceVersion := "4.22.0" +} + +/-- -/ +register_error_explanation lean.inferBinderTypeFailed { + summary := "The type of a binder could not be inferred." + sinceVersion := "4.23.0" +} + +/-- -/ +register_error_explanation lean.inferDefTypeFailed { + summary := "The type of a definition could not be inferred." + sinceVersion := "4.23.0" +} + +/-- -/ +register_error_explanation lean.invalidDottedIdent { + summary := "Dotted identifier notation used with invalid or non-inferrable expected type." + sinceVersion := "4.22.0" +} + +/-- -/ +register_error_explanation lean.invalidField { + summary := "Generalized field notation used in a potentially ambiguous way." + sinceVersion := "4.22.0" +} + +/-- -/ +register_error_explanation lean.projNonPropFromProp { + summary := "Tried to project data from a proof." + sinceVersion := "4.23.0" +} + +/-- -/ +register_error_explanation lean.propRecLargeElim { + summary := "Attempted to eliminate a proof into a higher type universe." + sinceVersion := "4.23.0" +} + +/-- -/ +register_error_explanation lean.redundantMatchAlt { + summary := "Match alternative will never be reached." + sinceVersion := "4.22.0" +} + +/-- -/ +register_error_explanation lean.synthInstanceFailed { + summary := "Failed to synthesize instance of type class." + sinceVersion := "4.26.0" +} + +/-- -/ +register_error_explanation lean.unknownIdentifier { + summary := "Failed to resolve identifier to variable or constant." + sinceVersion := "4.23.0" +} diff --git a/src/Lean/ErrorExplanations.lean b/src/Lean/ErrorExplanations.lean deleted file mode 100644 index a0d4c611d28b..000000000000 --- a/src/Lean/ErrorExplanations.lean +++ /dev/null @@ -1,93 +0,0 @@ -/- -Copyright (c) 2025 Lean FRO, LLC. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joseph Rotella --/ -module - -prelude -public import Lean.ErrorExplanation - -/-- -/ -register_error_explanation lean.ctorResultingTypeMismatch { - summary := "Resulting type of constructor was not the inductive type being declared." - sinceVersion := "4.22.0" -} - -/-- -/ -register_error_explanation lean.dependsOnNoncomputable { - summary := "Declaration depends on noncomputable definitions but is not marked as noncomputable" - sinceVersion := "4.22.0" -} - -/-- -/ -register_error_explanation lean.inductionWithNoAlts { - summary := "Induction pattern with nontactic in natural-number-game-style `with` clause." - sinceVersion := "4.26.0" -} - -/-- -/ -register_error_explanation lean.inductiveParamMismatch { - summary := " Invalid parameter in an occurrence of an inductive type in one of its constructors." - sinceVersion := "4.22.0" -} - -/-- -/ -register_error_explanation lean.inductiveParamMissing { - summary := "Parameter not present in an occurrence of an inductive type in one of its constructors." - sinceVersion := "4.22.0" -} - -/-- -/ -register_error_explanation lean.inferBinderTypeFailed { - summary := "The type of a binder could not be inferred." - sinceVersion := "4.23.0" -} - -/-- -/ -register_error_explanation lean.inferDefTypeFailed { - summary := "The type of a definition could not be inferred." - sinceVersion := "4.23.0" -} - -/-- -/ -register_error_explanation lean.invalidDottedIdent { - summary := "Dotted identifier notation used with invalid or non-inferrable expected type." - sinceVersion := "4.22.0" -} - -/-- -/ -register_error_explanation lean.invalidField { - summary := "Generalized field notation used in a potentially ambiguous way." - sinceVersion := "4.22.0" -} - -/-- -/ -register_error_explanation lean.projNonPropFromProp { - summary := "Tried to project data from a proof." - sinceVersion := "4.23.0" -} - -/-- -/ -register_error_explanation lean.propRecLargeElim { - summary := "Attempted to eliminate a proof into a higher type universe." - sinceVersion := "4.23.0" -} - -/-- -/ -register_error_explanation lean.redundantMatchAlt { - summary := "Match alternative will never be reached." - sinceVersion := "4.22.0" -} - -/-- -/ -register_error_explanation lean.synthInstanceFailed { - summary := "Failed to synthesize instance of type class." - sinceVersion := "4.26.0" -} - -/-- -/ -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 728664891560..a8e107eac5a9 100644 --- a/src/Lean/Exception.lean +++ b/src/Lean/Exception.lean @@ -9,7 +9,7 @@ prelude public import Lean.InternalExceptionId -- This import is necessary to ensure that any users of the `throwNamedError` macros have access to -- all declared explanations: -public import Lean.ErrorExplanations +public import Lean.ErrorExplanation public section diff --git a/src/Lean/Log.lean b/src/Lean/Log.lean index f329a2e49a01..3d40ada008ff 100644 --- a/src/Lean/Log.lean +++ b/src/Lean/Log.lean @@ -8,7 +8,7 @@ module prelude -- This import is necessary to ensure that any users of the `logNamedError` macros have access to -- all declared explanations: -public import Lean.ErrorExplanations +public import Lean.ErrorExplanation public section From e64a4f1ac3c8ece3ee08ca8dbf1ff353e1080a89 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Fri, 19 Dec 2025 20:42:15 -0500 Subject: [PATCH 07/11] Add back in 'doc' field, with the hunch it could be causing reference manual segfault --- src/Lean/Elab/ErrorExplanation.lean | 2 +- src/Lean/ErrorExplanation.lean | 2 ++ 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/Lean/Elab/ErrorExplanation.lean b/src/Lean/Elab/ErrorExplanation.lean index 160b8e9c226f..6e3aff0de910 100644 --- a/src/Lean/Elab/ErrorExplanation.lean +++ b/src/Lean/Elab/ErrorExplanation.lean @@ -126,5 +126,5 @@ open Command in module := (← getMainModule) range := .ofStringPositions map start fin } - modifyEnv (errorExplanationExt.addEntry · (name, { metadata, declLoc? })) + modifyEnv (errorExplanationExt.addEntry · (name, { doc := "", metadata, declLoc? })) | _ => throwUnsupportedSyntax diff --git a/src/Lean/ErrorExplanation.lean b/src/Lean/ErrorExplanation.lean index 4ab04b6e9e2c..0293b40623ec 100644 --- a/src/Lean/ErrorExplanation.lean +++ b/src/Lean/ErrorExplanation.lean @@ -40,6 +40,8 @@ Error explanations are rendered in the manual; a link to the resulting manual pa the bottom of corresponding error messages thrown using `throwNamedError` or `throwNamedErrorAt`. -/ structure ErrorExplanation where + /-- The `doc` field is deprecated and should always be the empty string -/ + doc : String metadata : ErrorExplanation.Metadata declLoc? : Option DeclarationLocation From b96018c297bc2253e4734ce899ef7800548dce30 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Sat, 20 Dec 2025 12:38:05 -0500 Subject: [PATCH 08/11] Deprecations and simplified interfaces --- src/Lean/ErrorExplanation.lean | 40 ++++++++++++++-------------------- 1 file changed, 16 insertions(+), 24 deletions(-) diff --git a/src/Lean/ErrorExplanation.lean b/src/Lean/ErrorExplanation.lean index 0293b40623ec..fec79db5f47a 100644 --- a/src/Lean/ErrorExplanation.lean +++ b/src/Lean/ErrorExplanation.lean @@ -62,41 +62,33 @@ builtin_initialize errorExplanationExt : SimplePersistentEnvExtension (Name × E acc.insert n v } -/-- Returns an error explanation for the given name if one exists, rewriting manual links. -/ -def getErrorExplanation? [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] (name : Name) : m (Option ErrorExplanation) := do +/-- Returns an error explanation for the given name if one exists. -/ +def getErrorExplanation? [Monad m] [MonadEnv m] (name : Name) : m (Option ErrorExplanation) := do return errorExplanationExt.getState (← getEnv) |>.find? name -/-- -Returns an error explanation for the given name if one exists *without* rewriting manual links. - -In general, use `Lean.getErrorExplanation?` instead if the body of the explanation will be used. --/ +@[deprecated getErrorExplanation? (since := "2026-12-20")] def getErrorExplanationRaw? (env : Environment) (name : Name) : Option ErrorExplanation := do errorExplanationExt.getState env |>.find? name /-- Returns `true` if there exists an error explanation named `name`. -/ -def hasErrorExplanation [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] (name : Name) : m Bool := +def hasErrorExplanation [Monad m] [MonadEnv m] (name : Name) : m Bool := return errorExplanationExt.getState (← getEnv) |>.contains name -/-- -Returns all error explanations with their names as an unsorted array, *without* rewriting manual -links. +/-- Returns all error explanations with their names, sorted by name. -/ +public def getErrorExplanations [Monad m] [MonadEnv m] : m (Array (Name × ErrorExplanation)) := do + return errorExplanationExt.getState (← getEnv) + |>.toArray + |>.qsort fun e e' => e.1.toString < e'.1.toString -In general, use `Lean.getErrorExplanations` or `Lean.getErrorExplanationsSorted` instead of this -function if the bodies of the fetched explanations will be used. --/ +@[deprecated getErrorExplanations (since := "2026-12-20")] public def getErrorExplanationsRaw (env : Environment) : Array (Name × ErrorExplanation) := - errorExplanationExt.getState env |>.toArray - -/-- Returns all error explanations with their names, rewriting manual links. -/ -public def getErrorExplanations [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] : m (Array (Name × ErrorExplanation)) := do - return errorExplanationExt.getState (← getEnv) |>.toArray + errorExplanationExt.getState env + |>.toArray + |>.qsort fun e e' => e.1.toString < e'.1.toString -/-- -Returns all error explanations with their names as a sorted array, rewriting manual links. --/ -public def getErrorExplanationsSorted [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] : m (Array (Name × ErrorExplanation)) := do - return (← getErrorExplanations).qsort fun e e' => e.1.toString < e'.1.toString +@[deprecated getErrorExplanations (since := "2026-12-20")] +public def getErrorExplanationsSorted [Monad m] [MonadEnv m] : m (Array (Name × ErrorExplanation)) := do + getErrorExplanations end Lean From 76ffa312e0891574f16785c711d3331baa8e3fe6 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Sat, 20 Dec 2025 12:43:22 -0500 Subject: [PATCH 09/11] Fix deprecation --- src/Lean/Server/InfoUtils.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean index 6fde2489dad0..b45ba908e944 100644 --- a/src/Lean/Server/InfoUtils.lean +++ b/src/Lean/Server/InfoUtils.lean @@ -342,7 +342,7 @@ def Info.docString? (i : Info) : MetaM (Option String) := do return decl.fullDescr return none | .ofErrorNameInfo eni => do - let some errorExplanation := getErrorExplanationRaw? (← getEnv) eni.errorName | return none + let some errorExplanation ← getErrorExplanation? eni.errorName | return none return errorExplanation.summaryWithSeverity | .ofDocInfo di => return (← findDocString? env di.stx.getKind) From 6c093a5f4c11066fe5641959e8255b2aa2d045d8 Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Sat, 20 Dec 2025 14:50:11 -0500 Subject: [PATCH 10/11] autocompletion order changes because of alpha-sorting getErrorExplanations --- ...orExplanationInteractive.lean.expected.out | 140 +++++++++--------- 1 file changed, 70 insertions(+), 70 deletions(-) diff --git a/tests/lean/interactive/errorExplanationInteractive.lean.expected.out b/tests/lean/interactive/errorExplanationInteractive.lean.expected.out index ae55c92d9c6f..f727eac4eceb 100644 --- a/tests/lean/interactive/errorExplanationInteractive.lean.expected.out +++ b/tests/lean/interactive/errorExplanationInteractive.lean.expected.out @@ -5,82 +5,82 @@ {"replace": {"start": {"line": 28, "character": 23}, "end": {"line": 28, "character": 30}}, - "newText": "testPkg.foo2", + "newText": "testPkg.bar", "insert": {"start": {"line": 28, "character": 23}, "end": {"line": 28, "character": 30}}}, - "label": "testPkg.foo2", + "label": "testPkg.bar", "kind": 10, - "documentation": {"value": "(error) Error 2", "kind": "markdown"}, + "documentation": {"value": "(error) Error 0", "kind": "markdown"}, "detail": "error name", "data": ["«external:file:///errorExplanationInteractive.lean»", 28, 30, 0]}, {"textEdit": {"replace": {"start": {"line": 28, "character": 23}, "end": {"line": 28, "character": 30}}, - "newText": "testPkg.bar", + "newText": "testPkg.foo1", "insert": {"start": {"line": 28, "character": 23}, "end": {"line": 28, "character": 30}}}, - "label": "testPkg.bar", + "label": "testPkg.foo1", "kind": 10, - "documentation": {"value": "(error) Error 0", "kind": "markdown"}, + "documentation": {"value": "(error) Error 1", "kind": "markdown"}, "detail": "error name", "data": ["«external:file:///errorExplanationInteractive.lean»", 28, 30, 0]}, {"textEdit": {"replace": {"start": {"line": 28, "character": 23}, "end": {"line": 28, "character": 30}}, - "newText": "testPkg.foo1", + "newText": "testPkg.foo2", "insert": {"start": {"line": 28, "character": 23}, "end": {"line": 28, "character": 30}}}, - "label": "testPkg.foo1", + "label": "testPkg.foo2", "kind": 10, - "documentation": {"value": "(error) Error 1", "kind": "markdown"}, + "documentation": {"value": "(error) Error 2", "kind": "markdown"}, "detail": "error name", "data": ["«external:file:///errorExplanationInteractive.lean»", 28, 30, 0]}], "isIncomplete": false} -Resolution of testPkg.foo2: +Resolution of testPkg.bar: {"textEdit": {"replace": {"start": {"line": 28, "character": 23}, "end": {"line": 28, "character": 30}}, - "newText": "testPkg.foo2", + "newText": "testPkg.bar", "insert": {"start": {"line": 28, "character": 23}, "end": {"line": 28, "character": 30}}}, - "label": "testPkg.foo2", + "label": "testPkg.bar", "kind": 10, - "documentation": {"value": "(error) Error 2", "kind": "markdown"}, + "documentation": {"value": "(error) Error 0", "kind": "markdown"}, "detail": "error name", "data": ["«external:file:///errorExplanationInteractive.lean»", 28, 30, 0]} -Resolution of testPkg.bar: +Resolution of testPkg.foo1: {"textEdit": {"replace": {"start": {"line": 28, "character": 23}, "end": {"line": 28, "character": 30}}, - "newText": "testPkg.bar", + "newText": "testPkg.foo1", "insert": {"start": {"line": 28, "character": 23}, "end": {"line": 28, "character": 30}}}, - "label": "testPkg.bar", + "label": "testPkg.foo1", "kind": 10, - "documentation": {"value": "(error) Error 0", "kind": "markdown"}, + "documentation": {"value": "(error) Error 1", "kind": "markdown"}, "detail": "error name", "data": ["«external:file:///errorExplanationInteractive.lean»", 28, 30, 0]} -Resolution of testPkg.foo1: +Resolution of testPkg.foo2: {"textEdit": {"replace": {"start": {"line": 28, "character": 23}, "end": {"line": 28, "character": 30}}, - "newText": "testPkg.foo1", + "newText": "testPkg.foo2", "insert": {"start": {"line": 28, "character": 23}, "end": {"line": 28, "character": 30}}}, - "label": "testPkg.foo1", + "label": "testPkg.foo2", "kind": 10, - "documentation": {"value": "(error) Error 1", "kind": "markdown"}, + "documentation": {"value": "(error) Error 2", "kind": "markdown"}, "detail": "error name", "data": ["«external:file:///errorExplanationInteractive.lean»", 28, 30, 0]} {"textDocument": {"uri": "file:///errorExplanationInteractive.lean"}, @@ -90,82 +90,82 @@ Resolution of testPkg.foo1: {"replace": {"start": {"line": 30, "character": 23}, "end": {"line": 30, "character": 31}}, - "newText": "testPkg.foo2", + "newText": "testPkg.bar", "insert": {"start": {"line": 30, "character": 23}, "end": {"line": 30, "character": 31}}}, - "label": "testPkg.foo2", + "label": "testPkg.bar", "kind": 10, - "documentation": {"value": "(error) Error 2", "kind": "markdown"}, + "documentation": {"value": "(error) Error 0", "kind": "markdown"}, "detail": "error name", "data": ["«external:file:///errorExplanationInteractive.lean»", 30, 31, 0]}, {"textEdit": {"replace": {"start": {"line": 30, "character": 23}, "end": {"line": 30, "character": 31}}, - "newText": "testPkg.bar", + "newText": "testPkg.foo1", "insert": {"start": {"line": 30, "character": 23}, "end": {"line": 30, "character": 31}}}, - "label": "testPkg.bar", + "label": "testPkg.foo1", "kind": 10, - "documentation": {"value": "(error) Error 0", "kind": "markdown"}, + "documentation": {"value": "(error) Error 1", "kind": "markdown"}, "detail": "error name", "data": ["«external:file:///errorExplanationInteractive.lean»", 30, 31, 0]}, {"textEdit": {"replace": {"start": {"line": 30, "character": 23}, "end": {"line": 30, "character": 31}}, - "newText": "testPkg.foo1", + "newText": "testPkg.foo2", "insert": {"start": {"line": 30, "character": 23}, "end": {"line": 30, "character": 31}}}, - "label": "testPkg.foo1", + "label": "testPkg.foo2", "kind": 10, - "documentation": {"value": "(error) Error 1", "kind": "markdown"}, + "documentation": {"value": "(error) Error 2", "kind": "markdown"}, "detail": "error name", "data": ["«external:file:///errorExplanationInteractive.lean»", 30, 31, 0]}], "isIncomplete": false} -Resolution of testPkg.foo2: +Resolution of testPkg.bar: {"textEdit": {"replace": {"start": {"line": 30, "character": 23}, "end": {"line": 30, "character": 31}}, - "newText": "testPkg.foo2", + "newText": "testPkg.bar", "insert": {"start": {"line": 30, "character": 23}, "end": {"line": 30, "character": 31}}}, - "label": "testPkg.foo2", + "label": "testPkg.bar", "kind": 10, - "documentation": {"value": "(error) Error 2", "kind": "markdown"}, + "documentation": {"value": "(error) Error 0", "kind": "markdown"}, "detail": "error name", "data": ["«external:file:///errorExplanationInteractive.lean»", 30, 31, 0]} -Resolution of testPkg.bar: +Resolution of testPkg.foo1: {"textEdit": {"replace": {"start": {"line": 30, "character": 23}, "end": {"line": 30, "character": 31}}, - "newText": "testPkg.bar", + "newText": "testPkg.foo1", "insert": {"start": {"line": 30, "character": 23}, "end": {"line": 30, "character": 31}}}, - "label": "testPkg.bar", + "label": "testPkg.foo1", "kind": 10, - "documentation": {"value": "(error) Error 0", "kind": "markdown"}, + "documentation": {"value": "(error) Error 1", "kind": "markdown"}, "detail": "error name", "data": ["«external:file:///errorExplanationInteractive.lean»", 30, 31, 0]} -Resolution of testPkg.foo1: +Resolution of testPkg.foo2: {"textEdit": {"replace": {"start": {"line": 30, "character": 23}, "end": {"line": 30, "character": 31}}, - "newText": "testPkg.foo1", + "newText": "testPkg.foo2", "insert": {"start": {"line": 30, "character": 23}, "end": {"line": 30, "character": 31}}}, - "label": "testPkg.foo1", + "label": "testPkg.foo2", "kind": 10, - "documentation": {"value": "(error) Error 1", "kind": "markdown"}, + "documentation": {"value": "(error) Error 2", "kind": "markdown"}, "detail": "error name", "data": ["«external:file:///errorExplanationInteractive.lean»", 30, 31, 0]} {"textDocument": {"uri": "file:///errorExplanationInteractive.lean"}, @@ -175,55 +175,55 @@ Resolution of testPkg.foo1: {"replace": {"start": {"line": 32, "character": 23}, "end": {"line": 32, "character": 32}}, - "newText": "testPkg.foo2", + "newText": "testPkg.foo1", "insert": {"start": {"line": 32, "character": 23}, "end": {"line": 32, "character": 32}}}, - "label": "testPkg.foo2", + "label": "testPkg.foo1", "kind": 10, - "documentation": {"value": "(error) Error 2", "kind": "markdown"}, + "documentation": {"value": "(error) Error 1", "kind": "markdown"}, "detail": "error name", "data": ["«external:file:///errorExplanationInteractive.lean»", 32, 32, 0]}, {"textEdit": {"replace": {"start": {"line": 32, "character": 23}, "end": {"line": 32, "character": 32}}, - "newText": "testPkg.foo1", + "newText": "testPkg.foo2", "insert": {"start": {"line": 32, "character": 23}, "end": {"line": 32, "character": 32}}}, - "label": "testPkg.foo1", + "label": "testPkg.foo2", "kind": 10, - "documentation": {"value": "(error) Error 1", "kind": "markdown"}, + "documentation": {"value": "(error) Error 2", "kind": "markdown"}, "detail": "error name", "data": ["«external:file:///errorExplanationInteractive.lean»", 32, 32, 0]}], "isIncomplete": false} -Resolution of testPkg.foo2: +Resolution of testPkg.foo1: {"textEdit": {"replace": {"start": {"line": 32, "character": 23}, "end": {"line": 32, "character": 32}}, - "newText": "testPkg.foo2", + "newText": "testPkg.foo1", "insert": {"start": {"line": 32, "character": 23}, "end": {"line": 32, "character": 32}}}, - "label": "testPkg.foo2", + "label": "testPkg.foo1", "kind": 10, - "documentation": {"value": "(error) Error 2", "kind": "markdown"}, + "documentation": {"value": "(error) Error 1", "kind": "markdown"}, "detail": "error name", "data": ["«external:file:///errorExplanationInteractive.lean»", 32, 32, 0]} -Resolution of testPkg.foo1: +Resolution of testPkg.foo2: {"textEdit": {"replace": {"start": {"line": 32, "character": 23}, "end": {"line": 32, "character": 32}}, - "newText": "testPkg.foo1", + "newText": "testPkg.foo2", "insert": {"start": {"line": 32, "character": 23}, "end": {"line": 32, "character": 32}}}, - "label": "testPkg.foo1", + "label": "testPkg.foo2", "kind": 10, - "documentation": {"value": "(error) Error 1", "kind": "markdown"}, + "documentation": {"value": "(error) Error 2", "kind": "markdown"}, "detail": "error name", "data": ["«external:file:///errorExplanationInteractive.lean»", 32, 32, 0]} {"textDocument": {"uri": "file:///errorExplanationInteractive.lean"}, @@ -233,55 +233,55 @@ Resolution of testPkg.foo1: {"replace": {"start": {"line": 34, "character": 23}, "end": {"line": 34, "character": 32}}, - "newText": "testPkg.foo2", + "newText": "testPkg.foo1", "insert": {"start": {"line": 34, "character": 23}, "end": {"line": 34, "character": 32}}}, - "label": "testPkg.foo2", + "label": "testPkg.foo1", "kind": 10, - "documentation": {"value": "(error) Error 2", "kind": "markdown"}, + "documentation": {"value": "(error) Error 1", "kind": "markdown"}, "detail": "error name", "data": ["«external:file:///errorExplanationInteractive.lean»", 34, 32, 0]}, {"textEdit": {"replace": {"start": {"line": 34, "character": 23}, "end": {"line": 34, "character": 32}}, - "newText": "testPkg.foo1", + "newText": "testPkg.foo2", "insert": {"start": {"line": 34, "character": 23}, "end": {"line": 34, "character": 32}}}, - "label": "testPkg.foo1", + "label": "testPkg.foo2", "kind": 10, - "documentation": {"value": "(error) Error 1", "kind": "markdown"}, + "documentation": {"value": "(error) Error 2", "kind": "markdown"}, "detail": "error name", "data": ["«external:file:///errorExplanationInteractive.lean»", 34, 32, 0]}], "isIncomplete": false} -Resolution of testPkg.foo2: +Resolution of testPkg.foo1: {"textEdit": {"replace": {"start": {"line": 34, "character": 23}, "end": {"line": 34, "character": 32}}, - "newText": "testPkg.foo2", + "newText": "testPkg.foo1", "insert": {"start": {"line": 34, "character": 23}, "end": {"line": 34, "character": 32}}}, - "label": "testPkg.foo2", + "label": "testPkg.foo1", "kind": 10, - "documentation": {"value": "(error) Error 2", "kind": "markdown"}, + "documentation": {"value": "(error) Error 1", "kind": "markdown"}, "detail": "error name", "data": ["«external:file:///errorExplanationInteractive.lean»", 34, 32, 0]} -Resolution of testPkg.foo1: +Resolution of testPkg.foo2: {"textEdit": {"replace": {"start": {"line": 34, "character": 23}, "end": {"line": 34, "character": 32}}, - "newText": "testPkg.foo1", + "newText": "testPkg.foo2", "insert": {"start": {"line": 34, "character": 23}, "end": {"line": 34, "character": 32}}}, - "label": "testPkg.foo1", + "label": "testPkg.foo2", "kind": 10, - "documentation": {"value": "(error) Error 1", "kind": "markdown"}, + "documentation": {"value": "(error) Error 2", "kind": "markdown"}, "detail": "error name", "data": ["«external:file:///errorExplanationInteractive.lean»", 34, 32, 0]} {"textDocument": {"uri": "file:///errorExplanationInteractive.lean"}, From 20f2ece16641258d9d5765c165045e6887fc2cca Mon Sep 17 00:00:00 2001 From: Rob Simmons Date: Sat, 20 Dec 2025 16:38:31 -0500 Subject: [PATCH 11/11] stop using deprecated functions --- src/Lean/Elab/ErrorExplanation.lean | 2 +- src/Lean/Server/Completion/CompletionCollectors.lean | 2 +- src/Lean/Server/GoTo.lean | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/Lean/Elab/ErrorExplanation.lean b/src/Lean/Elab/ErrorExplanation.lean index 6e3aff0de910..1c429d6fac4f 100644 --- a/src/Lean/Elab/ErrorExplanation.lean +++ b/src/Lean/Elab/ErrorExplanation.lean @@ -84,7 +84,7 @@ def elabCheckedNamedError : TermElab := fun stx expType? => do addCompletionInfo <| CompletionInfo.errorName span partialId let name := id.getId.eraseMacroScopes pushInfoLeaf <| .ofErrorNameInfo { stx := id, errorName := name } - if let some explan := getErrorExplanationRaw? (← getEnv) name then + if let some explan ← getErrorExplanation? name then if let some removedVersion := explan.metadata.removedVersion? then logWarningAt id m!"The error name `{name}` was removed in Lean version {removedVersion} and \ should not be used." diff --git a/src/Lean/Server/Completion/CompletionCollectors.lean b/src/Lean/Server/Completion/CompletionCollectors.lean index 3998fc14ebd3..64abd78e47a6 100644 --- a/src/Lean/Server/Completion/CompletionCollectors.lean +++ b/src/Lean/Server/Completion/CompletionCollectors.lean @@ -571,7 +571,7 @@ def errorNameCompletion (caps : ClientCapabilities) : IO (Array ResolvableCompletionItem) := ctx.runMetaM {} do - let explanations := getErrorExplanationsRaw (← getEnv) + let explanations ← getErrorExplanations return trailingDotCompletion explanations partialId caps ctx fun name explan textEdit? => { label := name.toString, detail? := "error name", diff --git a/src/Lean/Server/GoTo.lean b/src/Lean/Server/GoTo.lean index 0cf1840a1879..1846f16fc22f 100644 --- a/src/Lean/Server/GoTo.lean +++ b/src/Lean/Server/GoTo.lean @@ -194,7 +194,7 @@ where def locationLinksFromErrorNameInfo (eni : ErrorNameInfo) : GoToM (Array LeanLocationLink) := do let ctx ← read - let some explan := getErrorExplanationRaw? (← getEnv) eni.errorName + let some explan ← getErrorExplanation? eni.errorName | return #[] let some loc := explan.declLoc? | return #[]