chore: bump to latest nightly (2025-05-23), elan, and Verso

.github/workflows/ci.yml

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

Main.lean

@@ -16,44 +16,6 @@ def searchModule := {{
   }}
 
 
-def KaTeXLicense : LicenseInfo where
-  identifier := "MIT"
-  dependency := "KaTeX"
-  howUsed := "KaTeX is used to render mathematical notation."
-  link := "https://katex.org/"
-  text := #[(some "The MIT License", text)]
-where
-  text := r#"
-Copyright (c) 2013-2020 Khan Academy and other contributors
-
-Permission is hereby granted, free of charge, to any person obtaining a copy
-of this software and associated documentation files (the "Software"), to deal
-in the Software without restriction, including without limitation the rights
-to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
-copies of the Software, and to permit persons to whom the Software is
-furnished to do so, subject to the following conditions:
-
-The above copyright notice and this permission notice shall be included in all
-copies or substantial portions of the Software.
-
-THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
-IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
-FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
-AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
-LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
-OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
-SOFTWARE.
-"#
-
-
-def addKaTeX (config : Config) : Config :=
-  {config with
-    extraCss := "/static/katex/katex.min.css" :: config.extraCss,
-    extraJs := "/static/katex/katex.min.js" :: "/static/math.js" :: config.extraJs,
-    licenseInfo := KaTeXLicense :: config.licenseInfo
-  }
-
-
 def fuzzysortLicense : LicenseInfo where
   identifier := "MIT"
   dependency := "fuzzysort v3.1.0"
@@ -112,7 +74,7 @@ def scarfPixel := {{
 def main :=
   manualMain (%doc Manual) (config := config)
 where
-  config := addKaTeX {
+  config := Config.addKaTeX {
     extraFiles := [("static", "static")],
     extraCss := [
       "/static/colors.css",

Manual/BuildTools/Elan.lean

@@ -51,6 +51,10 @@ Channels may be:
 
   The latest stable Lean release. Elan automatically tracks stable releases and offers to upgrade when a new one is released.
 
+ : `beta`
+
+  The latest release candidate. Release candidates are builds of Lean that are intended to become the next stable release. They are made available for widespread user testing.
+
  : `nightly`
 
    The latest nightly build. Nightly builds are useful for experimenting with new Lean features to provide feedback to the developers.
@@ -233,8 +237,8 @@ FLAGS:
     -h, --help    Prints help information
 
 ARGS:
-    <toolchain>    Toolchain name, such as 'stable', 'nightly', or '3.3.0'. For more information see `elan help
-                   toolchain`
+    <toolchain>    Toolchain name, such as 'stable', 'beta', 'nightly', or '4.3.0'. For more information see `elan
+                   help toolchain`
 
 DISCUSSION:
     Sets the default toolchain to the one specified.
@@ -278,14 +282,14 @@ DISCUSSION:
     Many `elan` commands deal with *toolchains*, a single
     installation of the Lean theorem prover. `elan` supports multiple
     types of toolchains. The most basic track the official release
-    channels: 'stable' and 'nightly'; but `elan` can also
+    channels: 'stable', 'beta', and 'nightly'; but `elan` can also
     install toolchains from the official archives and from local builds.
 
     Standard release channel toolchain names have the following form:
 
         [<origin>:]<channel>[-<date>]
 
-        <channel>       = stable|nightly|<version>
+        <channel>       = stable|beta|nightly|<version>
         <date>          = YYYY-MM-DD
 
     'channel' is either a named release channel or an explicit version
@@ -327,8 +331,8 @@ FLAGS:
     -h, --help    Prints help information
 
 ARGS:
-    <toolchain>...    Toolchain name, such as 'stable', 'nightly', or '3.3.0'. For more information see `elan help
-                      toolchain`
+    <toolchain>...    Toolchain name, such as 'stable', 'beta', 'nightly', or '4.3.0'. For more information see
+                      `elan help toolchain`
 ```
 
 :::elan toolchain install "toolchain"
@@ -348,8 +352,8 @@ FLAGS:
     -h, --help    Prints help information
 
 ARGS:
-    <toolchain>...    Toolchain name, such as 'stable', 'nightly', or '3.3.0'. For more information see `elan help
-                      toolchain`
+    <toolchain>...    Toolchain name, such as 'stable', 'beta', 'nightly', or '4.3.0'. For more information see
+                      `elan help toolchain`
 ```
 
 :::elan toolchain uninstall "toolchain"
@@ -369,8 +373,8 @@ FLAGS:
     -h, --help    Prints help information
 
 ARGS:
-    <toolchain>    Toolchain name, such as 'stable', 'nightly', or '3.3.0'. For more information see `elan help
-                   toolchain`
+    <toolchain>    Toolchain name, such as 'stable', 'beta', 'nightly', or '4.3.0'. For more information see `elan
+                   help toolchain`
     <path>
 
 DISCUSSION:
@@ -527,8 +531,8 @@ FLAGS:
         --install    Install the requested toolchain if needed
 
 ARGS:
-    <toolchain>     Toolchain name, such as 'stable', 'nightly', or '3.3.0'. For more information see `elan help
-                    toolchain`
+    <toolchain>     Toolchain name, such as 'stable', 'beta', 'nightly', or '4.3.0'. For more information see `elan
+                    help toolchain`
     <command>...
 
 DISCUSSION:

Manual/Elaboration.lean

@@ -185,7 +185,7 @@ example (b : B) : ⟨b.1, b.2⟩ = b := rfl
 error: type mismatch
   rfl
 has type
-  ?m.744 = ?m.744 : Prop
+  ?m.848 = ?m.848 : Prop
 but is expected to have type
   e1 = e2 : Prop
 -/

Manual/Terms.lean

@@ -1321,9 +1321,9 @@ partial instance : OfNat Blah n where
 -- This shows that the partial instance was not unfolded
 /--
 error: Dependent elimination failed: Type mismatch when solving this alternative: it has type
-  motive (instOfNatBlah_1.f 0) : Sort ?u.859
+  motive (instOfNatBlah_1.f 0) : Sort ?u.903
 but is expected to have type
-  motive n✝ : Sort ?u.859
+  motive n✝ : Sort ?u.903
 -/
 #guard_msgs in
 def defg (n : Blah) : Bool :=
@@ -1332,9 +1332,9 @@ def defg (n : Blah) : Bool :=
 
 /--
 error: Dependent elimination failed: Type mismatch when solving this alternative: it has type
-  motive (Float.ofScientific 25 true 1) : Sort ?u.902
+  motive (Float.ofScientific 25 true 1) : Sort ?u.946
 but is expected to have type
-  motive x✝ : Sort ?u.902
+  motive x✝ : Sort ?u.946
 -/
 #guard_msgs in
 def twoPointFive? : Float → Option Float
@@ -1391,7 +1391,7 @@ is not definitionally equal to the right-hand side
   3 = 5
 ⊢ 3 = 3 ∨ 3 = 5
 ---
-info: { val := 3, val2 := ?m.1639, ok := ⋯ } : OnlyThreeOrFive
+info: { val := 3, val2 := ?m.1743, ok := ⋯ } : OnlyThreeOrFive
 -/
 #guard_msgs in
 #check OnlyThreeOrFive.mk 3 ..

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "40ce546e0e1416cedd4eef2fa5a51c7254b16a6b",
+   "rev": "67226e3872aed94c13d19a0e349ecc2832a05b5f",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "nightly-testing",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "83a4aa2bf2fe7346357ba0c63202bba94664dd6f",
+   "rev": "5f3249b337736723c55d62ea0b58b19c7bc14e53",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-05-20
+leanprover/lean4:nightly-2025-05-23