feat: more ergonomic error explanation creation

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 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)

src/Lean/ErrorExplanation.lean

@@ -102,85 +102,71 @@ 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"

src/Lean/IdentifierSuggestion.lean

@@ -66,9 +66,9 @@ builtin_initialize identifierSuggestionsImpl : (PersistentEnvExtension (Name ×
       unless kind == AttributeKind.global do throwAttrMustBeGlobal `suggest_for kind
       let altSyntaxIds : Array Syntax ← match stx with
         | -- Attributes parsed _after_ the suggest_for notation is added
-          .node _ ``suggest_for #[.atom _ "suggest_for", .node _ `null ids] => pure ids
+          `(suggest_for| suggest_for $[$ids]*) => pure ids
         | -- Attributes parsed _before the suggest_for notation is added
-          .node _ ``Parser.Attr.simple #[.ident _ _ `suggest_for [], .node _ `null #[id]] => pure #[id]
+          `(Parser.Attr.simple| suggest_for $id:ident) => pure #[id]
         | _ => throwError "Invalid `[suggest_for]` attribute syntax {repr stx}"
       if isPrivateName decl then
         throwError "Cannot make suggestions for private names"

src/Lean/Parser/Command.lean

@@ -959,9 +959,25 @@ builtin_initialize
   register_parser_alias "optionValue" Command.optionValue
 
 /--
-Registers an error explanation.
+Registers an named error that can be referenced in `throwNamedError` commands. This will attach
+a link to an error explanation in reference documentation.
 
-Note that the error name is not relativized to the current namespace.
+The error name should have the form `domain.errorName`, and is not relativized to the current
+namespace.
+ and should have the form
+, where the `domain` is `lean` for .
+
+Example usage:
+
+```
+register_error_explanation lean.exampleError {
+  summary := "This sentence summarizes the error."
+  sinceVersion := "4.28.0"
+}
+```
+
+See https://github.com/leanprover/reference-manual/blob/main/Manual/ErrorExplanations/README.md for
+details of adding error explanations to the Lean reference manual.
 -/
 @[builtin_command_parser] def registerErrorExplanationStx := leading_parser
   optional docComment >> "register_error_explanation " >> ident >> termParser

stage0/src/stdlib_flags.h

@@ -1,5 +1,6 @@
 #include "util/options.h"
 
+// edit
 namespace lean {
 options get_default_options() {
     options opts;
@@ -25,4 +26,4 @@ options get_default_options() {
 #endif
     return opts;
 }
-}
+}