Skip to content

Commit ddba321

Browse files
committed
chore: move to v4.9.0-rc1
1 parent 439687b commit ddba321

File tree

4 files changed

+13
-13
lines changed

4 files changed

+13
-13
lines changed

lean-toolchain

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.8.0
1+
leanprover/lean4:v4.9.0-rc1

test/Mathlib/lake-manifest.json

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,31 +1,31 @@
1-
{"version": 7,
1+
{"version": "1.0.0",
22
"packagesDir": ".lake/packages",
33
"packages":
44
[{"url": "https://github.com/leanprover-community/batteries",
55
"type": "git",
66
"subDir": null,
7-
"rev": "551ff2d7dffd7af914cdbd01abbd449fe3e3d428",
7+
"rev": "af2dda22771c59db026c48ac0aabc73b72b7a4de",
88
"name": "batteries",
99
"manifestFile": "lake-manifest.json",
10-
"inputRev": "main",
10+
"inputRev": "nightly-testing",
1111
"inherited": true,
1212
"configFile": "lakefile.lean"},
1313
{"url": "https://github.com/leanprover-community/quote4",
1414
"type": "git",
1515
"subDir": null,
16-
"rev": "53156671405fbbd5402ed17a79bd129b961bd8d6",
16+
"rev": "44f57616b0d9b8f9e5606f2c58d01df54840eba7",
1717
"name": "Qq",
1818
"manifestFile": "lake-manifest.json",
19-
"inputRev": "master",
19+
"inputRev": "nightly-testing",
2020
"inherited": true,
2121
"configFile": "lakefile.lean"},
2222
{"url": "https://github.com/leanprover-community/aesop",
2323
"type": "git",
2424
"subDir": null,
25-
"rev": "53ba96ad7666d4a2515292974631629b5ea5dfee",
25+
"rev": "f744aab6fc4e06553464e6ae66730a3b14b8e615",
2626
"name": "aesop",
2727
"manifestFile": "lake-manifest.json",
28-
"inputRev": "master",
28+
"inputRev": "nightly-testing",
2929
"inherited": true,
3030
"configFile": "lakefile.toml"},
3131
{"url": "https://github.com/leanprover-community/ProofWidgets4",
@@ -49,7 +49,7 @@
4949
{"url": "https://github.com/leanprover-community/import-graph.git",
5050
"type": "git",
5151
"subDir": null,
52-
"rev": "77e081815b30b0d30707e1c5b0c6a6761f7a2404",
52+
"rev": "7983e959f8f4a79313215720de3ef1eca2d6d474",
5353
"name": "importGraph",
5454
"manifestFile": "lake-manifest.json",
5555
"inputRev": "main",
@@ -58,10 +58,10 @@
5858
{"url": "https://github.com/leanprover-community/mathlib4",
5959
"type": "git",
6060
"subDir": null,
61-
"rev": "b5eba595428809e96f3ed113bc7ba776c5f801ac",
61+
"rev": "bbf0d1e39b5faac9276413942ac15bd64de65c1e",
6262
"name": "mathlib",
6363
"manifestFile": "lake-manifest.json",
64-
"inputRev": "v4.8.0",
64+
"inputRev": "master",
6565
"inherited": false,
6666
"configFile": "lakefile.lean"}],
6767
"name": "«repl-mathlib-tests»",

test/Mathlib/lakefile.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ open Lake DSL
33

44
package «repl-mathlib-tests» where
55
-- add package configuration options here
6-
require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "v4.8.0"
6+
require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "master"
77

88
@[default_target]
99
lean_lib «ReplMathlibTests» where

test/Mathlib/lean-toolchain

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
leanprover/lean4:v4.8.0
1+
leanprover/lean4:v4.9.0-rc1

0 commit comments

Comments
 (0)