chore: bump toolchain to v4.31.0-rc1 (#857)

Co-authored-by: github-actions[bot] <github-actions[bot]@users.noreply.github.com>
Co-authored-by: David Thrane Christiansen <david@lean-fro.org>
Co-authored-by: jcreedcmu <jcreed@gmail.com>
Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Co-authored-by: Sebastian Graf <sgraf1337@gmail.com>
Co-authored-by: Robert J. Simmons <442315+robsimmons@users.noreply.github.com>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
Co-authored-by: Pim Otte <otte.pim@gmail.com>
Co-authored-by: Phil Nguyen <pcn@cs.umd.edu>
Co-authored-by: Violetta Sim <38787503+eyihluyc@users.noreply.github.com>
Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: euprunin <178733547+euprunin@users.noreply.github.com>
Co-authored-by: u <u@h>
Co-authored-by: Pablo Graubner <2234137+pgraubner@users.noreply.github.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Marc Huisinga <mhuisi@protonmail.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: jrr6 <7482866+jrr6@users.noreply.github.com>
Co-authored-by: Leonardo de Moura <leomoura@amazon.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Violetta Sim <38787503+viol37@users.noreply.github.com>
Co-authored-by: Rob Simmons <rob@lean-fro.org>
Co-authored-by: leanprover-bot <leanprover-bot@lean-fro.org>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Wojciech Różowski <wojciech@lean-fro.org>
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
Co-authored-by: Richard Davison <richard.neil.davison@gmail.com>
Co-authored-by: Chris Su <102528557+chrissuu@users.noreply.github.com>
Co-authored-by: ericrbg-harmonic <eric@harmonic.fun>
Co-authored-by: Mac Malone <tydeu@hatpress.net>

Author: 30 people

.github/workflows/ci.yml

@@ -29,7 +29,7 @@ jobs:
             - name: Install elan
               run: |
                   set -o pipefail
-                  curl -sSfL https://github.com/leanprover/elan/releases/download/v4.1.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+                  curl -sSfL https://github.com/leanprover/elan/releases/download/v4.2.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
                   ./elan-init -y --default-toolchain none
                   echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
 

.github/workflows/discover-lean-pr-testing.yml

@@ -33,7 +33,7 @@ jobs:
             - name: Install elan
               run: |
                   set -o pipefail
-                  curl -sSfL https://github.com/leanprover/elan/releases/download/v4.1.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+                  curl -sSfL https://github.com/leanprover/elan/releases/download/v4.2.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
                   ./elan-init -y --default-toolchain none
                   echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
 

.github/workflows/merge-main-nightly.yml

@@ -38,7 +38,7 @@ jobs:
             - name: Install elan
               run: |
                   set -o pipefail
-                  curl -sSfL https://github.com/leanprover/elan/releases/download/v4.1.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+                  curl -sSfL https://github.com/leanprover/elan/releases/download/v4.2.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
                   ./elan-init -y --default-toolchain none
                   echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
 

.github/workflows/pr-testing.yml

@@ -15,7 +15,7 @@ jobs:
             - name: Install elan
               run: |
                   set -o pipefail
-                  curl -sSfL https://github.com/leanprover/elan/releases/download/v4.1.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+                  curl -sSfL https://github.com/leanprover/elan/releases/download/v4.2.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
                   ./elan-init -y --default-toolchain none
                   echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
 

.github/workflows/release-tag.yml

@@ -43,7 +43,7 @@ jobs:
             - name: Install elan
               run: |
                   set -o pipefail
-                  curl -sSfL https://github.com/leanprover/elan/releases/download/v4.1.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+                  curl -sSfL https://github.com/leanprover/elan/releases/download/v4.2.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
                   ./elan-init -y --default-toolchain none
                   echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
 

.github/workflows/update-nightly.yml

@@ -96,7 +96,7 @@ jobs:
             - name: Install elan
               run: |
                   set -o pipefail
-                  curl -sSfL https://github.com/leanprover/elan/releases/download/v4.1.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
+                  curl -sSfL https://github.com/leanprover/elan/releases/download/v4.2.2/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
                   ./elan-init -y --default-toolchain none
                   echo "$HOME/.elan/bin" >> "$GITHUB_PATH"
 

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/Elan.lean

@@ -390,7 +390,7 @@ DISCUSSION:
         $ elan toolchain link master <path/to/lean/root>
         $ elan override set master
 
-    If you now compile a crate in the current directory, the custom
+    If you now compile a package in the current directory, the custom
     toolchain 'master' will be used.
 ```
 

Manual/BuildTools/Lake/CLI.lean

@@ -38,7 +38,7 @@ COMMANDS:
   check-build           check if any default build targets are configured
   test                  test the package using the configured test driver
   check-test            check if there is a properly configured test driver
-  lint                  lint the package using the configured lint driver
+  lint                  lint the package
   check-lint            check if there is a properly configured lint driver
   clean                 remove build outputs
   shake                 minimize imports in source files
@@ -67,6 +67,7 @@ BASIC OPTIONS:
   --packages=file       JSON file of package entries that override the manifest
   --reconfigure, -R     elaborate configuration files instead of using OLeans
   --keep-toolchain      do not update toolchain on workspace update
+  --allow-empty         accept bare builds with no default targets configured
   --no-build            exit immediately if a build target is not up-to-date
   --no-cache            build packages locally; do not download build caches
   --try-cache           attempt to download build caches for supported packages
@@ -291,11 +292,14 @@ Single-character flags cannot be combined; `-HR` is not equivalent to `-H -R`.
 
 : {lakeOptDef flag}`--rehash` or {lakeOptDef flag}`-H`
 
-  Ignored cached file hashes, recomputing them.
+  Ignore cached file hashes, recomputing them.
   Lake uses hashes of dependencies to determine whether to rebuild an artifact.
   These hashes are cached on disk whenever a module is built.
   To save time during builds, these cached hashes are used instead of recomputing each hash unless {lakeOpt}`--rehash` is specified.
 
+: {lakeOptDef flag}`--allow-empty`
+
+  Accept builds that produce no output when no {tech}[default targets] are configured.
 
 : {lakeOptDef flag}`--update`
 
@@ -844,29 +848,93 @@ A library test driver will just be built; it is expected that tests are implemen
 :::
 
 ```lakeHelp lint
-Lint the workspace's root package using its configured lint driver
+Lint the workspace's root package
 
 USAGE:
-  lake lint [-- <args>...]
+  lake lint [OPTIONS] [<MODULE>...] [-- <args>...]
+
+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`, `--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.
+
+Positional `MODULE` arguments narrow only the builtin lints; if omitted,
+the workspace's default target roots are used. The lint driver is invoked
+with `lintDriverArgs` from the package config plus any arguments after
+`--`; the `MODULE` list is not passed to it.
+
+OPTIONS:
+  --builtin-lint        run builtin environment and text linters
+  --builtin-only        run only builtin linters, skip the lint driver
+  --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)
 
 A lint driver can be configured by either setting the `lintDriver` package
-configuration option by tagging a script or executable `@[lint_driver]`.
-A definition in dependency can be used as a test driver by using the
-`<pkg>/<name>` syntax for the 'testDriver' configuration option.
+configuration option or by tagging a script or executable `@[lint_driver]`.
+A definition in a dependency can be used as a lint driver by using the
+`<pkg>/<name>` syntax for the 'lintDriver' configuration option.
 
-A script lint driver will be run with the  package configuration's
+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.
 
 ```
 
-:::lake lint " [\"--\" args...]"
+:::lake lint "[options...] [module...] [\"--\" args...]"
 
-Lint the workspace's root package using its configured lint driver
+By default, lint the workspace's root package using its configured lint driver.
+If `builtinLint` is set to {name}`true` in the package configuration, builtin lints also run.
+
+Positional {lakeMeta}`module` arguments narrow only the builtin lints; if omitted,
+the workspace's default target roots are used. The lint driver is invoked
+with `lintDriverArgs` from the package config plus any arguments after
+`--`; the {lakeMeta}`module` list is not passed to it.
 
 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 extra linters; these linters are run only when `--extra` is specified.
+
+The {lakeMeta}`options` may be:
+
+: `--builtin-lint`
+
+  Run default builtin environment and text linters
+
+: `--builtin-only`
+
+  Run only default builtin linters, skip the lint driver
+
+: `--extra`
+
+  Run only non-default (extra) builtin linters
+
+: `--lint-all`
+
+  Run all registered linters, including defaults, extra,
+  and any other disabled-by-default linters
+
+: `--lint-only` `<name>`
+
+  Run only the specified linter (repeatable).
+
+
+
+A lint driver can be configured by either setting the `lintDriver` package
+configuration option or by tagging a script or executable `@[lint_driver]`.
+A definition in a dependency can be used as a lint driver by using the
+`<pkg>/<name>` syntax for the 'lintDriver' configuration option.
+
+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.
 :::
 
 ```lakeHelp "check-test"
@@ -1114,9 +1182,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 +1242,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 +1365,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 +1501,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/BuildTools/Lake/Config.lean

@@ -190,13 +190,15 @@ name = "example-package"
       restoreAllArtifacts? := none,
       libPrefixOnWindows := false,
       allowImportAll := false,
+      builtinLint? := none,
       fixedToolchain := false},
   configFile := FilePath.mk "lakefile",
   relConfigFile := FilePath.mk "lakefile",
   relManifestFile := FilePath.mk "lake-manifest.json",
   scope := "",
   remoteUrl := "",
   depConfigs := #[],
+  depPkgs := #[],
   targetDecls := #[],
   targetDeclMap := {},
   defaultTargets := #[],
@@ -276,13 +278,15 @@ name = "Sorting"
       restoreAllArtifacts? := none,
       libPrefixOnWindows := false,
       allowImportAll := false,
+      builtinLint? := none,
       fixedToolchain := false},
   configFile := FilePath.mk "lakefile",
   relConfigFile := FilePath.mk "lakefile",
   relManifestFile := FilePath.mk "lake-manifest.json",
   scope := "",
   remoteUrl := "",
   depConfigs := #[],
+  depPkgs := #[],
   targetDecls :=
     #[{toConfigDecl :=
           {pkg := `«example-package»,