Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
408 commits
Select commit Hold shift + click to select a range
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
e079c31
chore: update bump branch to use nightly-2026-01-26
kim-em Jan 27, 2026
d421f1e
Merge main into nightly-testing
Jan 27, 2026
c38d718
Merge remote-tracking branch 'origin/main' into bump/v4.29.0
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
0d02894
chore: adaptations for nightly-2026-01-27 (#298)
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
10cd774
Merge remote-tracking branch 'upstream/main' into bump/v4.29.0
chenson2018 Jan 29, 2026
3331536
chore: adaptations for nightly-2026-01-28 (#301)
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
bc69900
Merge remote-tracking branch 'origin/main' into bump/v4.29.0
chenson2018 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
dc8e18c
Merge remote-tracking branch 'origin/main' into bump/v4.29.0
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
0241271
chore: adaptations for nightly-2026-01-30 (#307)
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
f9fa00a
chore: adaptations for nightly-2026-01-31 (#309)
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
44e1e02
Auto-resolved conflicts in lean-toolchain and lake-manifest.json
Feb 3, 2026
3615bb3
chore: adaptations for nightly-2026-02-02
Feb 3, 2026
8b9eb9c
chore: adaptations for nightly-2026-02-02 (#315)
Feb 3, 2026
30af7e5
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 4, 2026
d49c166
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 4, 2026
a872c17
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 6, 2026
a0ac7ff
chore: bump to nightly-2026-02-05 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Feb 6, 2026
db264ae
use Lean.Meta.Instances
chenson2018 Feb 6, 2026
4e3ecf7
simp +instances
chenson2018 Feb 6, 2026
443c31e
simp +instances in CslibTests
chenson2018 Feb 6, 2026
5dd1530
Merge remote-tracking branch 'origin/main' into bump/v4.29.0
Feb 6, 2026
2103c21
chore: adaptations for nightly-2026-02-05
Feb 6, 2026
ab85bff
chore: adaptations for nightly-2026-02-05 (#324)
mathlib-nightly-testing[bot] Feb 6, 2026
0458b6e
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 6, 2026
7c79cc4
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 7, 2026
ffc0f7a
chore: bump to nightly-2026-02-10 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Feb 10, 2026
d972e98
Auto-resolved conflicts in lean-toolchain and lake-manifest.json
Feb 10, 2026
66107b5
chore: adaptations for nightly-2026-02-10
Feb 10, 2026
15e6b29
chore: adaptations for nightly-2026-02-10 (#330)
mathlib-nightly-testing[bot] Feb 10, 2026
6f161b8
chore: bump to nightly-2026-02-13-rev2 with mathlib at nightly-testin…
mathlib-nightly-testing[bot] Feb 13, 2026
53e1a01
chore: adaptations for nightly-2026-02-13-rev2
Feb 13, 2026
622d921
chore: adaptations for nightly-2026-02-13-rev2 (#332)
mathlib-nightly-testing[bot] Feb 13, 2026
0a02eb1
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 14, 2026
e21566e
chore: bump to nightly-2026-02-15-rev1 with mathlib at nightly-testin…
mathlib-nightly-testing[bot] Feb 15, 2026
da945d5
Merge remote-tracking branch 'origin/main' into bump/v4.29.0
Feb 15, 2026
41389cc
chore: adaptations for nightly-2026-02-15-rev1
Feb 15, 2026
f2a87d6
chore: adaptations for nightly-2026-02-15-rev1 (#337)
mathlib-nightly-testing[bot] Feb 15, 2026
da8e43e
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 16, 2026
4a56298
chore: bump to nightly-2026-02-16 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Feb 16, 2026
6d00a64
Merge remote-tracking branch 'origin/main' into bump/v4.29.0
Feb 16, 2026
a36a8b0
chore: adaptations for nightly-2026-02-16
Feb 16, 2026
7f01bb9
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 16, 2026
636ded9
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 17, 2026
4b2015a
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 17, 2026
055330f
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 17, 2026
b608dc1
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 18, 2026
89cd513
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 18, 2026
f6e17b7
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 19, 2026
b81084a
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 19, 2026
24e0a5a
manual bump to nightly-2026-02-17
chenson2018 Feb 19, 2026
4cde412
Merge commit '24e0a5a923e24d374f081a586aa1376ed72630b2' into bump/nig…
Feb 19, 2026
2deedee
chore: adaptations for nightly-2026-02-17
Feb 19, 2026
77ae4f0
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 19, 2026
f9ae9ad
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 19, 2026
786de85
chore: bump to nightly-2026-02-19 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Feb 19, 2026
a2e9349
use Lean.isImplicitReducible
chenson2018 Feb 19, 2026
424882b
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 20, 2026
1b8efc1
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 21, 2026
2116efc
chore: bump to nightly-2026-02-21 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Feb 21, 2026
e7ef5bb
Merge commit '2116efc6f5af698bd719929b3c5258b7e68de549' into bump/nig…
Feb 21, 2026
b4f8a0a
chore: adaptations for nightly-2026-02-21
Feb 21, 2026
e78d20c
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 23, 2026
a4559c7
chore: bump to nightly-2026-02-23 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Feb 23, 2026
8994f46
chore: adaptations for nightly-2026-02-23
Feb 23, 2026
c98fb7e
chore: bump to nightly-2026-02-23-rev1 with mathlib at nightly-testin…
mathlib-nightly-testing[bot] Feb 24, 2026
d919360
chore: adaptations for nightly-2026-02-23-rev1
Feb 24, 2026
e519b45
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 24, 2026
e461aa7
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 25, 2026
bf84fd6
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 25, 2026
3e9dded
chore: bump to nightly-2026-02-25 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Feb 27, 2026
6350a88
adaptation for lean4#12603
chenson2018 Feb 27, 2026
216c6fa
chore: adaptations for nightly-2026-02-25
Feb 27, 2026
f6ef535
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 27, 2026
2b18ca3
Merge main into nightly-testing
mathlib-nightly-testing[bot] Feb 28, 2026
70f90c0
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 2, 2026
6ea7b28
manual bump to 2026-03-02
chenson2018 Mar 3, 2026
28bd035
chore: adaptations for nightly-2026-03-02
Mar 3, 2026
d482a77
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 4, 2026
33a2a72
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 5, 2026
112445d
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 5, 2026
6b920b6
chore: bump to nightly-2026-03-05 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Mar 5, 2026
ecc3f0f
chore: adaptations for nightly-2026-03-05
Mar 5, 2026
d2c36fc
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 5, 2026
231c589
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 6, 2026
405ca40
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 9, 2026
06a4567
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 9, 2026
540c985
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 10, 2026
e06c14c
chore: bump to nightly-2026-03-09 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Mar 10, 2026
ab1c7e6
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 10, 2026
9888913
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 12, 2026
89d5477
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 12, 2026
0b924df
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 13, 2026
6e74614
manual update to 2026-03-14
chenson2018 Mar 15, 2026
10a8913
chore: adaptations for nightly-2026-03-14
Mar 15, 2026
bcfd3fb
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 17, 2026
e99b770
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 17, 2026
942e585
chore: bump to nightly-2026-03-17 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Mar 17, 2026
78d22fe
chore: adaptations for nightly-2026-03-17
Mar 17, 2026
6504a8f
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 17, 2026
33144c9
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 17, 2026
f6a4b5b
chore: bump to nightly-2026-03-18 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Mar 18, 2026
b7d8dc6
chore: adaptations for nightly-2026-03-18
Mar 18, 2026
8c9b401
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 19, 2026
71272f9
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 20, 2026
26bac37
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 20, 2026
bf2634f
chore: bump to nightly-2026-03-19 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Mar 20, 2026
c5efbb9
chore: adaptations for nightly-2026-03-19
Mar 20, 2026
ef513f8
chore: bump to nightly-2026-03-19-rev1 with mathlib at nightly-testin…
mathlib-nightly-testing[bot] Mar 22, 2026
0cf95b9
getNamespaceSet -> getNamespaces
chenson2018 Mar 22, 2026
71dc8ea
getNamespaceSet -> getNamespaces
chenson2018 Mar 22, 2026
e137a45
chore: adaptations for nightly-2026-03-19-rev1
Mar 22, 2026
4555ad5
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 23, 2026
a704c17
Merge main into nightly-testing
mathlib-nightly-testing[bot] Mar 24, 2026
cd361c8
chore: bump to nightly-2026-03-24 with mathlib at nightly-testing-202…
mathlib-nightly-testing[bot] Mar 24, 2026
af70787
chore: adaptations for nightly-2026-03-24
Mar 24, 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
16 changes: 8 additions & 8 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": "5a62ef12a14818672c68d9415dc766596d0221c3",
"rev": "0037610a33ecd84750e346a72af0981dd0e71c58",
"name": "mathlib",
"manifestFile": "lake-manifest.json",
"inputRev": "nightly-testing-2026-03-19-rev1",
"inputRev": "nightly-testing-2026-03-24",
"inherited": false,
"configFile": "lakefile.lean"},
{"url": "https://github.com/leanprover-community/plausible",
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "e84e3e16aea6b72cc5d311ca1bb25caad417e162",
"rev": "4d955ffd04d5f6d1143c5bf8fffab59ea7d84595",
"name": "plausible",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand All @@ -35,7 +35,7 @@
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "f207d9fcf0cef00ba79962a33ef156061914d9c7",
"rev": "4270b99dc7c5e90d5ee5c6cb2dd91aaba5b19557",
"name": "importGraph",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
Expand All @@ -55,7 +55,7 @@
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "61944418f2cf5a6d8b217ed2c5ed82a4d9f607b7",
"rev": "2ac0e066410c02c7f755c865c2a4770855d47291",
"name": "aesop",
"manifestFile": "lake-manifest.json",
"inputRev": "nightly-testing",
Expand All @@ -75,7 +75,7 @@
"type": "git",
"subDir": null,
"scope": "leanprover-community",
"rev": "0d632b9bcad639bde7d080c7f4faf676a9d27eb5",
"rev": "81c23850e7c2b5f82ed16e3569def2fe0f52e1c9",
"name": "batteries",
"manifestFile": "lake-manifest.json",
"inputRev": "nightly-testing",
Expand All @@ -85,10 +85,10 @@
"type": "git",
"subDir": null,
"scope": "leanprover",
"rev": "3de531c1135f5e3a01f3ac04830996fda476b28e",
"rev": "33583e6fb5096defc38f0c7f67d1c4a3825aee1f",
"name": "Cli",
"manifestFile": "lake-manifest.json",
"inputRev": "v4.29.0-rc6",
"inputRev": "v4.29.0-rc7",
"inherited": true,
"configFile": "lakefile.toml"}],
"name": "cslib",
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-03-19-rev1"
rev = "nightly-testing-2026-03-24"

[[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-03-19-rev1
leanprover/lean4:nightly-2026-03-24
Loading