Bump the Lean versions in CI.

Refs: leanprover-community/import-graph#86
Refs: leanprover/lean4#10524

Author: Julian

demos/project/lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e568f0d0bc8fd18c98e8cf40e7b8f7bdbf7d42ba",
+   "rev": "b8aaf14a892866ba8333faac94f658b9dc557afa",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b949552f6ca8e223f424b3e3b33f74185bbf1179",
+   "rev": "8864a73bf79aad549e34eff972c606343935106d",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
+   "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d768126816be17600904726ca7976b185786e6b9",
+   "rev": "451499ea6e97cee4c8979b507a9af5581a849161",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "556caed0eadb7901e068131d1be208dd907d07a2",
+   "rev": "fb8ed0a85a96e3176f6e94b20d413ea72d92576d",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.74",
+   "inputRev": "v0.0.77",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "725ac8cd67acd70a7beaf47c3725e23484c1ef50",
+   "rev": "1fa48c6a63b4c4cda28be61e1037192776e77ac0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2676cb5599c12c434daac781e2cea44e8105fc41",
+   "rev": "95c2f8afe09d9e49d3cacca667261da04f7f93f7",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee",
+   "rev": "c029ceb9956ef9d567fc034e5403ec829f8d0d87",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "91c18fa62838ad0ab7384c03c9684d99d306e1da",
+   "rev": "72ae7004d9f0ddb422aec5378204fdd7828c5672",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.25.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "NeovimLoves",

demos/project/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.24.0
+leanprover/lean4:v4.25.0-rc2

spec/fixtures/projects/Example/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.24.0
+leanprover/lean4:v4.25.0-rc2

spec/fixtures/projects/WithWidgets/lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e568f0d0bc8fd18c98e8cf40e7b8f7bdbf7d42ba",
+   "rev": "b8aaf14a892866ba8333faac94f658b9dc557afa",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b21695ed5db9bd30f7816621fa9ac142cae39a8f",
+   "rev": "995d1c221c336797a3da97f780e8060ad7ecbfc4",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d768126816be17600904726ca7976b185786e6b9",
+   "rev": "451499ea6e97cee4c8979b507a9af5581a849161",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b949552f6ca8e223f424b3e3b33f74185bbf1179",
+   "rev": "8864a73bf79aad549e34eff972c606343935106d",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "99657ad92e23804e279f77ea6dbdeebaa1317b98",
+   "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "725ac8cd67acd70a7beaf47c3725e23484c1ef50",
+   "rev": "1fa48c6a63b4c4cda28be61e1037192776e77ac0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2676cb5599c12c434daac781e2cea44e8105fc41",
+   "rev": "95c2f8afe09d9e49d3cacca667261da04f7f93f7",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8da40b72fece29b7d3fe3d768bac4c8910ce9bee",
+   "rev": "c029ceb9956ef9d567fc034e5403ec829f8d0d87",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "91c18fa62838ad0ab7384c03c9684d99d306e1da",
+   "rev": "72ae7004d9f0ddb422aec5378204fdd7828c5672",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.25.0-rc2",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "WithWidgets",

spec/fixtures/projects/WithWidgets/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.24.0
+leanprover/lean4:v4.25.0-rc2

spec/widgets/core_spec.lua

@@ -41,11 +41,11 @@ describe('Lean core widgets', function()
 
           ▼ 2:3-2:9: information:
           Try this:
-            exact rfl
+            [apply] exact rfl
         ]]
 
         infoview.go_to()
-        helpers.search 'exact '
+        helpers.search 'apply] '
         helpers.feed '<CR>'
 
         -- the buffer contents have changed but we also jumped to the lean win
@@ -71,11 +71,11 @@ describe('Lean core widgets', function()
 
           ▼ 1:62-1:68: information:
           Try this:
-            exact rfl
+            [apply] exact rfl
         ]]
 
         infoview.go_to()
-        helpers.search 'exact '
+        helpers.search 'apply] '
         helpers.feed '<CR>'
 
         assert.current_window.is(lean_window)
@@ -109,8 +109,8 @@ describe('Lean core widgets', function()
 
           ▼ 11:3-11:6: information:
           Try these:
-            • trivial
-            • sorry
+            [apply] trivial
+            [apply] sorry
         ]]
       end
     )
@@ -140,11 +140,11 @@ describe('Lean core widgets', function()
 
           ▼ 10:25-10:39: information:
           Try this:
-            trivial
+            [apply] trivial
 
           ▼ 10:25-10:39: information:
           Try this:
-            rfl
+            [apply] rfl
 
           ▼ 10:22-10:39: error:
           unsolved goals

spec/widgets/importgraph_spec.lua

@@ -15,7 +15,7 @@ describe('ImportGraph widgets', function()
     'supports GoToModule links',
     helpers.clean_buffer(
       [[
-        import ImportGraph.Imports
+        import ImportGraph.Meta
         #find_home Nat.add_one
       ]],
       function()