Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
295 commits
Select commit Hold shift + click to select a range
c9f6083
chore: bump to nightly-2025-11-06 with mathlib at nightly-testing-202…
Nov 6, 2025
1c4e4f2
chore: bump to nightly-2025-11-08 with mathlib at nightly-testing-202…
Nov 8, 2025
d6495ea
Merge main into nightly-testing
Nov 9, 2025
19d2653
chore: bump to nightly-2025-11-10 with mathlib at nightly-testing-202…
Nov 10, 2025
3c0e4f5
more lint changes
chenson2018 Nov 10, 2025
55dd070
chore: bump to nightly-2025-11-11 with mathlib at nightly-testing-202…
Nov 11, 2025
3fa0b55
chore: bump to nightly-2025-11-12 with mathlib at nightly-testing-202…
Nov 12, 2025
f135d38
Merge main into nightly-testing
Nov 12, 2025
c29367b
chore: bump to nightly-2025-11-13 with mathlib at nightly-testing-202…
Nov 13, 2025
e6aebd7
Merge main into nightly-testing
Nov 13, 2025
5e5e0ea
Merge main into nightly-testing
Nov 14, 2025
c41245c
chore: bump to nightly-2025-11-14 with mathlib at nightly-testing-202…
Nov 14, 2025
997971a
Merge main into nightly-testing
Nov 14, 2025
13cdf35
chore: bump to nightly-2025-11-15 with mathlib at nightly-testing-202…
Nov 15, 2025
813cfd3
Merge main into nightly-testing
Nov 15, 2025
bfc69ba
Merge main into nightly-testing
Nov 17, 2025
b367da2
Merge main into nightly-testing
Nov 17, 2025
222d5ab
chore: bump to nightly-2025-11-17 with mathlib at nightly-testing-202…
Nov 17, 2025
0e41c2f
Merge main into nightly-testing
Nov 17, 2025
2d54f98
Merge main into nightly-testing
Nov 18, 2025
520605c
Merge main into nightly-testing
Nov 18, 2025
4142d49
chore: bump to nightly-2025-11-18 with mathlib at nightly-testing-202…
Nov 18, 2025
985f4d5
FinFun grind failure
chenson2018 Nov 19, 2025
72c88be
Merge main into nightly-testing
Nov 19, 2025
3431d10
fix
kim-em Nov 19, 2025
53ba77f
Merge branch 'nightly-testing' of github.com:leanprover/cslib into ni…
kim-em Nov 19, 2025
88a38b0
remove redundant have
kim-em Nov 19, 2025
015da0d
Auto-resolved conflicts in lean-toolchain and lake-manifest.json
Nov 19, 2025
7fab2e7
chore: adaptations for nightly-2025-11-18
Nov 19, 2025
e3ff8df
Merge main into nightly-testing
Nov 19, 2025
72b08bc
Merge main into nightly-testing
Nov 19, 2025
02067a4
Merge main into nightly-testing
Nov 19, 2025
094eb8a
chore: bump to nightly-2025-11-20 with mathlib at nightly-testing-202…
Nov 20, 2025
3c82c96
destructuring needed in map_val_mem
chenson2018 Nov 20, 2025
534e652
unused variable
chenson2018 Nov 20, 2025
8ce06df
linter
chenson2018 Nov 20, 2025
eee9160
Merge main into nightly-testing
Nov 20, 2025
9050896
lean-toolchain
kim-em Nov 20, 2025
b030a4f
Merge main into nightly-testing
Nov 21, 2025
afaea48
lint
chenson2018 Nov 21, 2025
8b4ede2
Merge remote-tracking branch 'origin/main' into bump/v4.27.0
Nov 21, 2025
4ab93be
chore: adaptations for nightly-2025-11-20
Nov 21, 2025
9de9d9d
Merge branch 'bump/nightly-2025-11-20' into nightly-testing
Nov 21, 2025
5287af4
chore: adaptations for nightly-2025-11-20 (#175)
Nov 21, 2025
81ad2f2
chore: bump to nightly-2025-11-21 with mathlib at nightly-testing-202…
Nov 21, 2025
face112
Merge main into nightly-testing
Nov 22, 2025
1fbde58
conflict in lakefile
chenson2018 Nov 22, 2025
0dbb129
chore: adaptations for nightly-2025-11-21
chenson2018 Nov 22, 2025
53e2996
chore: adaptations for nightly-2025-11-21 (#177)
chenson2018 Nov 22, 2025
1346cb3
chore: adaptations for nightly-2025-11-21
kim-em Nov 23, 2025
6fc78ed
merge
kim-em Nov 23, 2025
6c09734
chore: adaptations for nightly-2025-11-21
kim-em Nov 23, 2025
9feef00
Merge branch 'bump/nightly-2025-11-21' into nightly-testing
kim-em Nov 23, 2025
9d3430a
chore: adaptations for nightly-2025-11-21 (#179)
kim-em Nov 23, 2025
94fcc38
chore: bump to nightly-2025-11-23 with mathlib at nightly-testing-202…
Nov 23, 2025
668b7d3
lint, make a proof explicit
chenson2018 Nov 23, 2025
0ca986f
Merge main into nightly-testing
Nov 24, 2025
5bcbb84
Merge remote-tracking branch 'origin/main' into bump/v4.27.0
Nov 24, 2025
d8b5872
chore: adaptations for nightly-2025-11-23
Nov 24, 2025
468cfbe
Merge branch 'bump/nightly-2025-11-23' into nightly-testing
Nov 24, 2025
ef2bdcf
chore: adaptations for nightly-2025-11-23 (#182)
Nov 24, 2025
8bf8c91
chore: bump to nightly-2025-11-24 with mathlib at nightly-testing-202…
Nov 24, 2025
c39aa90
chore: adaptations for nightly-2025-11-24
Nov 24, 2025
062288d
chore: adaptations for nightly-2025-11-24 (#183)
Nov 24, 2025
e6609ae
chore: bump to nightly-2025-11-25 with mathlib at nightly-testing-202…
Nov 25, 2025
9792c2a
Merge main into nightly-testing
Nov 27, 2025
82f9811
chore: bump to nightly-2025-11-27 with mathlib at nightly-testing-202…
Nov 28, 2025
2165ef3
linter
chenson2018 Nov 28, 2025
cbca973
shake
chenson2018 Nov 28, 2025
991b29d
Merge remote-tracking branch 'origin/main' into bump/v4.27.0
Nov 28, 2025
72275af
chore: adaptations for nightly-2025-11-27
Nov 28, 2025
0c679d6
chore: adaptations for nightly-2025-11-27 (#190)
Nov 28, 2025
143dd61
Merge main into nightly-testing
Nov 28, 2025
7b57d7c
Merge main into nightly-testing
Nov 29, 2025
5b9ea98
chore: bump to nightly-2025-12-01 with mathlib at nightly-testing-202…
Dec 1, 2025
2feaf8c
disable unusedDecidableInType linter in files using free_union
chenson2018 Dec 1, 2025
0e83cad
Merge remote-tracking branch 'origin/main' into bump/v4.27.0
Dec 1, 2025
384dcd5
chore: adaptations for nightly-2025-12-01
Dec 1, 2025
9302029
chore: adaptations for nightly-2025-12-01 (#193)
Dec 1, 2025
ee3eb3c
chore: bump to nightly-2025-12-04 with mathlib at nightly-testing-202…
Dec 4, 2025
f18d242
Merge remote-tracking branch 'origin/main' into bump/v4.27.0
Dec 4, 2025
2ad15dc
chore: adaptations for nightly-2025-12-04
Dec 4, 2025
c04534c
chore: adaptations for nightly-2025-12-04 (#197)
Dec 4, 2025
71d7f40
Merge main into nightly-testing
Dec 4, 2025
c8f3a75
chore: bump to nightly-2025-12-05 with mathlib at nightly-testing-202…
Dec 5, 2025
63d6f77
Merge remote-tracking branch 'origin/main' into bump/v4.27.0
Dec 5, 2025
93c5502
chore: adaptations for nightly-2025-12-05
Dec 5, 2025
30b9c10
chore: adaptations for nightly-2025-12-05 (#200)
Dec 5, 2025
4484b77
Merge main into nightly-testing
Dec 5, 2025
e0044ef
Merge main into nightly-testing
Dec 6, 2025
bad48f8
chore: bump to nightly-2025-12-07 with mathlib at nightly-testing-202…
Dec 7, 2025
2501a6c
Merge remote-tracking branch 'origin/main' into bump/v4.27.0
Dec 7, 2025
808dbc3
chore: adaptations for nightly-2025-12-07
Dec 7, 2025
2a6287a
chore: adaptations for nightly-2025-12-07 (#204)
Dec 7, 2025
162fdf5
chore: bump to nightly-2025-12-08 with mathlib at nightly-testing-202…
Dec 8, 2025
4f8f0d4
chore: adaptations for nightly-2025-12-08
Dec 8, 2025
2323933
chore: adaptations for nightly-2025-12-08 (#205)
Dec 8, 2025
c173c07
chore: bump to nightly-2025-12-09 with mathlib at nightly-testing-202…
Dec 9, 2025
779f68d
chore: bump to nightly-2025-12-10 with mathlib at nightly-testing-202…
Dec 10, 2025
94fa520
Merge main into nightly-testing
Dec 10, 2025
9cfb7d3
chore: fix failures caused by PR mathlib#31247 (#209)
ctchou Dec 11, 2025
f4c21d2
Merge remote-tracking branch 'origin/main' into bump/v4.27.0
Dec 11, 2025
aa52a60
chore: adaptations for nightly-2025-12-10
Dec 11, 2025
9387773
Merge main into nightly-testing
Dec 13, 2025
e3aaeb1
Merge main into nightly-testing
Dec 13, 2025
3d53956
chore: bump to nightly-2025-12-14 with mathlib at nightly-testing-202…
Dec 14, 2025
8f9851c
chore: update bump branch to nightly-2025-12-14 and mathlib master
kim-em Dec 14, 2025
f790789
Merge main into nightly-testing
Dec 14, 2025
757e35e
chore: adaptations for nightly-2025-12-14
Dec 14, 2025
0ee5076
Merge branch 'bump/nightly-2025-12-14' into nightly-testing
Dec 14, 2025
7245106
chore: adaptations for nightly-2025-12-14 (#219)
Dec 15, 2025
d7ddd27
Merge main into nightly-testing
Dec 15, 2025
b17e81b
chore: bump to nightly-2025-12-15 with mathlib at nightly-testing-202…
Dec 15, 2025
6780328
chore: adaptations for nightly-2025-12-15
Dec 15, 2025
3932b35
Merge remote-tracking branch 'origin/main' into bump/v4.28.0
Dec 15, 2025
c896b05
Merge main into nightly-testing
Dec 15, 2025
faac46f
chore: adaptations for nightly-2025-12-15 (#222)
Dec 15, 2025
8f280a0
Merge main into nightly-testing
Dec 16, 2025
c194385
Merge main into nightly-testing
Dec 16, 2025
47e3632
chore: bump to nightly-2025-12-16 with mathlib at nightly-testing-202…
Dec 16, 2025
cbc77d4
Merge remote-tracking branch 'origin/main' into bump/v4.28.0
Dec 16, 2025
4d0ffd4
chore: adaptations for nightly-2025-12-16
Dec 16, 2025
b8ccdfe
chore: adaptations for nightly-2025-12-16 (#226)
Dec 16, 2025
bfeaff1
Merge main into nightly-testing
Dec 17, 2025
6296f6c
chore: bump to nightly-2025-12-17 with mathlib at nightly-testing-202…
Dec 17, 2025
389b887
Merge remote-tracking branch 'origin/main' into bump/v4.28.0
Dec 17, 2025
53e051b
chore: adaptations for nightly-2025-12-17
Dec 17, 2025
0dd3422
chore: adaptations for nightly-2025-12-17 (#228)
Dec 18, 2025
f549e65
Merge main into nightly-testing
Dec 18, 2025
b43b1a5
Merge main into nightly-testing
Dec 19, 2025
2cde5db
chore: bump to nightly-2025-12-21 with mathlib at nightly-testing-202…
Dec 21, 2025
c1881d5
deprecations
chenson2018 Dec 21, 2025
ed6795c
grind lints
chenson2018 Dec 21, 2025
925f3a8
Merge remote-tracking branch 'origin/main' into bump/v4.28.0
Dec 21, 2025
88421bd
chore: adaptations for nightly-2025-12-21
Dec 21, 2025
99ef1fe
chore: adaptations for nightly-2025-12-21 (#233)
Dec 21, 2025
8f7cd9d
Merge main into nightly-testing
Dec 21, 2025
b3e25e1
chore: bump to nightly-2025-12-22 with mathlib at nightly-testing-202…
Dec 22, 2025
aa715b3
Merge remote-tracking branch 'origin/main' into bump/v4.28.0
Dec 22, 2025
aa7c4a3
chore: adaptations for nightly-2025-12-22
Dec 22, 2025
84ba53f
chore: adaptations for nightly-2025-12-22 (#235)
Dec 22, 2025
ebd7fc4
Merge main into nightly-testing
Dec 23, 2025
82dbf5b
Merge main into nightly-testing
Dec 23, 2025
b18ce61
chore: bump to nightly-2025-12-25 with mathlib at nightly-testing-202…
Dec 25, 2025
76be862
Merge remote-tracking branch 'origin/main' into bump/v4.28.0
Dec 25, 2025
5de1340
chore: adaptations for nightly-2025-12-25
Dec 25, 2025
16a87a4
chore: adaptations for nightly-2025-12-25 (#238)
Dec 25, 2025
a08f14f
Merge main into nightly-testing
Dec 31, 2025
3665faa
chore: bump to nightly-2026-01-02 with mathlib at nightly-testing-202…
Jan 3, 2026
d5f276f
use meta for env_linter
chenson2018 Jan 3, 2026
9f82b33
deprecated IsSymm
chenson2018 Jan 3, 2026
7756e70
Merge remote-tracking branch 'origin/main' into bump/v4.28.0
Jan 3, 2026
6c25080
chore: adaptations for nightly-2026-01-02
Jan 3, 2026
9e40afa
chore: adaptations for nightly-2026-01-02 (#242)
Jan 3, 2026
5b07be4
chore: bump to nightly-2026-01-05 with mathlib at nightly-testing-202…
Jan 5, 2026
483eb75
chore: adaptations for nightly-2026-01-05
Jan 5, 2026
c26d2dd
chore: adaptations for nightly-2026-01-05 (#244)
Jan 5, 2026
ea30ad5
Merge main into nightly-testing
Jan 6, 2026
fe78420
chore: bump to nightly-2026-01-06 with mathlib at nightly-testing-202…
Jan 6, 2026
4f9d91e
Merge remote-tracking branch 'origin/main' into bump/v4.28.0
Jan 6, 2026
c4258ab
chore: adaptations for nightly-2026-01-06
Jan 6, 2026
a0d656a
chore: adaptations for nightly-2026-01-06 (#246)
Jan 6, 2026
77217eb
chore: bump to nightly-2026-01-07 with mathlib at nightly-testing-202…
Jan 7, 2026
4d4835a
chore: adaptations for nightly-2026-01-07
Jan 7, 2026
f64a2bc
chore: adaptations for nightly-2026-01-07 (#248)
Jan 7, 2026
6ac7eb4
chore: bump to nightly-2026-01-08 with mathlib at nightly-testing-202…
Jan 8, 2026
6e98fe8
chore: adaptations for nightly-2026-01-08
Jan 8, 2026
bb479b5
chore: adaptations for nightly-2026-01-08 (#251)
Jan 8, 2026
e866484
Merge main into nightly-testing
Jan 8, 2026
d835455
Merge main into nightly-testing
Jan 9, 2026
6ae9f25
chore: bump to nightly-2026-01-09 with mathlib at nightly-testing-202…
Jan 9, 2026
64b6448
Merge remote-tracking branch 'origin/main' into bump/v4.28.0
Jan 9, 2026
fc194b7
chore: adaptations for nightly-2026-01-09
Jan 9, 2026
b085d16
chore: adaptations for nightly-2026-01-09 (#254)
Jan 9, 2026
9bab47b
chore: bump to nightly-2026-01-10 with mathlib at nightly-testing-202…
Jan 10, 2026
6d0c11d
chore: adaptations for nightly-2026-01-10
Jan 10, 2026
4d974ed
chore: adaptations for nightly-2026-01-10 (#257)
Jan 10, 2026
567a009
chore: bump to nightly-2026-01-11 with mathlib at nightly-testing-202…
Jan 11, 2026
dbfe5a2
chore: adaptations for nightly-2026-01-11
Jan 11, 2026
d07755e
chore: adaptations for nightly-2026-01-11 (#259)
Jan 11, 2026
1ac8c63
chore: bump to nightly-2026-01-12 with mathlib at nightly-testing-202…
Jan 12, 2026
85b5f56
chore: adaptations for nightly-2026-01-12
Jan 12, 2026
2e06c5b
chore: adaptations for nightly-2026-01-12 (#262)
Jan 12, 2026
b278f59
Merge main into nightly-testing
Jan 12, 2026
9766a3e
module system changes
chenson2018 Jan 12, 2026
76f5bb2
shake: keep-all for mk_all
chenson2018 Jan 12, 2026
79ab0c5
chore: bump to nightly-2026-01-14 with mathlib at nightly-testing-202…
Jan 14, 2026
d56559c
Merge remote-tracking branch 'origin/main' into bump/v4.28.0
Jan 14, 2026
ace2fae
chore: adaptations for nightly-2026-01-14
Jan 14, 2026
35febd5
chore: adaptations for nightly-2026-01-14 (#266)
Jan 14, 2026
fb8fa1c
Merge main into nightly-testing
Jan 15, 2026
fccefe1
Merge main into nightly-testing
Jan 16, 2026
fdc3677
chore: bump to nightly-2026-01-20 with mathlib at nightly-testing-202…
Jan 20, 2026
5fae006
unset linter.unusedFintypeInType linter
chenson2018 Jan 20, 2026
78774f3
Merge remote-tracking branch 'origin/main' into bump/v4.28.0
Jan 20, 2026
3b9d509
chore: adaptations for nightly-2026-01-20
Jan 20, 2026
321d5f9
chore: adaptations for nightly-2026-01-20 (#271)
Jan 20, 2026
b505ad0
Merge main into nightly-testing
Jan 20, 2026
31e54a7
chore: bump to nightly-2026-01-21 with mathlib at nightly-testing-202…
Jan 21, 2026
f0559bf
Merge remote-tracking branch 'origin/main' into bump/v4.28.0
Jan 21, 2026
73478c3
chore: adaptations for nightly-2026-01-21
Jan 21, 2026
e3b061b
chore: adaptations for nightly-2026-01-21 (#274)
Jan 21, 2026
296fafb
Merge main into nightly-testing
Jan 22, 2026
bc02831
chore: bump to nightly-2026-01-22 with mathlib at nightly-testing-202…
Jan 22, 2026
1fb2f03
Merge remote-tracking branch 'origin/main' into bump/v4.28.0
Jan 22, 2026
bdaa9ee
chore: adaptations for nightly-2026-01-22
Jan 22, 2026
b57c28d
chore: adaptations for nightly-2026-01-22 (#279)
Jan 22, 2026
6e509bc
Merge main into nightly-testing
Jan 22, 2026
ef39e81
Merge main into nightly-testing
Jan 23, 2026
335696f
Merge main into nightly-testing
Jan 23, 2026
d0f46a8
grind_lint
chenson2018 Jan 23, 2026
1817f26
chore: bump to nightly-2026-01-23 with mathlib at nightly-testing-202…
Jan 23, 2026
158eb85
Merge remote-tracking branch 'origin/main' into bump/v4.28.0
Jan 23, 2026
f501154
chore: adaptations for nightly-2026-01-23
Jan 23, 2026
3f6f6bd
Merge main into nightly-testing
Jan 23, 2026
285934d
Merge main into nightly-testing
Jan 24, 2026
d8869e6
chore: bump to nightly-2026-01-24 with mathlib at nightly-testing-202…
Jan 24, 2026
527ad63
Merge main into nightly-testing
Jan 24, 2026
67cb097
Merge main into nightly-testing
Jan 25, 2026
70bb0ac
Merge main into nightly-testing
Jan 26, 2026
75b1fd5
Merge main into nightly-testing
Jan 26, 2026
220c9b7
Merge main into nightly-testing
Jan 27, 2026
d421f1e
Merge main into nightly-testing
Jan 27, 2026
d8b2c44
chore: adaptations for nightly-2026-01-24
Jan 27, 2026
a1879e5
Merge branch 'bump/nightly-2026-01-24' into nightly-testing
Jan 27, 2026
36b466b
chore: bump to nightly-2026-01-27 with mathlib at nightly-testing-202…
Jan 27, 2026
f5c0726
chore: adaptations for nightly-2026-01-27
Jan 27, 2026
f577301
Merge main into nightly-testing
Jan 27, 2026
21bf1a6
chore: bump to nightly-2026-01-28 with mathlib at nightly-testing-202…
Jan 28, 2026
f32f068
Merge main into nightly-testing
Jan 29, 2026
778a971
one of the grind failures
chenson2018 Jan 29, 2026
62ef529
another grind failure
chenson2018 Jan 29, 2026
4a4d11a
Merge main into nightly-testing
Jan 29, 2026
8f10482
Merge main into nightly-testing
Jan 29, 2026
1f95e11
chore: bump to nightly-2026-01-30 with mathlib at nightly-testing-202…
Jan 30, 2026
fc3b93d
feat: add linear logic tests/benchmark (#302)
arademaker Jan 30, 2026
473375c
chore: simplify the connection between `HasFresh` and `Infinite` (#303)
chenson2018 Jan 30, 2026
5829d7b
chore: adaptations for nightly-2026-01-30
Jan 30, 2026
d638107
Merge branch 'bump/nightly-2026-01-30' into nightly-testing
Jan 30, 2026
1e33a08
one adaptation note fixed by main
chenson2018 Jan 30, 2026
cc1df00
chore: adaptations for nightly-2026-01-30
Jan 30, 2026
0af8ac9
Merge branch 'bump/nightly-2026-01-30' into nightly-testing
Jan 30, 2026
2663b63
chore: adaptations for nightly-2026-01-30
Jan 30, 2026
ad76b37
Merge branch 'bump/nightly-2026-01-30' into nightly-testing
Jan 30, 2026
e74578e
chore: bump to nightly-2026-01-31 with mathlib at nightly-testing-202…
Jan 31, 2026
c8d97c0
chore: adaptations for nightly-2026-01-31
Jan 31, 2026
faac567
Merge main into nightly-testing
Feb 1, 2026
d97ce93
chore: bump to nightly-2026-02-02 with mathlib at nightly-testing-202…
Feb 2, 2026
8782cdf
Merge main into nightly-testing
Feb 3, 2026
3615bb3
chore: adaptations for nightly-2026-02-02
Feb 3, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 5 additions & 5 deletions lake-manifest.json
Original file line number Diff line number Diff line change
Expand Up @@ -5,17 +5,17 @@
"type": "git",
"subDir": null,
"scope": "",
"rev": "a4ea915119d17bf47e9e43d27e163ad5ce9ec4d3",
"rev": "390c30bffcb2ad54f411853020617b8f99e2dd0f",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": "nightly-testing-2026-01-31",
"inputRev": "nightly-testing-2026-02-02",
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/plausible",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "ca46151b876597b20728bd65794928efda180d13",
"rev": "def0c628f155ea883ec84293df09d906eebbf363",
"name": "plausible",
"manifestFile": "lake-manifest.json",
"inputRev": "nightly-testing",
Expand All @@ -35,7 +35,7 @@
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "25b1494bbf3663d3418ef81918af8ec3b000cf54",
"rev": "9b261819fd5d669220cb6694d62ead0dfca1fb9d",
"name": "importGraph",
"manifestFile": "lake-manifest.json",
"inputRev": "nightly-testing",
Expand Down Expand Up @@ -75,7 +75,7 @@
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "9fae711bbe5f3c20d78f54204c3c6e6b37cbb37d",
"rev": "593b0ee5e468f94e284084b109332932d70f2eb8",
"name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "nightly-testing",
Expand Down
2 changes: 1 addition & 1 deletion lakefile.toml
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ weak.linter.allScriptsDocumented = false
[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4-nightly-testing"
rev = "nightly-testing-2026-01-31"
rev = "nightly-testing-2026-02-02"

[[lean_lib]]
name = "Cslib"
Expand Down
2 changes: 1 addition & 1 deletion lean-toolchain
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:nightly-2026-01-31
leanprover/lean4:nightly-2026-02-02