chore: bump to nightly-2026-04-15 (#831)

Author: david-christiansen

Manual/BuildTools/Lake/CLI.lean

@@ -1114,9 +1114,9 @@ USAGE:
 
 COMMANDS:
   get [<mappings>]      download build outputs into the local Lake cache
-  put <mappings>        upload build ouptuts to a remote cache
+  put <mappings>        upload build outputs to a remote cache
   add <mappings>        add input-to-output mappings to the Lake cache
-  clean                 removes ALL froms the local Lake cache
+  clean                 removes ALL from the local Lake cache
   services              print configured remote cache services
 
 STAGING COMMANDS:
@@ -1174,7 +1174,7 @@ will search the repository's entire history (or as far as Git will allow).
 
 By default, Lake will download both the input-to-output mappings and the
 output artifacts for a package. By using `--mappings-onlys`, Lake will only
-download the mappings abd delay downloading artifacts until they are needed.
+download the mappings and delay downloading artifacts until they are needed.
 
 If a download for an artifact fails or the download process for a whole
 package fails, Lake will report this and continue on to the next. Once done,
@@ -1297,7 +1297,7 @@ OPTIONS:
   --scope=<remote-scope>          the prefix of artifacts within the service
   --repo=<github-repo>            for Reservoir, a GitHub repository scope
 
-Reads a list of input-to-output mapppings from the provided file and adds
+Reads a list of input-to-output mappings from the provided file and adds
 them to the local Lake cache. If `--service` is provided, the output artifacts
 can then be fetched lazily from that service during a Lake build. The service
 must either be `reservoir` or  be configured through the Lake system
@@ -1433,9 +1433,9 @@ USAGE:
 
 COMMANDS:
   get [<mappings>]      download build outputs into the local Lake cache
-  put <mappings>        upload build ouptuts to a remote cache
+  put <mappings>        upload build outputs to a remote cache
   add <mappings>        add input-to-output mappings to the Lake cache
-  clean                 removes ALL froms the local Lake cache
+  clean                 removes ALL from the local Lake cache
   services              print configured remote cache services
 
 STAGING COMMANDS:

Manual/Classes/InstanceSynth.lean

@@ -95,7 +95,7 @@ Clicking a `▶` symbol expands that branch of the trace, and clicking the `▼`
 
 ```lean -show
 -- Hide Lake details that are intruding here
-attribute [-instance] Lake.inhabitedOfNilTrace
+attribute [-instance] Lake.inhabitedOfNilTrace Lake.inhabitedOfMonadCycle
 ```
 
 ```lean (name := trace)
@@ -156,7 +156,7 @@ In the example above, Lean follows these steps:
   - The {name}`Sum.nonemptyLeft` instance, which would create a sub-goal {lean}`Nonempty Nat`.
   - The {name}`instNonemptyOfMonad` instance, which would create two sub-goals {lean}`Monad (Sum Nat)` and {lean}`Nonempty Nat`.
   - The {name}`instNonemptyOfInhabited` instance, which would create a sub-goal {lean}`Inhabited (Sum Nat Empty)`.
-* It applies {name}`Sum.nonemptyRight`, which succeeds, leaving an new goal: {lean}`Nonempty Empty`.
+* It applies {name}`Sum.nonemptyRight`, which succeeds, leaving a new goal: {lean}`Nonempty Empty`.
 * The first sub-goal, {lean}`Nonempty Empty`, is considered. Lean sees two ways of possibly satisfying this goal:
   - The {name}`instNonemptyOfMonad` instance, which is rejected.
     It can't be used because the type {lean}`Empty` is not the application of a monad to a type.

Manual/Elaboration.lean

@@ -250,7 +250,7 @@ info: third_of_five.eq_def.{u_1} {α : Type u_1} (x✝ : List α) :
 #check third_of_five.eq_def
 
 /--
-info: def third_of_five.match_1.{u_1, u_2} : {α : Type u_1} →
+info: @[implicit_reducible] def third_of_five.match_1.{u_1, u_2} : {α : Type u_1} →
   (motive : List α → Sort u_2) →
     (x : List α) →
       ((head head_1 x head_2 head_3 : α) → motive [head, head_1, x, head_2, head_3]) →

Manual/Language/InductiveTypes/Structures.lean

@@ -285,10 +285,10 @@ structure AugmentedIntList where
   augmentation : String := ""
 ```
 
-When testing whether the list is empty, the function {name AugmentedIntList.isEmpty}`isEmpty` is also testing whether the {name AugmentedIntList.augmentation}`augmentation` field is empty, because the omitted field's default value is also used in pattern contexts:
+When testing whether the list is empty, the function {name AugmentedIntList.isEmpty}`isEmpty` must explicitly match the {name AugmentedIntList.augmentation}`augmentation` field, even though it has a default value:
 ```lean (name := isEmptyDefaults)
 def AugmentedIntList.isEmpty : AugmentedIntList → Bool
-  | {list := []} => true
+  | {list := [], augmentation := ""} => true
   | _ => false
 
 #eval {list := [], augmentation := "extra" : AugmentedIntList}.isEmpty

Manual/Meta/LakeToml.lean

@@ -828,6 +828,8 @@ def checkTomlPackage [Lean.MonadError m] (str : String) : m (Except String Strin
         baseName := name
         wsIdx := 0
         origName := name
+        keyName := name
+        relManifestFile := Lake.defaultManifestFile
       }
 
     .ok <$> report pkg errs

Manual/RecursiveDefs/Structural.lean

@@ -606,7 +606,7 @@ The auxiliary match function's definition is:
 #print half.match_1
 ```
 ```leanOutput halfmatch (whitespace := lax)
-def half.match_1.{u_1} :
+@[implicit_reducible] def half.match_1.{u_1} :
     (motive : Nat → Sort u_1) → (x : Nat) →
     (Unit → motive Nat.zero) → (Unit → motive 1) →
     ((n : Nat) → motive n.succ.succ) →

Manual/Terms.lean

@@ -1341,8 +1341,8 @@ instance : OfNat Blah n where
 
 /--
 error: Missing cases:
-(Blah.mk (Nat.succ (Nat.succ _)))
 (Blah.mk Nat.zero)
+(Blah.mk (Nat.succ (Nat.succ _)))
 -/
 #check_msgs in
 def abc (n : Blah) : Bool :=
@@ -1394,25 +1394,16 @@ structure OnlyThreeOrFive where
   ok : val = 3 ∨ val = 5 := by rfl
 
 
--- Default args are synthesized in patterns too!
+-- Default args are not synthesized in patterns
 /--
-error: Tactic `rfl` failed: The left-hand side
-  n = 3
-is not definitionally equal to the right-hand side
-  n = 5
-
-x✝ : OnlyThreeOrFive
-n : Nat
-⊢ n = 3 ∨ n = 5
+error: Fields missing: `val2`, `ok`
 -/
 #check_msgs in
 def ggg : OnlyThreeOrFive → Nat
   | {val := n} => n
 
 /--
-error: Missing cases:
-(OnlyThreeOrFive.mk _ true (Or.inr Eq.refl))
-(OnlyThreeOrFive.mk _ true (Or.inl Eq.refl))
+error: Fields missing: `val2`
 -/
 #check_msgs in
 def hhh : OnlyThreeOrFive → Nat

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "9de9961a7339b83b1d96131d9fb28df59697f16b",
+   "rev": "ccdfd799c239d81922ecf6f156cee32ee64ef229",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "7fc10c4acacf0a159f75366d048dc1d0fe545b09",
+   "rev": "32b8fbdc543b070f0e76a2b4b1d7fd0ce3e7e837",
    "name": "versowebcomponents",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "22a0afa903bcf65285152eea298a3d319badc78d",
+   "rev": "264309b5c0c10e569025a53ab6440a45c03133e4",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "52b9dfbd2658408e37ae6e8b72601ddeaaa25a0c",
+   "rev": "ce893b9042128037e2d3c0158b9567fab9fae268",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2026-04-02
+leanprover/lean4:nightly-2026-04-15