chore: bump to nightly-2026-05-06 (#845)

Author: david-christiansen

Manual/BasicTypes/UInt.lean

@@ -198,15 +198,15 @@ This is not equivalent to C's `sizeof` operator, which instead determines how ma
 {docstring Int64.ofInt}
 
 
-{docstring ISize.ofIntTruncate}
+{docstring ISize.ofIntClamp}
 
-{docstring Int8.ofIntTruncate}
+{docstring Int8.ofIntClamp}
 
-{docstring Int16.ofIntTruncate}
+{docstring Int16.ofIntClamp}
 
-{docstring Int32.ofIntTruncate}
+{docstring Int32.ofIntClamp}
 
-{docstring Int64.ofIntTruncate}
+{docstring Int64.ofIntClamp}
 
 
 {docstring ISize.ofIntLE}
@@ -254,15 +254,15 @@ This is not equivalent to C's `sizeof` operator, which instead determines how ma
 
 {docstring UInt64.ofNatLT}
 
-{docstring USize.ofNatTruncate}
+{docstring USize.ofNatClamp}
 
-{docstring UInt8.ofNatTruncate}
+{docstring UInt8.ofNatClamp}
 
-{docstring UInt16.ofNatTruncate}
+{docstring UInt16.ofNatClamp}
 
-{docstring UInt32.ofNatTruncate}
+{docstring UInt32.ofNatClamp}
 
-{docstring UInt64.ofNatTruncate}
+{docstring UInt64.ofNatClamp}
 
 {docstring USize.toNat}
 

Manual/BuildTools/Lake/CLI.lean

@@ -856,7 +856,7 @@ USAGE:
 By default, runs the package's configured lint driver. If `builtinLint` is
 set to `true` in the package configuration, builtin lints also run.
 
-Builtin linting (`--builtin-lint`, `--builtin-only`, `--clippy`, `--lint-all`,
+Builtin linting (`--builtin-lint`, `--builtin-only`, `--extra`, `--lint-all`,
 `--lint-only`, or `builtinLint = true` in the package configuration) drives a
 build of the targeted modules with the requested linter options enabled.
 The lint driver path on its own does not trigger a build.
@@ -869,8 +869,9 @@ with `lintDriverArgs` from the package config plus any arguments after
 OPTIONS:
   --builtin-lint        run builtin environment and text linters
   --builtin-only        run only builtin linters, skip the lint driver
-  --clippy              run only non-default (clippy) builtin linters
-  --lint-all            run all registered linters, including defaults, clippy,
+  --extra               run default builtin linters together with the
+                        non-default (extra) ones
+  --lint-all            run all registered linters, including defaults, extras,
                         and any other disabled-by-default linters
   --lint-only <name>    run only the specified linter (repeatable)
 
@@ -899,7 +900,7 @@ A script lint driver will be run with the  package configuration's
 `lintDriverArgs` plus the CLI `args`. An executable lint driver will be
 built and then run like a script.
 
-The builtin linters are a set of linters that can run as part of a build. Some of them are run by default; these linters are run when `--builtin-lint` is specified. Other linters are {deftech}_clippy_ linters; these linters are run only when `--clippy` is specified.
+The builtin linters are a set of linters that can run as part of a build. Some of them are run by default; these linters are run when `--builtin-lint` is specified. Other linters are extra linters; these linters are run only when `--extra` is specified.
 
 The {lakeMeta}`options` may be:
 
@@ -911,13 +912,13 @@ The {lakeMeta}`options` may be:
 
   Run only default builtin linters, skip the lint driver
 
-: `--clippy`
+: `--extra`
 
-  Run only non-default (clippy) builtin linters
+  Run only non-default (extra) builtin linters
 
 : `--lint-all`
 
-  Run all registered linters, including defaults, clippy,
+  Run all registered linters, including defaults, extra,
   and any other disabled-by-default linters
 
 : `--lint-only` `<name>`

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "83a07ade5228bad7db459752365bc10e386aa4b4",
+   "rev": "9e09309734ee42169a74d416637b89387d7281b2",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "3fa35e950da39bb594dedb0208d438d512d3aaa1",
+   "rev": "f019dfb95839acca9867bd0b965be8632c1aa935",
    "name": "illuminate",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2026-05-01
+leanprover/lean4:nightly-2026-05-06