Skip to content

Commit

Permalink
Update Mathlib version
Browse files Browse the repository at this point in the history
  • Loading branch information
PatrickMassot committed Feb 24, 2025
1 parent e125035 commit 65ea991
Show file tree
Hide file tree
Showing 3 changed files with 16 additions and 16 deletions.
28 changes: 14 additions & 14 deletions lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -5,27 +5,27 @@
"type": "git",
"subDir": null,
"scope": "",
"rev": "a6276f4c6097675b1cf5ebd49b1146b735f38c02",
"rev": "ecd33ba785aacf04b696fd0763a8f51e27197ec9",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.16.0",
"inputRev": "ecd33ba785aacf04b696fd0763a8f51e27197ec9",
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/plausible",
"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",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531",
"rev": "0c169a0d55fef3763cfb3099eafd7b884ec7e41d",
"name": "LeanSearchClient",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand All @@ -35,7 +35,7 @@
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "1a6613663c3eb08c401ce0fd1a408412f2c2321e",
"rev": "461b96f5527089718cb23d3f1fd2960a5d0ff516",
"name": "importGraph",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand All @@ -45,37 +45,37 @@
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "07f60e90998dfd6592688a14cd67bd4e384b77b2",
"rev": "322a050322e97b0a701588d9b1efbe2bee7f8527",
"name": "proofwidgets",
"manifestFile": "lake-manifest.json",
"inputRev": "v0.0.50",
"inputRev": "v0.0.52-pre2",
"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": "01006c9e86bf9e397c026fef4190478dd1fd897e",
"rev": "80520e5834d0d9a2446cb88ea3d2a38a94d2e143",
"name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand All @@ -85,7 +85,7 @@
"type": "git",
"subDir": null,
"scope": "leanprover",
"rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
"rev": "a2eb24a3dbf681f2b655f82ba5ee5b139d4a5abc",
"name": "Cli",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand Down
2 changes: 1 addition & 1 deletion lakefile.toml
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ autoImplicit = true
[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "v4.16.0"
rev = "ecd33ba785aacf04b696fd0763a8f51e27197ec9"

[[lean_lib]]
name = "GlimpseOfLean"
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 65ea991

Please sign in to comment.