chore: bump toolchain to v4.17.0

Author: jcommelin

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.17.0-rc1
+leanprover/lean4:v4.17.0

test/Mathlib/lake-manifest.json

@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "96a5ba5ce504f8b8e6acd659015e46e641d7af10",
+   "rev": "5269898d6a51d047931107c8d72d934d8d5d3753",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.17.0-rc1",
+   "inputRev": "v4.17.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "59a8514bb0ee5bae2689d8be717b5272c9b3dc1c",
+   "rev": "c708be04267e3e995a14ac0d08b1530579c1525a",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531",
+   "rev": "0c169a0d55fef3763cfb3099eafd7b884ec7e41d",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "5013810061a18ca1f5510106172b94c6fbd0a2fc",
+   "rev": "0447b0a7b7f41f0a1749010db3f222e4a96f9d30",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8fff3f074da9237cd4e179fd6dd89be6c4022d41",
+   "rev": "799f6986de9f61b784ff7be8f6a8b101045b8ffd",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v0.0.52",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ba9a63be53f16b3b6e4043641c6bad4883e650b4",
+   "rev": "56a2c80b209c253e0281ac4562a92122b457dcc0",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "b1311119f5f7c79c818d3e06621cc81f4bb8973f",
+   "rev": "95561f7a5811fae6a309e4a1bbe22a0a4a98bf03",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "512d7fa38234139a34c04e3b3438fc142b51bbee",
+   "rev": "efcc7d9bd9936ecdc625baf0d033b60866565cd5",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "a2eb24a3dbf681f2b655f82ba5ee5b139d4a5abc",
+   "rev": "e7fd1a415c80985ade02a021172834ca2139b0ca",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

test/Mathlib/lakefile.toml

@@ -4,7 +4,7 @@ defaultTargets = ["ReplMathlibTests"]
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
-rev = "v4.17.0-rc1"
+rev = "v4.17.0"
 
 [[lean_lib]]
 name = "ReplMathlibTests"

test/Mathlib/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.17.0-rc1
+leanprover/lean4:v4.17.0