chore: bump to 2026-01-20 (#755)

Author: david-christiansen

Manual/BuildTools/Lake/CLI.lean

@@ -41,6 +41,7 @@ COMMANDS:
   lint                  lint the package using the configured lint driver
   check-lint            check if there is a properly configured lint driver
   clean                 remove build outputs
+  shake                 minimize imports in source files
   env <cmd> <args>...   execute a command in Lake's environment
   lean <file>           elaborate a Lean file in Lake's context
   update                update dependencies and save them to the manifest
@@ -707,6 +708,106 @@ Builds the imports of the given {lakeMeta}`file` and then runs `lean` on it usin
 The `lean` process is executed in {ref "lake-environment"}[Lake's environment].
 :::
 
+# Module Imports
+
+```lakeHelp shake
+Minimize imports in Lean source files
+
+USAGE:
+  lake shake [OPTIONS] [<MODULE>...]
+
+Checks the current project for unused imports by analyzing generated `.olean`
+files to deduce required imports and ensuring that every import contributes
+some constant or other elaboration dependency.
+
+ARGUMENTS:
+  <MODULE>              A module path like `Mathlib`. All files transitively
+                        reachable from the provided module(s) will be checked.
+                        If not specified, uses the package's default targets.
+
+OPTIONS:
+  --force               Skip the `lake build --no-build` sanity check
+  --keep-implied        Preserve imports implied by other imports
+  --keep-prefix         Prefer parent module imports over specific submodules
+  --keep-public         Preserve all `public` imports for API stability
+  --add-public          Add new imports as `public` if they were in the
+                        original public closure
+  --explain             Show which constants require each import
+  --fix                 Apply suggested fixes directly to source files
+  --gh-style            Output in GitHub problem matcher format
+
+ANNOTATIONS:
+  Source files can contain special comments to control shake behavior:
+
+  * `module -- shake: keep-downstream`
+    Preserves this module in all downstream modules
+
+  * `module -- shake: keep-all`
+    Preserves all existing imports in this module
+
+  * `import X -- shake: keep`
+    Preserves this specific import
+```
+
+::::lake shake "[options...] [module ...]"
+
+Checks the current project for unused imports by analyzing generated {tech}[`.olean` files] to deduce required imports, ensuring that every import contributes some constant or other elaboration dependency.
+
+If a {lakeMeta}`module` is specified, then it and all files that are transitively reachable from it are checked. Otherwise, the package's {tech}[default targets] are checked.
+
+:::paragraph
+Source files can contain special comments to control the behavior of {lake}`shake`:
+
+: `module -- shake: keep-downstream`
+
+  Preserves this module in all downstream modules.
+
+: `module -- shake: keep-all`
+
+  Preserves all existing imports in this module.
+
+: `import X -- shake: keep`
+
+  Preserves this specific import.
+:::
+
+:::paragraph
+The {lakeMeta}`options` may be:
+
+: `--force`
+
+  Skip the `lake build --no-build` sanity check
+
+: `--keep-implied`
+
+  Preserve imports implied by other imports
+
+: `--keep-prefix`
+
+  Prefer parent module imports over specific submodules
+
+: `--keep-public`
+
+  Preserve all `public` imports for API stability
+
+: `--add-public`
+
+  Add new imports as `public` if they were in the original public closure
+
+: `--explain`
+
+  Show which constants require each import
+
+: `--fix`
+
+  Apply suggested fixes directly to source files
+
+: `--gh-style`
+
+  Output in GitHub problem matcher format
+:::
+
+::::
 
 # Development Tools
 

lake-manifest.json

@@ -11,25 +11,25 @@
    "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/verso.git",
+  {"url": "https://github.com/leanprover/subverso",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "fc796974205ec2c188b8d17bdd4f95f35197f72b",
-   "name": "verso",
+   "rev": "2aa08940ec078fdf3d4c168bf60091d07ccccbfb",
+   "name": "subverso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing",
+   "inputRev": "main",
    "inherited": false,
    "configFile": "lakefile.lean"},
-  {"url": "https://github.com/leanprover/subverso",
+  {"url": "https://github.com/leanprover/verso",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "7ada0eebb41eefab7c27aeaba0587cc44e0de194",
-   "name": "subverso",
+   "rev": "9b93b87b9301b780ab9f349f5d57586825ef48bb",
+   "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
-   "inherited": true,
+   "inputRev": "nightly-testing",
+   "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",

lakefile.lean

@@ -8,7 +8,8 @@ import Lake
 open Lake DSL
 open System (FilePath)
 
-require verso from git "https://github.com/leanprover/verso.git"@"nightly-testing"
+require verso from git "https://github.com/leanprover/verso"@"nightly-testing"
+require subverso from git "https://github.com/leanprover/subverso"@"main"
 require versowebcomponents from git "https://github.com/leanprover/verso-web-components"@"main"
 
 package "verso-manual" where

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2026-01-16
+leanprover/lean4:nightly-2026-01-20