Bump the Lean versions in CI.

Julian · Feb 5, 2025 · 5cc20fc · 5cc20fc
1 parent e521039
commit 5cc20fc
Show file tree

Hide file tree

Showing 4 changed files with 18 additions and 18 deletions.
diff --git a/demos/project/lake-manifest.json b/demos/project/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "85ca5b28aec713c9007232b98fb92ec2f43a0b5d",
+   "rev": "395bedc10df1587872e3c9d61b0f55284e62dc13",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -15,10 +15,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1622a8693b31523c8f82db48e01b14c74bc1f155",
+   "rev": "59a8514bb0ee5bae2689d8be717b5272c9b3dc1c",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.16.0-rc1",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "18d461b4acad559d6ec11ae42eeed0fe767e523b",
+   "rev": "5013810061a18ca1f5510106172b94c6fbd0a2fc",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,37 +45,37 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "07f60e90998dfd6592688a14cd67bd4e384b77b2",
+   "rev": "8fff3f074da9237cd4e179fd6dd89be6c4022d41",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.50",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "79402ad9ab4be9a2286701a9880697e2351e4955",
+   "rev": "ba9a63be53f16b3b6e4043641c6bad4883e650b4",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.16.0-rc1",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32",
+   "rev": "7b3b0c8327b3c0214ac49ca6d6922edbb81ab8c9",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "66225aab4f6bd1687053b03916105f7cab140507",
+   "rev": "512d7fa38234139a34c04e3b3438fc142b51bbee",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
+   "rev": "a2eb24a3dbf681f2b655f82ba5ee5b139d4a5abc",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

diff --git a/demos/project/lean-toolchain b/demos/project/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.16.0-rc1
+leanprover/lean4:v4.17.0-rc1
diff --git a/spec/fixtures/example-project/lake-manifest.json b/spec/fixtures/example-project/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "18d461b4acad559d6ec11ae42eeed0fe767e523b",
+   "rev": "5013810061a18ca1f5510106172b94c6fbd0a2fc",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,17 +22,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "66225aab4f6bd1687053b03916105f7cab140507",
+   "rev": "512d7fa38234139a34c04e3b3438fc142b51bbee",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.17.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
+   "rev": "a2eb24a3dbf681f2b655f82ba5ee5b139d4a5abc",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

diff --git a/spec/fixtures/example-project/lean-toolchain b/spec/fixtures/example-project/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.16.0-rc1
+leanprover/lean4:v4.17.0-rc1
Original file line number	Diff line number	Diff line change
		@@ -1 +1 @@
		leanprover/lean4:v4.16.0-rc1
		leanprover/lean4:v4.17.0-rc1