leanprover · david-christiansen · Jun 30, 2025 · Jun 30, 2025 · Jun 30, 2025 · Jun 30, 2025
diff --git a/Manual/BasicTypes/Fin.lean b/Manual/BasicTypes/Fin.lean
@@ -102,7 +102,7 @@ numerals are polymorphic in Lean, but the numeral `0` cannot be used in a contex
   Fin 0
 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.
 ```
 
 ```lean (error := true) (name := finK)
@@ -115,7 +115,7 @@ numerals are polymorphic in Lean, but the numeral `0` cannot be used in a contex
   Fin k
 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.
 ```
 
 :::

diff --git a/Manual/BasicTypes/Sum.lean b/Manual/BasicTypes/Sum.lean
@@ -152,7 +152,7 @@ example : Nat ⊕ String := panic! "Cant' find it"
 failed to synthesize
   Inhabited (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.
 ```
 
 The desired instance can be made available to instance synthesis using {keywordOf Lean.Parser.Term.have}`have`:

diff --git a/Manual/BuildTools/Lake/Config.lean b/Manual/BuildTools/Lake/Config.lean
@@ -7,8 +7,8 @@ Author: David Thrane Christiansen
 import VersoManual
 
 import Lean.Parser.Command
-import Lake.DSL.Syntax
 import Lake.Config.Monad
+import Lake.DSL
 
 import Manual.Meta
 import Manual.BuildTools.Lake.CLI
@@ -179,7 +179,8 @@ name = "example-package"
       license := "",
       licenseFiles := #[FilePath.mk "LICENSE"],
       readmeFile := FilePath.mk "README.md",
-      reservoir := true},
+      reservoir := true,
+      enableArtifactCache := false},
   configFile := FilePath.mk "lakefile",
   relConfigFile := FilePath.mk "lakefile",
   relManifestFile := FilePath.mk "lake-manifest.json",
@@ -194,7 +195,8 @@ name = "example-package"
   postUpdateHooks := #[],
   buildArchive := ELIDED,
   testDriver := "",
-  lintDriver := ""}
+  lintDriver := "",
+  cacheRef? := none}
 ```
 ::::
 :::::
@@ -258,7 +260,8 @@ name = "Sorting"
       license := "",
       licenseFiles := #[FilePath.mk "LICENSE"],
       readmeFile := FilePath.mk "README.md",
-      reservoir := true},
+      reservoir := true,
+      enableArtifactCache := false},
   configFile := FilePath.mk "lakefile",
   relConfigFile := FilePath.mk "lakefile",
   relManifestFile := FilePath.mk "lake-manifest.json",
@@ -341,7 +344,8 @@ name = "Sorting"
   postUpdateHooks := #[],
   buildArchive := ELIDED,
   testDriver := "",
-  lintDriver := ""}
+  lintDriver := "",
+  cacheRef? := none}
 ```
 ::::
 :::::
@@ -796,13 +800,14 @@ from git $t $[@ $t]? $[/ $t]?
 
 ## Targets
 
-{tech}[Targets] are typically added to the set of default targets by applying the `default_target` attribute, rather than by explicitly listing them.
 
+
+{tech}[Targets] are typically added to the set of default targets by applying the `default_target` attribute, rather than by explicitly listing them.
 :::TODO
-It's presently impossible to import Lake.DSL.AttributesCore due to initialization changes, so `default_target` can't be rendered/checked as an attribute above. This should be fixed upstream.
+Fix `default_target` above - it's not working on CI, but it is working locally, with the `attr` role.
 :::
 
-:::syntax attr (title := "Specifying Default Targets") (label := "attribute")
+:::syntax attr (title := "Specifying Default Targets") (label := "attribute") (namespace := Lake.DSL)
 
 ```grammar
 default_target
@@ -1019,7 +1024,7 @@ Whitespace is not permitted between the name and `.*` or `.+`.
 
 
 
-{docstring Lake.LeanOption (allowMissing := true)}
+{docstring Lake.LeanOption}
 
 {docstring Lake.Backend}
 

diff --git a/Manual/Classes.lean b/Manual/Classes.lean
@@ -151,7 +151,8 @@ def f [n : Nat] : n = n := rfl
 ```leanOutput notClass
 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
 ```
 
 :::
@@ -369,7 +370,7 @@ However, {name}`plusTimes2` fails, because there is no {lean}`AddMul' Nat` insta
 failed to synthesize
   AddMul' ?m.22
 
-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.
 ```
 Declaring an very general instance takes care of the problem for {lean}`Nat` and every other type:
 ```lean (name := plusTimes2b)

diff --git a/Manual/Classes/BasicClasses.lean b/Manual/Classes/BasicClasses.lean
@@ -246,7 +246,7 @@ example (f g : Nat → Nat) : Decidable (f = g) := inferInstance
 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.
 ```
 
 Opening `Classical` makes every proposition decidable; however, declarations and examples that use this fact must be marked {keywordOf Lean.Parser.Command.declaration}`noncomputable` to indicate that code should not be generated for them.

diff --git a/Manual/Classes/InstanceDecls.lean b/Manual/Classes/InstanceDecls.lean
@@ -142,7 +142,7 @@ with errors in both the left and right recursive calls that read:
 failed to synthesize
   BEq NatTree
 
-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.
 ```
 Given a suitable recursive function, such as {lean}`NatTree.beq`:
 ```lean
@@ -187,7 +187,7 @@ def NatRoseTree.beq : (tree1 tree2 : NatRoseTree) → Bool
 failed to synthesize
   BEq (Array NatRoseTree)
 
-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.
 ```
 
 To solve this, a local {lean}`BEq NatRoseTree` instance may be `let`-bound:
@@ -265,7 +265,7 @@ instance : DecidableEq StringList
 failed to synthesize
   Decidable (t1 = t2)
 
-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.
 ```
 However, because it is an ordinary Lean function, it can recursively refer to its own explicitly-provided name:
 ```lean

diff --git a/Manual/Classes/InstanceSynth.lean b/Manual/Classes/InstanceSynth.lean
@@ -278,7 +278,7 @@ Because instance synthesis selects the most recently defined instance, the follo
 failed to synthesize
   OneSmaller (Option Bool) 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.
 ```
 The {lean}`OneSmaller (Option Bool) (Option Unit)` instance was selected during instance synthesis, without regard to the supplied value of `β`.
 :::

diff --git a/Manual/Coercions.lean b/Manual/Coercions.lean
@@ -101,7 +101,7 @@ end
 #check Int.bdiv
 
 /--
-error: invalid field 'bdiv', the environment does not contain 'Nat.bdiv'
+error: Invalid field `bdiv`: The environment does not contain `Nat.bdiv`
   n
 has type
   Nat
@@ -122,7 +122,7 @@ The coercion from {lean}`Nat` to {lean}`Int` is not considered when looking up t
 example (n : Nat) := n.bdiv 2
 ```
 ```leanOutput natBdiv
-invalid field 'bdiv', the environment does not contain 'Nat.bdiv'
+Invalid field `bdiv`: The environment does not contain `Nat.bdiv`
   n
 has type
   Nat
@@ -221,7 +221,7 @@ numerals are polymorphic in Lean, but the numeral `9` cannot be used in a contex
   Bin
 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.
 ```
 This is because coercions are inserted in response to mismatched types, but a failure to synthesize an {name}`OfNat` instance is not a type mismatch.
 

diff --git a/Manual/Defs.lean b/Manual/Defs.lean
@@ -418,8 +418,9 @@ def select (choices : α × α × α) : Asnwer →  α
 ```
 The resulting error message states that the argument's type is not a constant, so dot notation cannot be used in the pattern:
 ```leanOutput asnwer
-invalid dotted identifier notation, expected type is not of the form (... → C ...) where C is a constant
+Invalid dotted identifier notation: The expected type of `.yes`
   Asnwer
+is not of the form `C ...` or `... → C ...` where C is a constant
 ```
 This is because the signature is:
 ```signature

diff --git a/Manual/ErrorExplanations.lean b/Manual/ErrorExplanations.lean
@@ -14,6 +14,7 @@ namespace Manual
 set_option pp.rawOnError true
 set_option guard_msgs.diff true
 
+set_option manual.requireErrorExplanations false
 
 inline_extension Inline.errorExplanationLink (errorName : Name) where
   data := toJson errorName

diff --git a/Manual/Interaction.lean b/Manual/Interaction.lean
@@ -251,7 +251,7 @@ Attempting to add a string to a natural number fails, as expected:
 failed to synthesize
   HAdd String Nat ?m.32
 
-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.
 ```
 Nonetheless, a partially-elaborated term is available:
 ```leanOutput oneOne

diff --git a/Manual/Language/InductiveTypes.lean b/Manual/Language/InductiveTypes.lean
@@ -552,7 +552,9 @@ example : OddList String := .cons "x" (.cons "y" (.cons "z" .nil))
 example : OddList String := .cons "x" (.cons "y" .nil)
 ```
 ```leanOutput evenOddMut
-invalid dotted identifier notation, unknown identifier `OddList.nil` from expected type
+Unknown identifier `OddList.nil`
+
+Note: Inferred this identifier from the expected type of `.nil`:
   OddList String
 ```
 :::

diff --git a/Manual/Meta/ErrorExplanation.lean b/Manual/Meta/ErrorExplanation.lean
@@ -23,6 +23,11 @@ set_option guard_msgs.diff true
 
 namespace Manual
 
+register_option manual.requireErrorExplanations : Bool := {
+  defValue := true,
+  descr := "Whether to fail or warn when error explanations don't match. Must be `true` for releases."
+}
+
 /-- Loads the JSON data file for the preprocessed MWE code block `name`. -/
 def loadPreprocessedMWE (name : Name) (contents : String)
     : MetaM (Highlighted × Array (MessageSeverity × String)) := do
@@ -241,7 +246,10 @@ def tryElabErrorExplanationCodeBlock (errorName : Name) (errorSev : MessageSever
           let kindStr := kind?.map (s!" ({·} example)") |>.getD ""
           -- Log rather than throw so we can detect all invalid outputs in a
           -- single build
-          logErrorAt ref m!"Invalid output for {(← read).name} code block \
+          let logFailure :=
+            if manual.requireErrorExplanations.get (← getOptions) then logErrorAt
+            else logWarningAt
+          logFailure ref m!"Invalid output for {(← read).name} code block \
             #{codeBlockIdx}{kindStr}: {msg}"
           pure #[← ``(Verso.Doc.Block.code "<invalid output>")]
         | e@(.internal ..) => throw e

diff --git a/Manual/Meta/LakeToml.lean b/Manual/Meta/LakeToml.lean
@@ -632,13 +632,32 @@ instance : Test (Lake.ConfigType kind pkg name) where
     | .anonymous => fun (x : Lake.OpaqueTargetConfig pkg name) => Test.toString x
     | _ => fun _ => "Impossible!"
 
+instance : Test Lake.CacheRef where
+  toString _ := "#<cacheref>"
+
+private def contains (fmt : Format) (c : Char) : Bool :=
+  match fmt with
+  | .text s => s.contains c
+  | .tag _ x | .group x .. | .nest _ x => contains x c
+  | .append x y => contains x c || contains y c
+  | .align .. | .line | .nil => false
+
+instance [Test α] : Test (Option α) where
+  toString
+    | none => "none"
+    | some x =>
+      let s := Test.toString x
+      let s := if contains s '(' || contains s ' ' then "(" ++ s ++ ")" else s
+      s!"some " ++ s
 
 deriving instance Test for Lake.ConfigDecl
 deriving instance Test for Lake.PConfigDecl
 deriving instance Test for Lake.NConfigDecl
+
 deriving instance Test for Lake.Package
 
 
+
 open Lake Toml in
 def report [Monad m] [Lean.MonadLog m] [MonadFileMap m] [Test α] (val : α) (errs : Array DecodeError) : m String := do
     let mut result := ""

diff --git a/Manual/Monads/Lift.lean b/Manual/Monads/Lift.lean
@@ -250,7 +250,7 @@ def getBytes' (input : Array Nat) :
 failed to synthesize
   MonadStateOf (Array String) (Except 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.
 ```
 
 Because {name}`StateT` has a {name}`MonadControl` instance, {name}`control` can be used instead of {name}`liftM`.

diff --git a/Manual/Monads/Zoo.lean b/Manual/Monads/Zoo.lean
@@ -263,7 +263,7 @@ Only the outermost may be used, because the type of the state is an output param
 failed to synthesize
   MonadState 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.
 ```
 
 Providing the state type explicitly using {name}`getThe` from {name}`MonadStateOf` allows both states to be read.

diff --git a/Manual/Namespaces.lean b/Manual/Namespaces.lean
@@ -356,7 +356,8 @@ automatically included section variable(s) unused in theorem 'p_all':
   pFifteen
 consider restructuring your `variable` declarations so that the variables are not in scope or explicitly omit them:
   omit pFifteen 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`
 ```
 
 This can be avoided by using {keywordOf Lean.Parser.Command.omit}`omit`to remove {lean}`pFifteen`:

diff --git a/Manual/NotationsMacros/Elab.lean b/Manual/NotationsMacros/Elab.lean
@@ -261,7 +261,7 @@ numerals are polymorphic in Lean, but the numeral `5` cannot be used in a contex
   Int → Int
 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.
 ```
 
 :::

diff --git a/Manual/NotationsMacros/Operators.lean b/Manual/NotationsMacros/Operators.lean
@@ -196,7 +196,7 @@ However, because the new operator is not associative, the {tech}[local longest-m
 failed to synthesize
   HAdd Prop Prop ?m.38
 
-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.
 ```
 
 :::
@@ -223,7 +223,7 @@ numerals are polymorphic in Lean, but the numeral `2` cannot be used in a contex
   Prop
 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.
 ```
 
 The new operator is not associative, so the {tech}[local longest-match rule] means that only {name}`HAdd.hAdd` applies to the three-argument version:
@@ -234,7 +234,7 @@ The new operator is not associative, so the {tech}[local longest-match rule] mea
 failed to synthesize
   HAdd Prop Prop ?m.20
 
-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.
 ```
 :::
 

diff --git a/Manual/RecursiveDefs.lean b/Manual/RecursiveDefs.lean
@@ -440,7 +440,7 @@ However, {lean}`Clause` is semireducible, so the {inst}`ToString String` instanc
 failed to synthesize
   ToString Clause
 
-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.
 ```
 
 The instance can be explicitly enabled by creating a {lean}`ToString Clause` instance that reduces to the {lean}`ToString String` instance.
@@ -471,7 +471,7 @@ attribute [irreducible] Sequence
 #check let xs : Sequence Nat := .ofList [1,2,3]; xs.reverse
 ```
 ```leanOutput irredSeq
-invalid field 'reverse', the environment does not contain 'Sequence.reverse'
+Invalid field `reverse`: The environment does not contain `Sequence.reverse`
   xs
 has type
   Sequence Nat