Skip to content

Commit

Permalink
chore: bump toolchain to v4.17.0-rc1
Browse files Browse the repository at this point in the history
  • Loading branch information
jcommelin committed Feb 3, 2025
1 parent 44dab9f commit 615b8de
Show file tree
Hide file tree
Showing 3 changed files with 4 additions and 4 deletions.
4 changes: 2 additions & 2 deletions lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -5,10 +5,10 @@
"type": "git",
"subDir": null,
"scope": "",
"rev": "01006c9e86bf9e397c026fef4190478dd1fd897e",
"rev": "512d7fa38234139a34c04e3b3438fc142b51bbee",
"name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.16.0",
"inputRev": "v4.17.0-rc1",
"inherited": false,
"configFile": "lakefile.toml"}],
"name": "aesop",
Expand Down
2 changes: 1 addition & 1 deletion lakefile.toml
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ precompileModules = false # We would like to turn this on, but it breaks the Mat
[[require]]
name = "batteries"
git = "https://github.com/leanprover-community/batteries"
rev = "v4.16.0"
rev = "v4.17.0-rc1"

[[lean_lib]]
name = "Aesop"
Expand Down
2 changes: 1 addition & 1 deletion lean-toolchain
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:v4.16.0
leanprover/lean4:v4.17.0-rc1

0 comments on commit 615b8de

Please sign in to comment.