chore: use note and hint' for message addenda (#8980)

This PR improves the consistency of error message formatting by
rendering addenda of several existing error messages as labeled notes
and hints.

src/Lean/CoreM.lean

@@ -68,7 +68,7 @@ def useDiagnosticMsg : MessageData :=
     if diagnostics.get ctx.opts then
       pure ""
     else
-      pure s!"\n\nAdditional diagnostic information may be available using the `set_option {diagnostics.name} true` command."
+      pure <| .hint' s!"Additional diagnostic information may be available using the `set_option {diagnostics.name} true` command."
 
 /-- Name generator that creates user-accessible names. -/
 structure DeclNameGenerator where
@@ -457,8 +457,8 @@ def throwMaxHeartbeat (moduleName : Name) (optionName : Name) (max : Nat) : Core
   let includeModuleName := debug.moduleNameAtTimeout.get (← getOptions)
   let atModuleName := if includeModuleName then s!" at `{moduleName}`" else ""
   throw <| Exception.error (← getRef) <| .tagged `runtime.maxHeartbeats m!"\
-    (deterministic) timeout{atModuleName}, maximum number of heartbeats ({max/1000}) has been reached\n\
-    Use `set_option {optionName} <num>` to set the limit.\
+    (deterministic) timeout{atModuleName}, maximum number of heartbeats ({max/1000}) has been reached\
+    {.note m!"Use `set_option {optionName} <num>` to set the limit."}\
     {useDiagnosticMsg}"
 
 def checkMaxHeartbeatsCore (moduleName : String) (optionName : Name) (max : Nat) : CoreM Unit := do

src/Lean/Elab/Binders.lean

@@ -215,7 +215,7 @@ private partial def elabBinderViews (binderViews : Array BinderView) (fvars : Ar
       registerFailedToInferBinderTypeInfo type binderView.type
       if binderView.bi.isInstImplicit && checkBinderAnnotations.get (← getOptions) then
         unless (← isClass? type).isSome do
-          throwErrorAt binderView.type "invalid binder annotation, type is not a class instance{indentExpr type}\nuse the command `set_option checkBinderAnnotations false` to disable the check"
+          throwErrorAt binderView.type (m!"invalid binder annotation, type is not a class instance{indentExpr type}" ++ .note "Use the command `set_option checkBinderAnnotations false` to disable the check")
         withRef binderView.type <| checkLocalInstanceParameters type
       let id := binderView.id.getId
       let kind := kindOfBinderName id

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -514,21 +514,19 @@ where
           reduction got stuck at the '{.ofConstName ``Decidable}' instance{indentExpr reason}"
       let hint :=
         if reason.isAppOf ``Eq.rec then
-          m!"\n\n\
-          Hint: Reduction got stuck on '▸' ({.ofConstName ``Eq.rec}), \
-          which suggests that one of the '{.ofConstName ``Decidable}' instances is defined using tactics such as 'rw' or 'simp'. \
-          To avoid tactics, make use of functions such as \
-          '{.ofConstName ``inferInstanceAs}' or '{.ofConstName ``decidable_of_decidable_of_iff}' \
-          to alter a proposition."
+          .hint' m!"Reduction got stuck on '▸' ({.ofConstName ``Eq.rec}), \
+            which suggests that one of the '{.ofConstName ``Decidable}' instances is defined using tactics such as 'rw' or 'simp'. \
+            To avoid tactics, make use of functions such as \
+            '{.ofConstName ``inferInstanceAs}' or '{.ofConstName ``decidable_of_decidable_of_iff}' \
+            to alter a proposition."
         else if reason.isAppOf ``Classical.choice then
-          m!"\n\n\
-          Hint: Reduction got stuck on '{.ofConstName ``Classical.choice}', \
-          which indicates that a '{.ofConstName ``Decidable}' instance \
-          is defined using classical reasoning, proving an instance exists rather than giving a concrete construction. \
-          The '{tacticName}' tactic works by evaluating a decision procedure via reduction, \
-          and it cannot make progress with such instances. \
-          This can occur due to the 'opened scoped Classical' command, which enables the instance \
-          '{.ofConstName ``Classical.propDecidable}'."
+          .hint' m!"Reduction got stuck on '{.ofConstName ``Classical.choice}', \
+            which indicates that a '{.ofConstName ``Decidable}' instance \
+            is defined using classical reasoning, proving an instance exists rather than giving a concrete construction. \
+            The '{tacticName}' tactic works by evaluating a decision procedure via reduction, \
+            and it cannot make progress with such instances. \
+            This can occur due to the 'opened scoped Classical' command, which enables the instance \
+            '{.ofConstName ``Classical.propDecidable}'."
         else
           MessageData.nil
       return m!"\

src/Lean/Linter/Basic.lean

@@ -70,8 +70,8 @@ def getLinterValue (opt : Lean.Option Bool) (o : LinterOptions) : Bool :=
 
 def logLint [Monad m] [MonadLog m] [AddMessageContext m] [MonadOptions m]
     (linterOption : Lean.Option Bool) (stx : Syntax) (msg : MessageData) : m Unit :=
-  let disable := m!"note: this linter can be disabled with `set_option {linterOption.name} false`"
-  logWarningAt stx (.tagged linterOption.name m!"{msg}\n{disable}")
+  let disable := .note m!"This linter can be disabled with `set_option {linterOption.name} false`"
+  logWarningAt stx (.tagged linterOption.name m!"{msg}{disable}")
 
 /--
 If `linterOption` is enabled, print a linter warning message at the position determined by `stx`.

src/Lean/ReducibilityAttrs.lean

@@ -97,37 +97,37 @@ register_builtin_option allowUnsafeReducibility : Bool := {
 }
 
 private def validate (declName : Name) (status : ReducibilityStatus) (attrKind : AttributeKind) : CoreM Unit := do
-  let suffix := "use `set_option allowUnsafeReducibility true` to override reducibility status validation"
+  let suffix := .note "Use `set_option allowUnsafeReducibility true` to override reducibility status validation"
   unless allowUnsafeReducibility.get (← getOptions) do
     match (← getConstInfo declName) with
     | .defnInfo _ =>
       let statusOld := getReducibilityStatusCore (← getEnv) declName
       match attrKind with
       | .scoped =>
-        throwError "failed to set reducibility status for `{declName}`, the `scoped` modifier is not recommended for this kind of attribute\n{suffix}"
+        throwError "failed to set reducibility status for `{declName}`, the `scoped` modifier is not recommended for this kind of attribute{suffix}"
       | .global =>
         if (← getEnv).getModuleIdxFor? declName matches some _ then
-          throwError "failed to set reducibility status, `{declName}` has not been defined in this file, consider using the `local` modifier\n{suffix}"
+          throwError "failed to set reducibility status, `{declName}` has not been defined in this file, consider using the `local` modifier{suffix}"
         match status with
         | .reducible =>
           unless statusOld matches .semireducible do
-            throwError "failed to set `[reducible]`, `{declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`\n{suffix}"
+            throwError "failed to set `[reducible]`, `{declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}"
         | .irreducible =>
           unless statusOld matches .semireducible do
-            throwError "failed to set `[irreducible]`, `{declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`\n{suffix}"
+            throwError "failed to set `[irreducible]`, `{declName}` is not currently `[semireducible]`, but `{statusOld.toAttrString}`{suffix}"
         | .semireducible =>
-          throwError "failed to set `[semireducible]` for `{declName}`, declarations are `[semireducible]` by default\n{suffix}"
+          throwError "failed to set `[semireducible]` for `{declName}`, declarations are `[semireducible]` by default{suffix}"
       | .local =>
         match status with
         | .reducible =>
-          throwError "failed to set `[local reducible]` for `{declName}`, recall that `[reducible]` affects the term indexing datastructures used by `simp` and type class resolution\n{suffix}"
+          throwError "failed to set `[local reducible]` for `{declName}`, recall that `[reducible]` affects the term indexing datastructures used by `simp` and type class resolution{suffix}"
         | .irreducible =>
           unless statusOld matches .semireducible do
-            throwError "failed to set `[local irreducible]`, `{declName}` is currently `{statusOld.toAttrString}`, `[semireducible]` expected\n{suffix}"
+            throwError "failed to set `[local irreducible]`, `{declName}` is currently `{statusOld.toAttrString}`, `[semireducible]` expected{suffix}"
         | .semireducible =>
           unless statusOld matches .irreducible do
-            throwError "failed to set `[local semireducible]`, `{declName}` is currently `{statusOld.toAttrString}`, `[irreducible]` expected\n{suffix}"
-    | _ => throwError "failed to set reducibility status, `{declName}` is not a definition\n{suffix}"
+            throwError "failed to set `[local semireducible]`, `{declName}` is currently `{statusOld.toAttrString}`, `[irreducible]` expected{suffix}"
+    | _ => throwError "failed to set reducibility status, `{declName}` is not a definition{suffix}"
 
 private def addAttr (status : ReducibilityStatus) (declName : Name) (stx : Syntax) (attrKind : AttributeKind) : AttrM Unit := do
   Attribute.Builtin.ensureNoArgs stx

tests/lean/1007.lean.expected.out

@@ -9,4 +9,4 @@
 1007.lean:56:64-56:78: error: failed to synthesize
   IsLin fun x => sum fun i => norm x
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/1102.lean.expected.out

@@ -1,4 +1,4 @@
 1102.lean:22:35-22:49: error: failed to synthesize
   DVR 1
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/2273.lean.expected.out

@@ -1,4 +1,4 @@
 2273.lean:9:8-9:14: error: failed to synthesize
   P 37
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/297.lean.expected.out

@@ -4,4 +4,4 @@ numerals are polymorphic in Lean, but the numeral `0` cannot be used in a contex
   Sort ?u
 due to the absence of the instance above
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/386.lean.expected.out

@@ -1,4 +1,4 @@
 386.lean:9:2-9:46: error: failed to synthesize
   Fintype ?m
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/448.lean.expected.out

@@ -1,4 +1,4 @@
 448.lean:21:2-23:20: error: failed to synthesize
   MonadExceptOf IO.Error M
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/attrCmd.lean.expected.out

@@ -1,4 +1,4 @@
 attrCmd.lean:6:0-6:6: error: failed to synthesize
   Pure M
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/calcErrors.lean.expected.out

@@ -13,7 +13,7 @@ calcErrors.lean:24:8-24:11: error: invalid 'calc' step, relation expected
 calcErrors.lean:31:8-31:13: error: invalid 'calc' step, failed to synthesize `Trans` instance
   Trans p p ?m
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 calcErrors.lean:40:7-40:12: error: invalid 'calc' step, left-hand side is
   γ : Sort u_1
 but previous right-hand side is

tests/lean/defInst.lean.expected.out

@@ -2,7 +2,7 @@
 defInst.lean:8:26-8:32: error: failed to synthesize
   BEq Foo
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 fun x y => sorry : (x y : Foo) → ?m x y
 [4, 5, 6]
 fun x y => x == y : Foo → Foo → Bool

tests/lean/defaultInstance.lean.expected.out

@@ -1,6 +1,6 @@
 defaultInstance.lean:20:20-20:23: error: failed to synthesize
   Foo Bool (?m x)
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 defaultInstance.lean:22:35-22:38: error: typeclass instance problem is stuck, it is often due to metavariables
   Foo Bool (?m x)

tests/lean/eagerUnfoldingIssue.lean.expected.out

@@ -1,8 +1,8 @@
 eagerUnfoldingIssue.lean:6:2-6:17: error: failed to synthesize
   MonadLog (StateM Nat)
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 eagerUnfoldingIssue.lean:12:2-12:17: error: failed to synthesize
   MonadLog (StateM Nat)
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/eraseInsts.lean.expected.out

@@ -1,4 +1,4 @@
 eraseInsts.lean:12:22-12:27: error: failed to synthesize
   HAdd Foo Foo ?m
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/forErrors.lean.expected.out

@@ -1,4 +1,4 @@
 forErrors.lean:3:29-3:30: error: failed to synthesize
   ToStream α ?m
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/interactive/4880.lean.expected.out

@@ -17,7 +17,7 @@
    {"start": {"line": 16, "character": 12},
     "end": {"line": 17, "character": 0}},
    "message":
-   "failed to synthesize\n  A\n\nAdditional diagnostic information may be available using the `set_option diagnostics true` command.",
+   "failed to synthesize\n  A\n\nHint: Additional diagnostic information may be available using the `set_option diagnostics true` command.",
    "fullRange":
    {"start": {"line": 16, "character": 12},
     "end": {"line": 20, "character": 0}}},
@@ -37,7 +37,7 @@
    {"start": {"line": 22, "character": 17},
     "end": {"line": 22, "character": 20}},
    "message":
-   "failed to synthesize\n  A\n\nAdditional diagnostic information may be available using the `set_option diagnostics true` command.",
+   "failed to synthesize\n  A\n\nHint: Additional diagnostic information may be available using the `set_option diagnostics true` command.",
    "fullRange":
    {"start": {"line": 22, "character": 17},
     "end": {"line": 22, "character": 20}}},

tests/lean/interactive/strInterpSynthError.lean.expected.out

@@ -7,7 +7,7 @@
    {"start": {"line": 15, "character": 25},
     "end": {"line": 15, "character": 28}},
    "message":
-   "failed to synthesize\n  ToString Bar\n\nAdditional diagnostic information may be available using the `set_option diagnostics true` command.",
+   "failed to synthesize\n  ToString Bar\n\nHint: Additional diagnostic information may be available using the `set_option diagnostics true` command.",
    "fullRange":
    {"start": {"line": 15, "character": 25},
     "end": {"line": 15, "character": 28}}},
@@ -17,7 +17,7 @@
    {"start": {"line": 20, "character": 15},
     "end": {"line": 20, "character": 18}},
    "message":
-   "failed to synthesize\n  ToString Bar\n\nAdditional diagnostic information may be available using the `set_option diagnostics true` command.",
+   "failed to synthesize\n  ToString Bar\n\nHint: Additional diagnostic information may be available using the `set_option diagnostics true` command.",
    "fullRange":
    {"start": {"line": 20, "character": 15},
     "end": {"line": 20, "character": 18}}},
@@ -27,7 +27,7 @@
    {"start": {"line": 26, "character": 17},
     "end": {"line": 26, "character": 20}},
    "message":
-   "failed to synthesize\n  ToString Bar\n\nAdditional diagnostic information may be available using the `set_option diagnostics true` command.",
+   "failed to synthesize\n  ToString Bar\n\nHint: Additional diagnostic information may be available using the `set_option diagnostics true` command.",
    "fullRange":
    {"start": {"line": 26, "character": 17},
     "end": {"line": 26, "character": 20}}}]}

tests/lean/invalidInstImplicit.lean.expected.out

@@ -1,3 +1,4 @@
 invalidInstImplicit.lean:1:9-1:12: error: invalid binder annotation, type is not a class instance
   Nat
-use the command `set_option checkBinderAnnotations false` to disable the check
+
+Note: Use the command `set_option checkBinderAnnotations false` to disable the check

tests/lean/kernelMVarBug.lean.expected.out

@@ -1,4 +1,4 @@
 kernelMVarBug.lean:5:15-5:20: error: failed to synthesize
   HAdd α α α
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/linterMissingDocs.lean.expected.out

@@ -1,74 +1,111 @@
 linterMissingDocs.lean:8:4-8:9: warning: missing doc string for public def noDoc
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:13:14-13:20: warning: missing doc string for public def noDoc2
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:17:4-17:10: warning: missing doc string for public def openIn
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:24:4-24:16: warning: missing doc string for public def setOptionIn1
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:39:4-39:11: warning: missing doc string for public def lintDoc
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:41:10-41:13: warning: missing doc string for public inductive Ind
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:42:4-42:8: warning: missing doc string for public constructor Ind.ind1
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:43:4-43:8: warning: missing doc string for public constructor Ind.ind2
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:46:20-46:25: warning: missing doc string for computed field Ind.field
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:49:10-49:13: warning: missing doc string for public structure Foo
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:50:2-50:5: warning: missing doc string for public field Foo.mk1
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:53:3-53:6: warning: missing doc string for public field Foo.mk4
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:53:7-53:10: warning: missing doc string for public field Foo.mk5
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:54:3-54:6: warning: missing doc string for public field Foo.mk6
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:54:7-54:10: warning: missing doc string for public field Foo.mk7
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:56:6-56:9: warning: missing doc string for public structure Bar
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:57:3-57:6: warning: missing doc string for public field Bar.foo
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:57:7-57:10: warning: missing doc string for public field Bar.bar
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:59:6-59:10: warning: missing doc string for public structure Bar2
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:60:2-60:5: warning: missing doc string for public field Bar2.bar
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:62:6-62:10: warning: missing doc string for public structure Bar3
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:64:7-64:10: warning: missing doc string for public field Bar3.baz
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:70:11-70:15: warning: missing doc string for initializer init
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:73:19-73:24: warning: missing doc string for syntax category myCat
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:75:0-75:6: warning: missing doc string for syntax
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:76:16-76:24: warning: missing doc string for syntax namedSyn
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:77:0-77:6: warning: missing doc string for infixl
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:78:19-78:29: warning: missing doc string for infixr namedInfix
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:79:0-79:8: warning: missing doc string for notation
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:80:21-80:30: warning: missing doc string for notation namedNota
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:87:0-87:4: warning: missing doc string for elab
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:88:0-88:5: warning: missing doc string for macro
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:90:13-90:22: warning: missing doc string for class abbrev [anonymous]
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:92:16-92:24: warning: missing doc string for option myOption
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:94:14-94:19: warning: missing doc string for elab myCmd
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:100:4-100:15: warning: missing doc string for public def handleMyCmd
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`
 linterMissingDocs.lean:107:11-107:12: warning: missing doc string for my_command z
-note: this linter can be disabled with `set_option linter.missingDocs false`
+
+Note: This linter can be disabled with `set_option linter.missingDocs false`

tests/lean/linterSuspiciousUnexpanderPatterns.lean.expected.out

@@ -1,4 +1,6 @@
 linterSuspiciousUnexpanderPatterns.lean:6:6-6:14: warning: Unexpanders should match the function name against an antiquotation `$_` so as to be independent of the specific pretty printing of the name.
-note: this linter can be disabled with `set_option linter.suspiciousUnexpanderPatterns false`
+
+Note: This linter can be disabled with `set_option linter.suspiciousUnexpanderPatterns false`
 linterSuspiciousUnexpanderPatterns.lean:11:6-11:15: warning: Unexpanders should match the function name against an antiquotation `$_` so as to be independent of the specific pretty printing of the name.
-note: this linter can be disabled with `set_option linter.suspiciousUnexpanderPatterns false`
+
+Note: This linter can be disabled with `set_option linter.suspiciousUnexpanderPatterns false`

tests/lean/linterUnusedVariables.lean.expected.out

@@ -1,57 +1,84 @@
 linterUnusedVariables.lean:17:21-17:22: warning: unused variable `x`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:18:6-18:7: warning: unused variable `y`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:23:8-23:9: warning: unused variable `x`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:39:5-39:6: warning: unused variable `x`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:44:5-44:6: warning: unused variable `x`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:47:7-47:8: warning: unused variable `x`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:50:8-50:9: warning: unused variable `x`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:54:9-54:10: warning: unused variable `z`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:56:11-56:12: warning: unused variable `z`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:61:14-61:15: warning: unused variable `y`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:67:20-67:21: warning: unused variable `y`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:72:34-72:38: warning: unused variable `inst`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:113:25-113:26: warning: unused variable `x`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:114:6-114:7: warning: unused variable `y`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:120:6-120:7: warning: unused variable `a`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:130:26-130:27: warning: unused variable `z`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:139:9-139:10: warning: unused variable `h`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:153:8-153:9: warning: unused variable `y`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:156:20-156:21: warning: unused variable `β`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:157:7-157:8: warning: unused variable `x`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:167:6-167:7: warning: unused variable `s`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:191:6-191:7: warning: unused variable `y`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:201:19-201:20: warning: unused variable `x`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:205:6-205:7: warning: unused variable `y`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:210:6-210:7: warning: unused variable `y`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:215:6-215:7: warning: unused variable `y`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:226:32-226:33: warning: unused variable `b`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 linterUnusedVariables.lean:244:27-244:28: error: don't know how to synthesize placeholder
 context:
 a : Nat
@@ -68,4 +95,5 @@ a : Nat
 linterUnusedVariables.lean:248:0-248:40: error: type of theorem 'async' is not a proposition
   Nat → Nat
 linterUnusedVariables.lean:283:41-283:43: warning: unused variable `ha`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`

tests/lean/macroStack.lean.expected.out

@@ -12,7 +12,7 @@ macroStack.lean:11:9-11:15: error: invalid use of `(<- ...)`, must be nested ins
 macroStack.lean:17:0-17:6: error: failed to synthesize
   HAdd Nat String ?m
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 with resulting expansion
   binop% HAdd.hAdd✝ (x + x✝) x✝¹
 while expanding

tests/lean/macroSwizzle.lean.expected.out

@@ -1,7 +1,7 @@
 macroSwizzle.lean:4:7-4:23: error: failed to synthesize
   HAdd Bool String ?m
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 macroSwizzle.lean:6:7-6:10: error: Application type mismatch: In the application
   Nat.succ "x"
 the argument

tests/lean/openScoped.lean.expected.out

@@ -2,7 +2,7 @@ openScoped.lean:1:7-1:14: error: unknown identifier 'epsilon'
 openScoped.lean:4:2-4:24: error: failed to synthesize
   Decidable (f = g)
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 Classical.epsilon.{u} {α : Sort u} [h : Nonempty α] (p : α → Prop) : α
 openScoped.lean:15:7-15:14: error: unknown identifier 'epsilon'
 openScoped.lean:20:7-20:14: error: unknown identifier 'epsilon'

tests/lean/run/1163.lean

@@ -17,7 +17,7 @@ numerals are polymorphic in Lean, but the numeral `0` cannot be used in a contex
   Bool
 due to the absence of the instance above
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 def x : Bool := 0
@@ -31,7 +31,7 @@ numerals are polymorphic in Lean, but the numeral `0` cannot be used in a contex
   Bool
 due to the absence of the instance above
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 theorem result4 : False := by -- Does not generate a `sorry` warning because there is an error

tests/lean/run/345.lean

@@ -7,7 +7,7 @@ numerals are polymorphic in Lean, but the numeral `1` cannot be used in a contex
   Sort _
 due to the absence of the instance above
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 axiom bla : 1
@@ -19,7 +19,7 @@ numerals are polymorphic in Lean, but the numeral `1` cannot be used in a contex
   Sort _
 due to the absence of the instance above
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 ---
 warning: declaration uses 'sorry'
 -/
@@ -34,7 +34,7 @@ numerals are polymorphic in Lean, but the numeral `1` cannot be used in a contex
   Sort _
 due to the absence of the instance above
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 inductive Bla (x : 1) : Type

tests/lean/run/3554.lean

@@ -5,9 +5,10 @@ def foo : Nat → Nat
 set_option debug.moduleNameAtTimeout false
 /--
 error: (deterministic) timeout, maximum number of heartbeats (100) has been reached
-Use `set_option maxHeartbeats <num>` to set the limit.
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Note: Use `set_option maxHeartbeats <num>` to set the limit.
+
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 set_option maxHeartbeats 100 in

tests/lean/run/3996.lean

@@ -18,7 +18,7 @@ instance instB10000 : B 10000 where
 error: failed to synthesize
   A
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 #synth A -- should fail quickly

tests/lean/run/4203.lean

@@ -15,7 +15,7 @@ def IsGood [DecidableEq dOut] [DecidableEq dOut₂] (Λ : Mappish dIn dOut) (Λ
 error: failed to synthesize
   Fintype v
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 def MappishOrder [DecidableEq dIn] : Preorder

tests/lean/run/4365.lean

@@ -38,7 +38,7 @@ numerals are polymorphic in Lean, but the numeral `1` cannot be used in a contex
   String
 due to the absence of the instance above
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 #check (1 : String)
@@ -50,7 +50,7 @@ numerals are polymorphic in Lean, but the numeral `1` cannot be used in a contex
   Bool
 due to the absence of the instance above
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 #check (1 : Bool)
@@ -62,7 +62,7 @@ numerals are polymorphic in Lean, but the numeral `1` cannot be used in a contex
   Bool → Nat
 due to the absence of the instance above
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 #check (1 : Bool → Nat)
@@ -74,7 +74,7 @@ numerals are polymorphic in Lean, but the numeral `0` cannot be used in a contex
   String
 due to the absence of the instance above
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 def foo : String :=

tests/lean/run/5236.lean

@@ -6,7 +6,8 @@ set_option linter.deprecated true
 
 /--
 warning: 'inductive ... :=' has been deprecated in favor of 'inductive ... where'.
-note: this linter can be disabled with `set_option linter.deprecated false`
+
+Note: This linter can be disabled with `set_option linter.deprecated false`
 -/
 #guard_msgs in
 inductive DogSound' :=
@@ -15,7 +16,8 @@ inductive DogSound' :=
 
 /--
 warning: structure ... :=' has been deprecated in favor of 'structure ... where'.
-note: this linter can be disabled with `set_option linter.deprecated false`
+
+Note: This linter can be disabled with `set_option linter.deprecated false`
 -/
 #guard_msgs in
 structure S :=
@@ -23,7 +25,8 @@ structure S :=
 
 /--
 warning: class ... :=' has been deprecated in favor of 'class ... where'.
-note: this linter can be disabled with `set_option linter.deprecated false`
+
+Note: This linter can be disabled with `set_option linter.deprecated false`
 -/
 #guard_msgs in
 class C :=

tests/lean/run/5634.lean

@@ -102,7 +102,8 @@ def foo (n : α) := [n]
 
 /--
 warning: try 'simp at h' instead of 'simpa using h'
-note: this linter can be disabled with `set_option linter.unnecessarySimpa false`
+
+Note: This linter can be disabled with `set_option linter.unnecessarySimpa false`
 -/
 #guard_msgs in
 example (h : foo n ≠ [n]) : False := by

tests/lean/run/by_cases.lean

@@ -14,7 +14,7 @@ example (p : Prop) : True := by
 error: failed to synthesize
   Decidable p
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 example (p : Prop) : True := by

tests/lean/run/constructor_as_variable.lean

@@ -18,7 +18,8 @@ inductive A where
 
 /--
 warning: Local variable 'x' resembles constructor 'A.x' - write '.x' (with a dot) or 'A.x' to use the constructor.
-note: this linter can be disabled with `set_option linter.constructorNameAsVariable false`
+
+Note: This linter can be disabled with `set_option linter.constructorNameAsVariable false`
 -/
 #guard_msgs(drop error, warning) in
 def f : A → Unit
@@ -27,7 +28,8 @@ def f : A → Unit
 -- Show that the linter also works when there are no errors
 /--
 warning: Local variable 'x' resembles constructor 'A.x' - write '.x' (with a dot) or 'A.x' to use the constructor.
-note: this linter can be disabled with `set_option linter.constructorNameAsVariable false`
+
+Note: This linter can be disabled with `set_option linter.constructorNameAsVariable false`
 -/
 #guard_msgs(warning) in
 def g : A → Unit
@@ -47,10 +49,12 @@ def h : A → Unit
 -- Check that it works for let-bindings
 /--
 warning: Local variable 'x' resembles constructor 'A.x' - write '.x' (with a dot) or 'A.x' to use the constructor.
-note: this linter can be disabled with `set_option linter.constructorNameAsVariable false`
+
+Note: This linter can be disabled with `set_option linter.constructorNameAsVariable false`
 ---
 warning: Local variable 'y' resembles constructor 'A.y' - write '.y' (with a dot) or 'A.y' to use the constructor.
-note: this linter can be disabled with `set_option linter.constructorNameAsVariable false`
+
+Note: This linter can be disabled with `set_option linter.constructorNameAsVariable false`
 -/
 #guard_msgs in
 def i (a : A × A) : Unit :=
@@ -59,7 +63,8 @@ def i (a : A × A) : Unit :=
 
 /--
 warning: Local variable 'x' resembles constructor 'A.x' - write '.x' (with a dot) or 'A.x' to use the constructor.
-note: this linter can be disabled with `set_option linter.constructorNameAsVariable false`
+
+Note: This linter can be disabled with `set_option linter.constructorNameAsVariable false`
 -/
 #guard_msgs in
 def i' : Unit :=
@@ -69,7 +74,8 @@ def i' : Unit :=
 -- Check that it works in tactic proofs
 /--
 warning: Local variable 'x' resembles constructor 'A.x' - write '.x' (with a dot) or 'A.x' to use the constructor.
-note: this linter can be disabled with `set_option linter.constructorNameAsVariable false`
+
+Note: This linter can be disabled with `set_option linter.constructorNameAsVariable false`
 -/
 #guard_msgs in
 theorem j (a : A ⊕ A) : True := by
@@ -112,7 +118,8 @@ Hint: These are similar:
   'List.cons'
 ---
 warning: Local variable 'nil' resembles constructor 'List.nil' - write '.nil' (with a dot) or 'List.nil' to use the constructor.
-note: this linter can be disabled with `set_option linter.constructorNameAsVariable false`
+
+Note: This linter can be disabled with `set_option linter.constructorNameAsVariable false`
 -/
 #guard_msgs in
 def ctorSuggestion2 (list : List α) : Nat :=
@@ -141,7 +148,8 @@ Hint: These are similar:
   'StringList.cons'
 ---
 warning: Local variable 'nil' resembles constructor 'List.nil' - write '.nil' (with a dot) or 'List.nil' to use the constructor.
-note: this linter can be disabled with `set_option linter.constructorNameAsVariable false`
+
+Note: This linter can be disabled with `set_option linter.constructorNameAsVariable false`
 -/
 #guard_msgs in
 def ctorSuggestion3 (list : List α) : Nat :=

tests/lean/run/diagnosticsMsgOptional.lean

@@ -6,7 +6,7 @@
 error: failed to synthesize
   Coe Nat Int
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 #synth Coe Nat Int

tests/lean/run/ext.lean

@@ -40,7 +40,8 @@ example (f g : Nat × Nat → Nat) : f = g := by
 -- Check that we generate a warning if there are too many patterns.
 /--
 warning: `ext` did not consume the patterns: [j]
-note: this linter can be disabled with `set_option linter.unusedRCasesPattern false`
+
+Note: This linter can be disabled with `set_option linter.unusedRCasesPattern false`
 -/
 #guard_msgs in
 example (f g : Nat → Nat) (h : f = g) : f = g := by

tests/lean/run/extract_lets.lean

@@ -91,7 +91,8 @@ Too many names, linter warning.
 -/
 /--
 warning: unused name
-note: this linter can be disabled with `set_option linter.tactic.unusedName false`
+
+Note: This linter can be disabled with `set_option linter.tactic.unusedName false`
 ---
 trace: z : Nat := 2
 z' : Nat := 1 + 1

tests/lean/run/guard_msgs.lean

@@ -54,7 +54,7 @@ numerals are polymorphic in Lean, but the numeral `22` cannot be used in a conte
   α
 due to the absence of the instance above
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs(error) in
 example : α := 22
@@ -110,7 +110,8 @@ Lax whitespace
 /--
 error: failed to synthesize
   DecidableEq (Nat → Nat)
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs (whitespace := lax) in
 #synth DecidableEq (Nat → Nat)
@@ -118,7 +119,8 @@ Additional diagnostic information may be available using the `set_option diagnos
 /--
 error: failed to synthesize
   DecidableEq (Nat → Nat)
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs (whitespace := lax) in
 #synth DecidableEq (Nat → Nat)
@@ -153,7 +155,8 @@ set_option linter.unusedVariables true
 #guard_msgs in
 /--
 warning: unused variable `n`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 -/
 #guard_msgs in
 example (n : Nat) : True := trivial
@@ -161,7 +164,8 @@ example (n : Nat) : True := trivial
 #guard_msgs in
 /--
 warning: unused variable `n`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`
 -/
 #guard_msgs in
 #guard_msgs (info) in

tests/lean/run/index_variables_linter.lean

@@ -5,10 +5,12 @@ example (xs : List Nat) (i : Nat) (h) : xs[i] = xs[i] := rfl
 
 /--
 warning: Forbidden variable appearing as an index: use `i`, `j`, or `k`: m
-note: this linter can be disabled with `set_option linter.indexVariables false`
+
+Note: This linter can be disabled with `set_option linter.indexVariables false`
 ---
 warning: Forbidden variable appearing as an index: use `i`, `j`, or `k`: m
-note: this linter can be disabled with `set_option linter.indexVariables false`
+
+Note: This linter can be disabled with `set_option linter.indexVariables false`
 -/
 #guard_msgs in
 example (xs : List Nat) (m : Nat) (h) : xs[m] = xs[m] := rfl
@@ -24,10 +26,12 @@ example (xs : List Nat) (i : Nat) : xs[i]? = xs[i]? := rfl
 
 /--
 warning: Forbidden variable appearing as an index: use `i`, `j`, or `k`: m
-note: this linter can be disabled with `set_option linter.indexVariables false`
+
+Note: This linter can be disabled with `set_option linter.indexVariables false`
 ---
 warning: Forbidden variable appearing as an index: use `i`, `j`, or `k`: m
-note: this linter can be disabled with `set_option linter.indexVariables false`
+
+Note: This linter can be disabled with `set_option linter.indexVariables false`
 -/
 #guard_msgs in
 example (xs : List Nat) (m : Nat) : xs[m]? = xs[m]? := rfl
@@ -37,10 +41,12 @@ example (xs : List Nat) (i : Nat) : xs.take i = xs.take i := rfl
 
 /--
 warning: Forbidden variable appearing as an index: use `i`, `j`, or `k`: m
-note: this linter can be disabled with `set_option linter.indexVariables false`
+
+Note: This linter can be disabled with `set_option linter.indexVariables false`
 ---
 warning: Forbidden variable appearing as an index: use `i`, `j`, or `k`: m
-note: this linter can be disabled with `set_option linter.indexVariables false`
+
+Note: This linter can be disabled with `set_option linter.indexVariables false`
 -/
 #guard_msgs in
 example (xs : List Nat) (m : Nat) : xs.drop m = xs.drop m := rfl

tests/lean/run/isDefEqProjIssue.lean

@@ -52,9 +52,10 @@ where
 
 /--
 error: (deterministic) timeout at `whnf`, maximum number of heartbeats (400) has been reached
-Use `set_option maxHeartbeats <num>` to set the limit.
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Note: Use `set_option maxHeartbeats <num>` to set the limit.
+
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 set_option backward.isDefEq.lazyWhnfCore false in

tests/lean/run/list_variables_linter.lean

@@ -14,10 +14,12 @@ example (l₂ : List Nat) : l₂ = l₂ := rfl
 
 /--
 warning: Forbidden variable appearing as a `List` name: l₅
-note: this linter can be disabled with `set_option linter.listVariables false`
+
+Note: This linter can be disabled with `set_option linter.listVariables false`
 ---
 warning: Forbidden variable appearing as a `List` name: l₅
-note: this linter can be disabled with `set_option linter.listVariables false`
+
+Note: This linter can be disabled with `set_option linter.listVariables false`
 -/
 #guard_msgs in
 example (l₅ : List Nat) : l₅ = l₅ := rfl
@@ -27,20 +29,24 @@ example (xs : List Nat) : xs = xs := rfl
 
 /--
 warning: Forbidden variable appearing as a `List` name: ps
-note: this linter can be disabled with `set_option linter.listVariables false`
+
+Note: This linter can be disabled with `set_option linter.listVariables false`
 ---
 warning: Forbidden variable appearing as a `List` name: ps
-note: this linter can be disabled with `set_option linter.listVariables false`
+
+Note: This linter can be disabled with `set_option linter.listVariables false`
 -/
 #guard_msgs in
 example (ps : List Nat) : ps = ps := rfl
 
 /--
 warning: Forbidden variable appearing as a `Array` name: l
-note: this linter can be disabled with `set_option linter.listVariables false`
+
+Note: This linter can be disabled with `set_option linter.listVariables false`
 ---
 warning: Forbidden variable appearing as a `Array` name: l
-note: this linter can be disabled with `set_option linter.listVariables false`
+
+Note: This linter can be disabled with `set_option linter.listVariables false`
 -/
 #guard_msgs in
 example (l : Array Nat) : l = l := rfl

tests/lean/run/mergeSort.lean

@@ -35,7 +35,7 @@ error: could not synthesize default value for parameter 'le' using tactics
 error: failed to synthesize
   LE NoLE
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 example : mergeSort [NoLE.mk] = [NoLE.mk] := sorry

tests/lean/run/reducibilityAttrValidation.lean

@@ -2,7 +2,8 @@ def f (x : Nat) := x + 1
 
 /--
 error: failed to set `[semireducible]` for `f`, declarations are `[semireducible]` by default
-use `set_option allowUnsafeReducibility true` to override reducibility status validation
+
+Note: Use `set_option allowUnsafeReducibility true` to override reducibility status validation
 -/
 #guard_msgs in
 attribute [semireducible] f
@@ -11,7 +12,8 @@ attribute [reducible] f
 
 /--
 error: failed to set `[reducible]`, `f` is not currently `[semireducible]`, but `[reducible]`
-use `set_option allowUnsafeReducibility true` to override reducibility status validation
+
+Note: Use `set_option allowUnsafeReducibility true` to override reducibility status validation
 -/
 #guard_msgs in
 attribute [reducible] f -- should fail because of double reducible setting
@@ -24,7 +26,8 @@ attribute [irreducible] f
 
 /--
 error: failed to set `[irreducible]`, `f` is not currently `[semireducible]`, but `[irreducible]`
-use `set_option allowUnsafeReducibility true` to override reducibility status validation
+
+Note: Use `set_option allowUnsafeReducibility true` to override reducibility status validation
 -/
 #guard_msgs in
 attribute [irreducible] f
@@ -33,7 +36,8 @@ attribute [local semireducible] f
 
 /--
 error: failed to set `[local semireducible]`, `f` is currently `[semireducible]`, `[irreducible]` expected
-use `set_option allowUnsafeReducibility true` to override reducibility status validation
+
+Note: Use `set_option allowUnsafeReducibility true` to override reducibility status validation
 -/
 #guard_msgs in
 attribute [local semireducible] f
@@ -42,35 +46,40 @@ attribute [local irreducible] f
 
 /--
 error: failed to set `[local irreducible]`, `f` is currently `[irreducible]`, `[semireducible]` expected
-use `set_option allowUnsafeReducibility true` to override reducibility status validation
+
+Note: Use `set_option allowUnsafeReducibility true` to override reducibility status validation
 -/
 #guard_msgs in
 attribute [local irreducible] f
 
 /--
 error: failed to set `[local reducible]` for `f`, recall that `[reducible]` affects the term indexing datastructures used by `simp` and type class resolution
-use `set_option allowUnsafeReducibility true` to override reducibility status validation
+
+Note: Use `set_option allowUnsafeReducibility true` to override reducibility status validation
 -/
 #guard_msgs in
 attribute [local reducible] f
 
 /--
 error: failed to set reducibility status, `Nat.add` has not been defined in this file, consider using the `local` modifier
-use `set_option allowUnsafeReducibility true` to override reducibility status validation
+
+Note: Use `set_option allowUnsafeReducibility true` to override reducibility status validation
 -/
 #guard_msgs in
 attribute [semireducible] Nat.add
 
 /--
 error: failed to set reducibility status, `Nat.add` has not been defined in this file, consider using the `local` modifier
-use `set_option allowUnsafeReducibility true` to override reducibility status validation
+
+Note: Use `set_option allowUnsafeReducibility true` to override reducibility status validation
 -/
 #guard_msgs in
 attribute [reducible] Nat.add
 
 /--
 error: failed to set reducibility status, `Nat.add` has not been defined in this file, consider using the `local` modifier
-use `set_option allowUnsafeReducibility true` to override reducibility status validation
+
+Note: Use `set_option allowUnsafeReducibility true` to override reducibility status validation
 -/
 #guard_msgs in
 attribute [irreducible] Nat.add
@@ -82,7 +91,8 @@ attribute [scoped reducible] Nat.add
 namespace Foo
 /--
 error: failed to set reducibility status for `Nat.add`, the `scoped` modifier is not recommended for this kind of attribute
-use `set_option allowUnsafeReducibility true` to override reducibility status validation
+
+Note: Use `set_option allowUnsafeReducibility true` to override reducibility status validation
 -/
 #guard_msgs in
 attribute [scoped reducible] Nat.add

tests/lean/run/simpLoopProtection.lean

@@ -57,7 +57,8 @@ warning: Possibly looping simp theorem: `aa`
 Note: Possibly caused by: `id`
 
 Hint: You can disable a simp theorem from the default simp set by passing `- theoremName` to `simp`.
-note: this linter can be disabled with `set_option linter.loopingSimpArgs false`
+
+Note: This linter can be disabled with `set_option linter.loopingSimpArgs false`
 ---
 error: unsolved goals
 ⊢ b = 23

tests/lean/run/simpUnusedArgs.lean

@@ -13,7 +13,8 @@ warning: This simp argument is unused:
 
 Hint: Omit it from the simp argument list.
   simp ̵[̵i̵d̵_̵e̵q̵]̵
-note: this linter can be disabled with `set_option linter.unusedSimpArgs false`
+
+Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
 -/
 #guard_msgs in
 example : True := by simp [id_eq]
@@ -24,7 +25,8 @@ warning: This simp argument is unused:
 
 Hint: Omit it from the simp argument list.
   simp [i̵d̵_̵e̵q̵,̵ ̵and_self]
-note: this linter can be disabled with `set_option linter.unusedSimpArgs false`
+
+Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
 -/
 #guard_msgs in
 example : True ∧ True := by simp [id_eq, and_self]
@@ -38,7 +40,8 @@ warning: This simp argument is unused:
 
 Hint: Omit it from the simp argument list.
   simp ̵[̵s̵o̵m̵e̵_̵d̵e̵f̵]̵
-note: this linter can be disabled with `set_option linter.unusedSimpArgs false`
+
+Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
 -/
 #guard_msgs in example : True := by simp [some_def]
 
@@ -56,14 +59,16 @@ warning: This simp argument is unused:
 
 Hint: Omit it from the simp argument list.
   simp [some_def, some_def.eq_def,̵ ̵s̵o̵m̵e̵_̵d̵e̵f̵.̵e̵q̵_̵d̵e̵f̵]
-note: this linter can be disabled with `set_option linter.unusedSimpArgs false`
+
+Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
 ---
 warning: This simp argument is unused:
   some_def.eq_def
 
 Hint: Omit it from the simp argument list.
   simp [some_def, some_def.eq_def,̵ ̵s̵o̵m̵e̵_̵d̵e̵f̵.̵e̵q̵_̵d̵e̵f̵]
-note: this linter can be disabled with `set_option linter.unusedSimpArgs false`
+
+Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
 -/
 #guard_msgs in example : 0 < some_def := by simp [some_def, some_def.eq_def, some_def.eq_def]
 
@@ -73,14 +78,16 @@ warning: This simp argument is unused:
 
 Hint: Omit it from the simp argument list.
   simp [some_def, (̵s̵o̵m̵e̵_̵d̵e̵f̵.̵e̵q̵_̵d̵e̵f̵)̵,̵ ̵some_def.eq_def]
-note: this linter can be disabled with `set_option linter.unusedSimpArgs false`
+
+Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
 ---
 warning: This simp argument is unused:
   some_def.eq_def
 
 Hint: Omit it from the simp argument list.
   simp [some_def, (some_def.eq_def),̵ ̵s̵o̵m̵e̵_̵d̵e̵f̵.̵e̵q̵_̵d̵e̵f̵]
-note: this linter can be disabled with `set_option linter.unusedSimpArgs false`
+
+Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
 -/
 #guard_msgs in example : 0 < some_def := by simp [some_def, (some_def.eq_def), some_def.eq_def]
 
@@ -100,7 +107,8 @@ warning: This simp argument is unused:
 
 Hint: Omit it from the simp argument list.
   simp -failIfUnchanged ̵[̵s̵o̵m̵e̵_̵r̵d̵e̵f̵]̵
-note: this linter can be disabled with `set_option linter.unusedSimpArgs false`
+
+Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
 -/
 #guard_msgs in example : 0 < some_def := by simp -failIfUnchanged [some_rdef]
 
@@ -114,7 +122,8 @@ warning: This simp argument is unused:
 
 Hint: Omit it from the simp argument list.
   simp -failIfUnchanged [some_rdef,̵ ̵s̵o̵m̵e̵_̵r̵d̵e̵f̵.̵e̵q̵_̵d̵e̵f̵]
-note: this linter can be disabled with `set_option linter.unusedSimpArgs false`
+
+Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
 -/
 #guard_msgs in example : 0 < some_rdef 10 := by simp -failIfUnchanged [some_rdef, some_rdef.eq_def]
 
@@ -152,7 +161,8 @@ warning: This simp argument is unused:
 
 Hint: Omit it from the simp argument list.
   simp -failIfUnchanged ̵[̵_̵h̵]̵
-note: this linter can be disabled with `set_option linter.unusedSimpArgs false`
+
+Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
 -/
 #guard_msgs in example (a : Nat) (_h : a = 1) : True := by simp -failIfUnchanged [_h]
 
@@ -169,7 +179,8 @@ warning: This simp argument is unused:
 
 Hint: Omit it from the simp argument list.
   simp only [↓reduceI̵t̵e̵,̵ ̵↓̵r̵e̵d̵u̵c̵e̵DIte]
-note: this linter can be disabled with `set_option linter.unusedSimpArgs false`
+
+Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
 -/
 #guard_msgs in example : if _ : true then True else False := by simp only [↓reduceIte, ↓reduceDIte]
 
@@ -192,7 +203,8 @@ warning: This simp argument is unused:
 
 Hint: Omit it from the simp argument list.
   simp ̵[̵x̵]̵
-note: this linter can be disabled with `set_option linter.unusedSimpArgs false`
+
+Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
 -/
 #guard_msgs in example : let x := 1; True ∨ x > 0:= by intro x; left; simp [x]
 
@@ -205,7 +217,8 @@ warning: This simp argument is unused:
 
 Hint: Omit it from the simp argument list.
   simp [h1, h2,̵ ̵h̵3̵]
-note: this linter can be disabled with `set_option linter.unusedSimpArgs false`
+
+Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
 -/
 #guard_msgs in
 example (h1 : P) (h2 : Q) (h3 : R) : P ∧ (Q ∨ R) := by
@@ -217,14 +230,16 @@ warning: This simp argument is unused:
 
 Hint: Omit it from the simp argument list.
   simp [h1,̵ ̵h̵2̵]
-note: this linter can be disabled with `set_option linter.unusedSimpArgs false`
+
+Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
 ---
 warning: This simp argument is unused:
   h1
 
 Hint: Omit it from the simp argument list.
   simp [h1̵,̵ ̵h̵2]
-note: this linter can be disabled with `set_option linter.unusedSimpArgs false`
+
+Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
 -/
 #guard_msgs in
 example (h1 : P) (h2 : Q) : P ∧ Q := by
@@ -243,7 +258,8 @@ warning: This simp argument is unused:
 
 Hint: Omit it from the simp argument list.
   simp ̵[̵h̵]̵
-note: this linter can be disabled with `set_option linter.unusedSimpArgs false`
+
+Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
 -/
 #guard_msgs in
 example {P : Prop} (h : P) : True ∧ True := by constructor <;> simp [h]

tests/lean/run/varBinderUpdate.lean

@@ -126,7 +126,8 @@ variable (n : Nat)
 error: cannot update binder annotation of variable 'n' to instance implicit:
 invalid binder annotation, type is not a class instance
   Nat
-use the command `set_option checkBinderAnnotations false` to disable the check
+
+Note: Use the command `set_option checkBinderAnnotations false` to disable the check
 -/
 #guard_msgs in
 variable [n]

tests/lean/run/variable.lean

@@ -37,7 +37,8 @@ warning: automatically included section variable(s) unused in theorem 't6':
   [ToString α]
 consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
   omit [ToString α] in theorem ...
-note: this linter can be disabled with `set_option linter.unusedSectionVars false`
+
+Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
 -/
 #guard_msgs in
 theorem t6 (a : α) : a = a := rfl
@@ -56,7 +57,8 @@ warning: automatically included section variable(s) unused in theorem 'act_rel_o
   [IsTrans N r]
 consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
   omit [IsTrans N r] in theorem ...
-note: this linter can be disabled with `set_option linter.unusedSectionVars false`
+
+Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
 -/
 #guard_msgs in
 theorem act_rel_of_rel_of_act_rel (ab : r a b) : r a b := ab
@@ -79,7 +81,7 @@ variable [ToString α] [ToString β]
 error: failed to synthesize
   ToString α
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 omit [ToString α] in
@@ -90,7 +92,7 @@ theorem t8 (a : α) (b : β) : True :=
 error: failed to synthesize
   ToString β
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 omit [ToString β] in
@@ -101,12 +103,12 @@ theorem t9 (a : α) (b : β) : True :=
 error: failed to synthesize
   ToString α
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 ---
 error: failed to synthesize
   ToString β
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 -/
 #guard_msgs in
 omit [ToString _] in
@@ -164,7 +166,8 @@ warning: automatically included section variable(s) unused in theorem 't15':
   α
 consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
   omit α in theorem ...
-note: this linter can be disabled with `set_option linter.unusedSectionVars false`
+
+Note: This linter can be disabled with `set_option linter.unusedSectionVars false`
 -/
 #guard_msgs in
 variable (α : Type) in
@@ -178,7 +181,8 @@ theorem t15 : True := trivial
 set_option linter.omit true in
 /--
 warning: `omit` should be avoided in favor of restructuring your `variable` declarations
-note: this linter can be disabled with `set_option linter.omit false`
+
+Note: This linter can be disabled with `set_option linter.omit false`
 -/
 #guard_msgs in
 variable (α : Type) in

tests/lean/sanitychecks.lean.expected.out

@@ -10,7 +10,7 @@ sanitychecks.lean:7:7-7:31: error: 'unsafe' theorems are not allowed
 sanitychecks.lean:10:0-10:23: error: failed to synthesize
   Inhabited False
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 sanitychecks.lean:18:12-18:20: error: invalid use of 'partial', 'Foo.unsound3' is not a function
   False
 sanitychecks.lean:20:0-20:54: error: failed to compile 'partial' definition 'Foo.unsound4', could not prove that the type

tests/lean/scopedLocalInsts.lean.expected.out

@@ -1,15 +1,15 @@
 scopedLocalInsts.lean:12:6-12:39: error: failed to synthesize
   ToString A
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 "A.mk 10 20"
 scopedLocalInsts.lean:21:6-21:39: error: failed to synthesize
   ToString A
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 "{ x := 10, y := 20 }"
 scopedLocalInsts.lean:32:6-32:39: error: failed to synthesize
   ToString A
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 "A.mk 10 20"

tests/lean/semicolonOrLinebreak.lean.expected.out

@@ -11,4 +11,4 @@ Note: Expected a function because this term is being applied to the argument
 semicolonOrLinebreak.lean:20:2-20:9: error: failed to synthesize
   Singleton ?m Point
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/setLit.lean.expected.out

@@ -2,13 +2,13 @@ setLit.lean:22:19-22:21: error: overloaded, errors
   failed to synthesize
     EmptyCollection String
   
-  Additional diagnostic information may be available using the `set_option diagnostics true` command.
+  Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
   
   fields missing: 'data'
 setLit.lean:24:31-24:38: error: overloaded, errors 
   failed to synthesize
     Singleton Nat String
   
-  Additional diagnostic information may be available using the `set_option diagnostics true` command.
+  Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
   
   24:33 'val' is not a field of structure 'String'

tests/lean/tcloop.lean.expected.out

@@ -1,8 +1,9 @@
 tcloop.lean:14:2-14:15: error: failed to synthesize
   B Nat
 (deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached
-Use `set_option synthInstance.maxHeartbeats <num>` to set the limit.
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Note: Use `set_option synthInstance.maxHeartbeats <num>` to set the limit.
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
+
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.

tests/lean/typeOf.lean.expected.out

@@ -1,11 +1,11 @@
 typeOf.lean:11:22-11:25: error: failed to synthesize
   HAdd Nat Nat Bool
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 typeOf.lean:12:0-12:5: error: failed to synthesize
   HAdd Bool Nat Nat
 
-Additional diagnostic information may be available using the `set_option diagnostics true` command.
+Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
 typeOf.lean:20:56-20:62: error: invalid reassignment, term has type
   Bool : Type
 but is expected to have type

tests/lean/warningAsError.lean.expected.out

@@ -3,4 +3,5 @@ warningAsError.lean:8:6-8:7: warning: `g` has been deprecated: use `f` instead
 warningAsError.lean:12:6-12:7: error: `g` has been deprecated: use `f` instead
 1
 warningAsError.lean:15:7-15:13: error: unused variable `unused`
-note: this linter can be disabled with `set_option linter.unusedVariables false`
+
+Note: This linter can be disabled with `set_option linter.unusedVariables false`

tests/pkg/prv/Prv.lean

@@ -15,7 +15,7 @@ error: overloaded, errors ⏎
   failed to synthesize
     EmptyCollection (Name "hello")
   ⏎
-  Additional diagnostic information may be available using the `set_option diagnostics true` command.
+  Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
   ⏎
   invalid {...} notation, constructor for 'Name' is marked as private
 -/