diff --git a/Manual/BasicTypes/Fin.lean b/Manual/BasicTypes/Fin.lean
index 3c50e3e5..469c9b87 100644
--- 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
index 7daaac20..99a655d3 100644
--- 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
index 85c7e2c5..61941cfd 100644
--- 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
index 532e0406..094ecf87 100644
--- 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
index 38119ad6..735a5d16 100644
--- 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
index 78886132..20f31659 100644
--- 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
index 6461ff84..c0ddcdd2 100644
--- 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
index d8ada64f..d16d84bf 100644
--- 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
index b84dd5ac..c8678118 100644
--- 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
index b0cc94a7..259fb301 100644
--- 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
index 7cf4c5ce..7a81a475 100644
--- 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
index 2cf85001..80e83541 100644
--- 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
index c890b675..911def5f 100644
--- 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
index 01a85263..6c10fa1b 100644
--- 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
index 7020973a..5e1f44b3 100644
--- 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
index 7566db06..0c4cb646 100644
--- 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
index 8ca5fc30..4612d9c3 100644
--- 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
index 334d0353..b9b788dc 100644
--- 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
index 50ae19df..9159f7fb 100644
--- 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
index da66326b..79309f0d 100644
--- 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
diff --git a/Manual/SourceFiles.lean b/Manual/SourceFiles.lean
index bf50575b..0476ae14 100644
--- a/Manual/SourceFiles.lean
+++ b/Manual/SourceFiles.lean
@@ -94,7 +94,7 @@ tag := "keywords-and-identifiers"
 An {tech}[identifier] consists of one or more identifier components, separated by `'.'`.{index}[identifier]
 
 {deftech}[Identifier components] consist of a letter or letter-like character or an underscore (`'_'`), followed by zero or more identifier continuation characters.
-Letters are English letters, upper- or lowercase, and the letter-like characters include a range of non-English alphabetic scripts, including the Greek script which is widely used in Lean, as well as the members of the Unicode letter-like symbol block, which contains a number of double-struck characters (including `ℕ` and `ℤ`) and abbreviations.
+Letters are English letters, upper- or lowercase, and the letter-like characters include a range of non-English alphabetic scripts, including the Greek script which is widely used in Lean, the Coptic script, the members of the Unicode letter-like symbol block, which contains a number of double-struck characters (including `ℕ` and `ℤ`) and abbreviations, the Latin-1 supplemental letters (with the exception of `×` and `÷`), and the Latin Extended-A block.
 Identifier continuation characters consist of letters, letter-like characters, underscores (`'_'`), exclamation marks (`!`), question marks (`?`), subscripts, and single quotes (`'`).
 As an exception, underscore alone is not a valid identifier.
 
@@ -130,29 +130,31 @@ def validIdentifier (str : String) : IO String :=
 #check_msgs in
 #eval validIdentifier "αποδεικνύοντας"
 
-
-/- Here's some things that probably should be identifiers but aren't at the time of writing -/
-
 /-- info: "Success! Final stack:\n  `κύκ\nRemaining:\n\"λος\"" -/
 #check_msgs in
 #eval validIdentifier "κύκλος"
 
-/-- info: "Failure @0 (⟨1, 0⟩): expected token\nFinal stack:\n  <missing>\nRemaining: \"øvelse\"" -/
+/-- info: "Success! Final stack:\n  `øvelse\nAll input consumed." -/
 #check_msgs in
 #eval validIdentifier "øvelse"
 
-/--
-info: "Failure @0 (⟨1, 0⟩): expected token\nFinal stack:\n  <missing>\nRemaining: \"Übersetzung\""
--/
+/-- info: "Success! Final stack:\n  `Übersetzung\nAll input consumed." -/
 #check_msgs in
 #eval validIdentifier "Übersetzung"
 
+/- Here's some things that probably should be identifiers but aren't at the time of writing -/
+
 /--
 info: "Failure @0 (⟨1, 0⟩): expected token\nFinal stack:\n  <missing>\nRemaining: \"переклад\""
 -/
 #check_msgs in
 #eval validIdentifier "переклад"
 
+/-- info: "Failure @0 (⟨1, 0⟩): expected token\nFinal stack:\n  <missing>\nRemaining: \"汉语\"" -/
+#check_msgs in
+#eval validIdentifier "汉语"
+
+
 ```
 
 Identifiers components may also be surrounded by double {deftech}[guillemets] (`'«'` and `'»'`).
diff --git a/Manual/Terms.lean b/Manual/Terms.lean
index 5aaf6fc3..03e2d343 100644
--- a/Manual/Terms.lean
+++ b/Manual/Terms.lean
@@ -202,7 +202,9 @@ open B
 #eval x
 ```
 ```leanOutput ambi (whitespace := lax)
-ambiguous, possible interpretations
+Ambiguous term
+  x
+Possible interpretations:
   B.x : String
 
   A.x : String
@@ -753,7 +755,7 @@ However, {lean}`Username.validate` can't be called on {lean}`"root"` using field
 #eval "root".validate
 ```
 ```leanOutput notString
-invalid field 'validate', the environment does not contain 'String.validate'
+Invalid field `validate`: The environment does not contain `String.validate`
   "root"
 has type
   String
@@ -884,7 +886,7 @@ numerals are polymorphic in Lean, but the numeral `4` cannot be used in a contex
   Array ?m.4
 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.
 ```
 
 Using pipeline field notation causes the array to be inserted at the first type-correct position:
diff --git a/lean-toolchain b/lean-toolchain
index efadbdc1..8c78ff9c 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2025-06-26
+leanprover/lean4:nightly-2025-06-29