Bump the Lean version in CI.

Julian · Julian · commit 8b39931f5e7d · 2026-04-18T14:36:57.000-04:00
In 4.30 `2 = 2` is special-er than `37 = 37` and suggests a different
lemma :D

And apparently unfold? no longer needs the wait...
diff --git a/demos/project/lake-manifest.json b/demos/project/lake-manifest.json
@@ -1,11 +1,11 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "76af11c66b4608f33b1346b877119458d0a50110",
+   "rev": "9b51fe6ec0377d1e0f1ebeb551a7ab8d9ad8f3a4",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "22a0afa903bcf65285152eea298a3d319badc78d",
+   "rev": "86210d4ad1b08b086d0bd638637a75246523dbb8",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "db22912cdd820b2a2bd84bd25273cb322ff09ead",
+   "rev": "cdab3938ccabbdb044be6896e251b5814bec932e",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,51 +45,52 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "136730b5a40dc633967f5433cb7668df5c3bf9a3",
+   "rev": "2db6054a44326f8c0230ee0570e2ddb894816511",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.94",
+   "inputRev": "v0.0.98",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3426969888a264d3f69b6f30ab50aa11f28eb38d",
+   "rev": "f0c6e183ea26531e82773feb4b73ab6595ca17a5",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.30.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3a9fde028258300f1cbb003d457d47c8d8e16b1c",
+   "rev": "1cc7e819b9b9bc1e87c9edcccb62e0269e00a809",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.30.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bce25af79ec73f5e63240d4399a4cd8a6a227fcb",
+   "rev": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.30.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "61cd682f2a25175996bc1b9e8d8231e76cded866",
+   "rev": "13567aed1ac4f12aea9484178e07e51f8c9f7658",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0-rc8",
+   "inputRev": "v4.30.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "NeovimLoves",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/demos/project/lean-toolchain b/demos/project/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.29.0-rc8
+leanprover/lean4:v4.30.0-rc2
diff --git a/spec/fixtures/projects/Example/lake-manifest.json b/spec/fixtures/projects/Example/lake-manifest.json
@@ -1,4 +1,4 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"type": "path",
@@ -9,4 +9,5 @@
    "dir": "foo",
    "configFile": "lakefile.toml"}],
  "name": "example",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/spec/fixtures/projects/Example/lean-toolchain b/spec/fixtures/projects/Example/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.29.0-rc8
+leanprover/lean4:v4.30.0-rc2
diff --git a/spec/fixtures/projects/SimpleFakeCoreLean/lean-toolchain b/spec/fixtures/projects/SimpleFakeCoreLean/lean-toolchain
@@ -1 +1 @@
-build/release/stage1
+leanprover/lean4:v4.30.0-rc2
diff --git a/spec/fixtures/projects/WithWidgets/lake-manifest.json b/spec/fixtures/projects/WithWidgets/lake-manifest.json
@@ -1,11 +1,11 @@
-{"version": "1.1.0",
+{"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "76af11c66b4608f33b1346b877119458d0a50110",
+   "rev": "9b51fe6ec0377d1e0f1ebeb551a7ab8d9ad8f3a4",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "136730b5a40dc633967f5433cb7668df5c3bf9a3",
+   "rev": "2db6054a44326f8c0230ee0570e2ddb894816511",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "db22912cdd820b2a2bd84bd25273cb322ff09ead",
+   "rev": "cdab3938ccabbdb044be6896e251b5814bec932e",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "22a0afa903bcf65285152eea298a3d319badc78d",
+   "rev": "86210d4ad1b08b086d0bd638637a75246523dbb8",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,41 +55,42 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3426969888a264d3f69b6f30ab50aa11f28eb38d",
+   "rev": "f0c6e183ea26531e82773feb4b73ab6595ca17a5",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.30.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3a9fde028258300f1cbb003d457d47c8d8e16b1c",
+   "rev": "1cc7e819b9b9bc1e87c9edcccb62e0269e00a809",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.30.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "bce25af79ec73f5e63240d4399a4cd8a6a227fcb",
+   "rev": "5c57f3857ba81924a88b2cdf4f062e34ec04ff11",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.30.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "61cd682f2a25175996bc1b9e8d8231e76cded866",
+   "rev": "13567aed1ac4f12aea9484178e07e51f8c9f7658",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.29.0-rc8",
+   "inputRev": "v4.30.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "WithWidgets",
- "lakeDir": ".lake"}
+ "lakeDir": ".lake",
+ "fixedToolchain": false}
diff --git a/spec/fixtures/projects/WithWidgets/lean-toolchain b/spec/fixtures/projects/WithWidgets/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.29.0-rc8
+leanprover/lean4:v4.30.0-rc2
diff --git a/spec/widgets/core_spec.lua b/spec/widgets/core_spec.lua
@@ -29,7 +29,7 @@ describe('Lean core widgets', function()
     'supports try this widgets with one suggestion',
     helpers.clean_buffer(
       [[
-        example : 2 = 2 := by
+        example : 37 = 37 := by
           apply?
       ]],
       function()
@@ -38,7 +38,7 @@ describe('Lean core widgets', function()
         assert.infoview_contents.are [[
           Goals accomplished 🎉
 
-          ⊢ 2 = 2
+          ⊢ 37 = 37
 
           ▼ 2:3-2:9: information:
           Try this:
@@ -52,7 +52,7 @@ describe('Lean core widgets', function()
         -- the buffer contents have changed but we also jumped to the lean win
         assert.current_window.is(lean_window)
         assert.contents.are [[
-          example : 2 = 2 := by
+          example : 37 = 37 := by
             exact Nat.eq_of_beq_eq_true rfl
         ]]
       end
diff --git a/spec/widgets/mathlib_spec.lua b/spec/widgets/mathlib_spec.lua
@@ -76,7 +76,6 @@ describe('Mathlib widgets', function()
 
         helpers.search 'Uninteresting'
         helpers.feed 'gK'
-        helpers.wait_for_async_elements()
 
         assert.infoview_contents.are [[
           ⊢ isUninteresting 73

Original file line number	Diff line number	Diff line change
`@@ -1 +1 @@`
`1`		`-leanprover/lean4:v4.29.0-rc8`
	`1`	`+leanprover/lean4:v4.30.0-rc2`
Original file line number	Diff line number	Diff line change
`@@ -1 +1 @@`
`1`		`-build/release/stage1`
	`1`	`+leanprover/lean4:v4.30.0-rc2`