chore: bump to nightly-2026-04-01 (#821)

Author: david-christiansen

.github/workflows/ci.yml

@@ -403,11 +403,14 @@ jobs:
                   name: "html"
                   path: "_out/"
 
-            - name: Install TypeScript
-              run: |
-                  sudo apt update && sudo apt install node-typescript
+            - uses: actions/setup-node@v4
+              with:
+                  node-version: "lts/*"
+                  cache: npm
+
+            - run: npm ci
 
             - name: Type check the search bar code
               run: |
                   cd _out/html-multi/-verso-search
-                  tsc --noEmit -p jsconfig.json
+                  npx tsc --noEmit -p jsconfig.json

Manual/Axioms.lean

@@ -93,7 +93,7 @@ The existence of this function contradicts the “free theorem”:
 ```lean
 theorem unit_not_nat : Unit ≠ Nat := by
   intro eq
-  have ⟨allEq⟩ := eq ▸ inferInstanceAs (Subsingleton Unit)
+  have ⟨allEq⟩ := eq ▸ (inferInstance : Subsingleton Unit)
   specialize allEq 0 1
   contradiction
 

Manual/BasicTypes/Subtype.lean

@@ -76,7 +76,7 @@ def s2 : NonEmptyString where
   val := "equal"
   property :=
     fun h =>
-      List.cons_ne_nil _ _ (String.data_eq_of_eq h)
+      List.cons_ne_nil _ _ (String.ext_iff.mp h)
 
 theorem s1_eq_s2 : s1 = s2 := by rfl
 ```
@@ -98,7 +98,7 @@ def s2 : NonEmptyString where
   val := "equal"
   property :=
     fun h =>
-      List.cons_ne_nil _ _ (String.data_eq_of_eq h)
+      List.cons_ne_nil _ _ (String.ext_iff.mp h)
 
 theorem s1_eq_s2 : s1 = s2 := by
   ext

Manual/BuildTools/Lake.lean

@@ -375,6 +375,7 @@ module.input
 module.ir
 module.lean
 module.leanArts
+module.ltar
 module.o
 module.o.export
 module.o.noexport
@@ -477,6 +478,10 @@ The facets available for modules are:
 
   A shared library (e.g., for the Lean option `--load-dynlib`){TODO}[Document Lean command line options, and cross-reference from here].
 
+: `ltar`
+
+  A compressed archive (produced via `leantar`) of the module's build artifacts. {TODO}[Document `leantar` in the manual as well]
+
 :::
 
 

Manual/BuildTools/Lake/CLI.lean

@@ -1117,6 +1117,11 @@ COMMANDS:
   clean                 removes ALL froms the local Lake cache
   services              print configured remote cache services
 
+STAGING COMMANDS:
+  stage <map> <dir>     copy build outputs from the cache to a directory
+  unstage <dir>         cache build outputs from a staging directory
+  put-staged <dir>      upload build outputs from a staging directory
+
 See `lake cache help <command>` for more information on a specific command.
 ```
 
@@ -1134,11 +1139,11 @@ OPTIONS:
   --platform=<target-triple>      with Reservoir or --repo, sets the platform
   --toolchain=<name>              with Reservoir or --repo, sets the toolchain
   --scope=<remote-scope>          scope for a custom endpoint
-  --download-arts                 download artifacts now, not on demand
+  --mappings-only                 only download mappings, delay artifacts
   --force-download                redownload existing files
 
 Downloads build outputs for packages in the workspace from a remote cache
-service. The cache service used can be specifed via the `--service` option.
+service. The cache service used can be specified via the `--service` option.
 Otherwise, Lake will the system default, or, if none is configured, Reservoir.
 See `lake cache services` for more information on how to configure services.
 
@@ -1165,17 +1170,16 @@ artifacts. If no mappings are found, Lake will backtrack the Git history up to
 `--max-revs`, looking for a revision with mappings. If `--max-revs` is 0, Lake
 will search the repository's entire history (or as far as Git will allow).
 
-With a named service and without a mappings file, Lake will only download
-the input-to-output mappings for packages. It will delay downloading of the
-corresponding artifacts to the next `lake build` that requires them. Using
-`--download-arts` will force Lake to download all artifacts eagerly.
+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.
 
 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,
 if any download failed, Lake will exit with a nonzero status code.
 ```
 
-:::lake cache get "[mappings] [\"--max-revs=\" cn] [\"--rev=\" «commit-hash»] [\"--service=\" «name»] [\"--repo=\" «github-repo»] [\"--platform=\" «target-triple»] [\"--toolchain=\"«name»] [\"--scope=\" «remote-scope»] [\"--download-arts\"] [\"--force-download\"]"
+:::lake cache get "[mappings] [\"--max-revs=\" cn] [\"--rev=\" «commit-hash»] [\"--service=\" «name»] [\"--repo=\" «github-repo»] [\"--platform=\" «target-triple»] [\"--toolchain=\"«name»] [\"--scope=\" «remote-scope»] [\"--mappings-only\"] [\"--force-download\"]"
 Downloads build outputs for packages in the workspace from a remote cache service to the local Lake {tech (key:="local cache")}[artifact cache].
 The cache service used can be specified via the {lakeOpt}`--service` option.
 Otherwise, Lake will use the system default, or, if none is configured, Reservoir.
@@ -1195,9 +1199,8 @@ Lake will download the artifacts for the most recent commit with available mappi
 It will backtrack up to {lakeOptDef option}`--max-revs`, which defaults to 100.
 If set to 0, Lake will search the repository's whole history, or as far back as Git will allow.
 
-With a named service and without a mappings file, Lake will only download the input-to-output mappings for packages.
-It will delay downloading of the corresponding artifacts to the next `lake build` that requires them.
-Using {lakeOptDef option}`--download-arts` will force Lake to download all artifacts eagerly.
+By default, Lake will download both the input-to-output mappings and the output artifacts for packages.
+Using {lakeOptDef option}`--mappings-only` will cause Lake to only download the mappings and delay downloading artifacts until they are needed.
 Using {lakeOptDef option}`--force-download` will redownload existing files.
 
 While downloading, Lake will continue on when a download for an artifact fails or if the download process for a whole package fails.
@@ -1213,7 +1216,7 @@ USAGE:
 
 Uploads the input-to-output mappings contained in the specified file along
 with the corresponding output artifacts to a remote cache. The cache service
-used via be specified via `--service` option. If not specifed, Lake will used
+used can be specified via the `--service` option. If not specified, Lake will use
 the system default, or error if none is configured. See the help page of
 `lake cache services` for more information on how to configure services.
 
@@ -1282,7 +1285,7 @@ As such, the command will warn if the work tree currently has changes.
 ::::
 
 ```lakeCacheHelp add
-Addd input-to-output mappings to the Lake cache
+Add input-to-output mappings to the Lake cache
 
 USAGE:
   lake cache add <mappings>
@@ -1377,6 +1380,70 @@ If no `cache.defaultService` is configured, Lake will use Reservoir by default.
 :::
 ::::
 
+```lakeCacheHelp stage
+Copy build outputs from the cache to a staging directory
+
+USAGE:
+  lake cache stage <mappings> <staging-directory>
+
+Creates the staging directory and copies the mappings file to it. Then, it
+copies all artifacts described within the mappings file from the cache to the
+staging directory. Errors if any of the artifacts described cannot be found in
+the cache.
+```
+
+::::lake cache stage "mappings «staging-directory»"
+Creates {lakeMeta}`staging-directory` and copies the {lakeMeta}`mappings` file to it.
+After this, it copies all artifacts described within the mappings file from the cache to the
+staging directory.
+It is an error if any of the artifacts described cannot be found in the cache.
+::::
+
+```lakeCacheHelp unstage
+Cache build outputs from a staging directory
+
+USAGE:
+  lake cache unstage <staging-directory>
+
+Copies the mappings and artifacts stored in staging directory (e.g., via
+`lake cache stage`) back into the cache.
+
+Reads the mappings file located at `outputs.jsonl` within the staging
+directory and writes the mappings to the Lake cache. Then, it copies the
+described artifacts from the staging directory into the cache.
+```
+
+::::lake cache unstage "«staging-directory»"
+
+Copies the mappings and artifacts stored in {lakeMeta}`staging-directory` (e.g., via {lake}`cache stage`) back into the cache.
+
+Reads the mappings file located at `outputs.jsonl` within the staging
+directory and writes the mappings to the Lake cache. Then, it copies the
+described artifacts from the staging directory into the cache.
+::::
+
+
+```lakeCacheHelp "put-stage"
+Manage the Lake cache
+
+USAGE:
+  lake cache <COMMAND>
+
+COMMANDS:
+  get [<mappings>]      download build outputs into the local Lake cache
+  put <mappings>        upload build ouptuts to a remote cache
+  add <mappings>        add input-to-output mappings to the Lake cache
+  clean                 removes ALL froms the local Lake cache
+  services              print configured remote cache services
+
+STAGING COMMANDS:
+  stage <map> <dir>     copy build outputs from the cache to a directory
+  unstage <dir>         cache build outputs from a staging directory
+  put-staged <dir>      upload build outputs from a staging directory
+
+See `lake cache help <command>` for more information on a specific command.
+```
+
 
 # Configuration Files
 

Manual/BuildTools/Lake/Config.lean

@@ -161,7 +161,6 @@ name = "example-package"
           dynlibs := #[],
           plugins := #[] },
       bootstrap := false,
-      manifestFile := none,
       extraDepTargets := #[],
       precompileModules := false,
       moreGlobalServerArgs := #[],
@@ -190,7 +189,8 @@ name = "example-package"
       enableArtifactCache? := none,
       restoreAllArtifacts? := none,
       libPrefixOnWindows := false,
-      allowImportAll := false},
+      allowImportAll := false,
+      fixedToolchain := false},
   configFile := FilePath.mk "lakefile",
   relConfigFile := FilePath.mk "lakefile",
   relManifestFile := FilePath.mk "lake-manifest.json",
@@ -205,9 +205,7 @@ name = "example-package"
   postUpdateHooks := #[],
   buildArchive := ELIDED,
   testDriver := "",
-  lintDriver := "",
-  inputsRef? := none,
-  outputsRef? := none}
+  lintDriver := ""}
 ```
 ::::
 :::::
@@ -249,7 +247,6 @@ name = "Sorting"
           dynlibs := #[],
           plugins := #[] },
       bootstrap := false,
-      manifestFile := none,
       extraDepTargets := #[],
       precompileModules := false,
       moreGlobalServerArgs := #[],
@@ -278,7 +275,8 @@ name = "Sorting"
       enableArtifactCache? := none,
       restoreAllArtifacts? := none,
       libPrefixOnWindows := false,
-      allowImportAll := false},
+      allowImportAll := false,
+      fixedToolchain := false},
   configFile := FilePath.mk "lakefile",
   relConfigFile := FilePath.mk "lakefile",
   relManifestFile := FilePath.mk "lake-manifest.json",
@@ -365,9 +363,7 @@ name = "Sorting"
   postUpdateHooks := #[],
   buildArchive := ELIDED,
   testDriver := "",
-  lintDriver := "",
-  inputsRef? := none,
-  outputsRef? := none}
+  lintDriver := ""}
 ```
 ::::
 :::::

Manual/Meta/Monotonicity.lean

@@ -146,11 +146,13 @@ def mkMonotonicityLemmas : TermElabM Name := do
                 pure .continue)
 
             let hlCall ← withOptions (·.setBool `pp.tagAppFns true) do
+              let sigCache ← IO.mkRef {}
               let ctxt := {
                 ids := {},
                 definitionsPossible := false,
                 includeUnparsed := false,
-                suppressNamespaces := []
+                suppressNamespaces := [],
+                sigCache
               }
               let fmt ← Lean.Widget.ppExprTagged call'
               (renderTagged none fmt : ReaderT SubVerso.Highlighting.Context _ _).run ctxt

Manual/RecursiveDefs/WF.lean

@@ -851,7 +851,7 @@ The definition of {name}`WellFounded` builds on the notion of _accessible elemen
 The definition of division by iterated subtraction can be written explicitly using well-founded recursion.
 ```lean
 noncomputable def div (n k : Nat) : Nat :=
-  (inferInstanceAs (WellFoundedRelation Nat)).wf.fix
+  (inferInstance : WellFoundedRelation Nat).wf.fix
     (fun n r =>
       if h : k = 0 then 0
       else if h : k > n then 0