Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

chore: adaptations for leanprover/lean4#3756 #765

Draft
wants to merge 373 commits into
base: nightly-testing
Choose a base branch
from
Draft
Changes from 1 commit
Commits
Show all changes
373 commits
Select commit Hold shift + click to select a range
a45defd
chore: compatibility updates for Int migration
joehendrix Feb 16, 2024
c21447f
chore: adaptations for nightly-2024-02-15 (#652)
kim-em Feb 16, 2024
9237675
Merge main into nightly-testing
leanprover-community-mathlib4-bot Feb 16, 2024
edae365
ripping stuff out
kim-em Feb 16, 2024
767f696
merge lean-pr-testing-3364
kim-em Feb 16, 2024
74c7d4e
finished
kim-em Feb 16, 2024
b281189
oops cleanup
kim-em Feb 16, 2024
31d95ec
Merge main into nightly-testing
leanprover-community-mathlib4-bot Feb 16, 2024
601f022
Merge main into nightly-testing
leanprover-community-mathlib4-bot Feb 16, 2024
44f0b92
Merge main into nightly-testing
leanprover-community-mathlib4-bot Feb 16, 2024
426c0f9
update all
kim-em Feb 17, 2024
ce2284e
chore: bump to nightly-2024-02-17
leanprover-community-mathlib4-bot Feb 17, 2024
0f3cc42
Merge main into nightly-testing
leanprover-community-mathlib4-bot Feb 17, 2024
9ce61f1
Merge main into nightly-testing
leanprover-community-mathlib4-bot Feb 17, 2024
db74bfd
Merge main into nightly-testing
leanprover-community-mathlib4-bot Feb 18, 2024
bfa9e08
bump toolchain
kim-em Feb 18, 2024
05a934e
Merge main into nightly-testing
leanprover-community-mathlib4-bot Feb 18, 2024
796408b
Merge main into nightly-testing
leanprover-community-mathlib4-bot Feb 18, 2024
39070b1
Merge main into nightly-testing
leanprover-community-mathlib4-bot Feb 18, 2024
1da1231
Merge main into nightly-testing
leanprover-community-mathlib4-bot Feb 18, 2024
6b45710
Merge main into nightly-testing
leanprover-community-mathlib4-bot Feb 19, 2024
bbf6b59
Merge main into nightly-testing
leanprover-community-mathlib4-bot Feb 19, 2024
c6e95fa
Merge main into nightly-testing
leanprover-community-mathlib4-bot Feb 19, 2024
269beca
chore: bump to nightly-2024-02-19
leanprover-community-mathlib4-bot Feb 19, 2024
fe0a29a
not sure why that proof broke
kim-em Feb 19, 2024
3e4027b
fixes
kim-em Feb 19, 2024
0fc11f3
fix
kim-em Feb 19, 2024
5cb2a58
fixes
kim-em Feb 19, 2024
afdc088
Delete
kim-em Feb 19, 2024
1586642
remove imports
kim-em Feb 19, 2024
c8ada7a
reduce imports
kim-em Feb 20, 2024
6a756a4
merge main
kim-em Feb 20, 2024
5f9deb5
Merge main into nightly-testing
leanprover-community-mathlib4-bot Feb 20, 2024
a1eba7d
Merge remote-tracking branch 'origin/main' into nightly-testing
kim-em Feb 20, 2024
1eb42c7
Merge branch 'nightly-testing' of github.com:leanprover/std4 into nig…
kim-em Feb 20, 2024
cb218dc
Merge remote-tracking branch 'origin/main' into bump/v4.7.0
kim-em Feb 20, 2024
6d2ee66
chore: bump to nightly-2024-02-20
leanprover-community-mathlib4-bot Feb 20, 2024
21e80ab
adaptations for nightly-2024-02-20
kim-em Feb 20, 2024
c939336
fixes
kim-em Feb 20, 2024
652a672
Merge main into nightly-testing
leanprover-community-mathlib4-bot Feb 20, 2024
0b837b3
chore: bump to nightly-2024-02-21
leanprover-community-mathlib4-bot Feb 21, 2024
ef96051
fixes
kim-em Feb 22, 2024
292f8f2
.
kim-em Feb 22, 2024
b997f3f
.
kim-em Feb 22, 2024
cad2a50
fixes
kim-em Feb 22, 2024
f1f0b58
chore: bump to nightly-2024-02-22
leanprover-community-mathlib4-bot Feb 22, 2024
a178ab5
fix
kim-em Feb 22, 2024
dc1b9b4
merge main
kim-em Feb 22, 2024
327fee2
chore: bump to nightly-2024-02-23
leanprover-community-mathlib4-bot Feb 23, 2024
bc54f14
Merge main into nightly-testing
leanprover-community-mathlib4-bot Feb 23, 2024
d7451c6
chore: adaptations for nightly-2024-02-19 (#666)
kim-em Feb 23, 2024
1eef461
chore: bump to nightly-2024-02-24
leanprover-community-mathlib4-bot Feb 24, 2024
79e7958
Merge remote-tracking branch 'origin/main' into bump/v4.7.0
kim-em Feb 25, 2024
aca27e1
adaptations for nightly-2024-02-24
kim-em Feb 25, 2024
43d6686
rename std_apply?
kim-em Feb 25, 2024
4c80d37
fixes
kim-em Feb 25, 2024
58f119a
chore: add test for simultaneous 'import Lean' and 'import Std'
kim-em Feb 25, 2024
4f24443
Merge branch 'import_all' into nightly-testing
kim-em Feb 25, 2024
1910966
updates
kim-em Feb 25, 2024
5a874b1
restore lemma
kim-em Feb 25, 2024
ce0285d
fix bitvec stuff
kim-em Feb 25, 2024
5cda2bc
Merge main into nightly-testing
leanprover-community-mathlib4-bot Feb 25, 2024
b4c07ab
Merge remote-tracking branch 'origin/main' into nightly-testing
kim-em Feb 25, 2024
d6cc703
Merge branch 'nightly-testing' of github.com:leanprover/std4 into nig…
kim-em Feb 25, 2024
6b80b72
Merge main into nightly-testing
leanprover-community-mathlib4-bot Feb 26, 2024
6162096
Merge main into nightly-testing
leanprover-community-mathlib4-bot Feb 26, 2024
ced7701
fix tests
kim-em Feb 26, 2024
c733963
chore: bump to nightly-2024-02-26
leanprover-community-mathlib4-bot Feb 26, 2024
3fdf76f
incomplete fixes
kim-em Feb 26, 2024
faf7129
chore: adaptations for nightly-2024-02-22 (#668)
kim-em Feb 27, 2024
a9af8e1
,
kim-em Feb 27, 2024
4b1c0ce
remove sorries
kim-em Feb 27, 2024
ad10d34
Merge branch 'bump/v4.7.0' of github.com:leanprover/std4 into bump/v4…
kim-em Feb 27, 2024
1e1f991
Merge remote-tracking branch 'origin/main' into bump/v4.7.0
kim-em Feb 27, 2024
c416f40
chore: adaptations for nightly-2024-02-27
kim-em Feb 27, 2024
f9edca7
backport cleanup from bump/nightly-2024-02-27
kim-em Feb 27, 2024
fb65114
chore: bump to nightly-2024-02-28
leanprover-community-mathlib4-bot Feb 28, 2024
026c06b
chore: adaptations for nightly-2024-02-27 (#674)
kim-em Feb 28, 2024
9ec791d
Merge main into nightly-testing
leanprover-community-mathlib4-bot Feb 28, 2024
67ab85e
delete librarySearch test; it's in Lean
kim-em Feb 28, 2024
946e6f8
remove tests already in Lean
kim-em Feb 28, 2024
9a2342b
remove test already moved to Lean
kim-em Feb 28, 2024
a6501ee
migrate tests in https://github.com/leanprover/lean4/pull/3535
kim-em Feb 28, 2024
79c1bcf
Merge main into nightly-testing
leanprover-community-mathlib4-bot Feb 29, 2024
0de6b50
deleted tests upstreamed in https://github.com/leanprover/lean4/pull/…
kim-em Feb 29, 2024
ffd8e69
chore: bump to nightly-2024-02-29
leanprover-community-mathlib4-bot Feb 29, 2024
bb1c3db
Merge main into nightly-testing
leanprover-community-mathlib4-bot Feb 29, 2024
004dcf8
remove upstreamed lemmas
kim-em Feb 29, 2024
6d22f96
fixed
kim-em Feb 29, 2024
e2648a0
oops, omega benchmark regression
kim-em Feb 29, 2024
7179275
remove @[simp] from lemmas simp can prove
kim-em Feb 29, 2024
9d123ff
chore: bump to nightly-2024-03-01
leanprover-community-mathlib4-bot Mar 1, 2024
ff94a57
upstreamed lemmas
kim-em Mar 1, 2024
bafb6c2
lint
kim-em Mar 1, 2024
44c96b4
merge main
kim-em Mar 1, 2024
53641cf
merge bump/v4.7.0
kim-em Mar 1, 2024
f7b73e3
restore one lemma
kim-em Mar 1, 2024
0f56020
chore: bump to nightly-2024-03-02
leanprover-community-mathlib4-bot Mar 2, 2024
d0a9d56
chore: adaptations for nightly-2024-03-01 (#678)
kim-em Mar 2, 2024
8650789
bump/v4.7.0
kim-em Mar 2, 2024
1fc6571
Update lean-toolchain for testing https://github.com/leanprover/lean4…
leanprover-community-mathlib4-bot Mar 4, 2024
86c0e09
fixes
kim-em Mar 4, 2024
f495a4a
Trigger CI for https://github.com/leanprover/lean4/pull/3579
leanprover-community-mathlib4-bot Mar 4, 2024
354e681
fixes
kim-em Mar 4, 2024
d53045b
Merge branch 'lean-pr-testing-3579' of github.com:leanprover/std4 int…
kim-em Mar 4, 2024
fef6851
Trigger CI for https://github.com/leanprover/lean4/pull/3579
leanprover-community-mathlib4-bot Mar 4, 2024
0594498
fix (#680)
Ruben-VandeVelde Mar 4, 2024
253a287
toolchain
kim-em Mar 4, 2024
1c42649
Merge branch 'nightly-testing' of github.com:leanprover/std4 into nig…
kim-em Mar 4, 2024
9baecd6
Update lean-toolchain for testing https://github.com/leanprover/lean4…
leanprover-community-mathlib4-bot Mar 4, 2024
e53c259
chore: bump to nightly-2024-03-05
leanprover-community-mathlib4-bot Mar 5, 2024
d9e573b
upstream lemmas
kim-em Mar 5, 2024
1501a2e
changes to simp normal form
kim-em Mar 5, 2024
bd2ee35
changes to simp
kim-em Mar 5, 2024
ebd8f65
Merge main into nightly-testing
leanprover-community-mathlib4-bot Mar 6, 2024
19d21a2
merge nightly-testing
kim-em Mar 7, 2024
204abb9
chore: bump to nightly-2024-03-07
leanprover-community-mathlib4-bot Mar 7, 2024
b1e4f9f
fix
kim-em Mar 7, 2024
b0616e9
Merge main into nightly-testing
leanprover-community-mathlib4-bot Mar 7, 2024
8740fe4
Merge main into nightly-testing
leanprover-community-mathlib4-bot Mar 7, 2024
22c99b7
chore: bump to nightly-2024-03-08
leanprover-community-mathlib4-bot Mar 8, 2024
9fa2310
chore: bump to nightly-2024-03-09
leanprover-community-mathlib4-bot Mar 9, 2024
dd225d4
chore: fixes
joehendrix Mar 7, 2024
004e8d1
chore: reduce imports
joehendrix Mar 7, 2024
a2a2479
chore: bump to nightly-2024-03-10
leanprover-community-mathlib4-bot Mar 10, 2024
ea0bc70
chore: bump to nightly-2024-03-11
leanprover-community-mathlib4-bot Mar 11, 2024
a0945f0
Trigger CI for https://github.com/leanprover/lean4/pull/3589
leanprover-community-mathlib4-bot Mar 11, 2024
2cd6bbf
fix
kim-em Mar 11, 2024
dafa107
fix tests
kim-em Mar 12, 2024
0936d27
fixes
kim-em Mar 12, 2024
63e50b7
chore: adaptations for nightly-2024-03-11 (#692)
kim-em Mar 12, 2024
0ef13c5
chore: adaptations for nightly-2024-03-12
kim-em Mar 12, 2024
6332027
chore: adaptations for nightly-2024-03-12
kim-em Mar 12, 2024
d273b2f
fix test
kim-em Mar 12, 2024
359d423
merge bump/nightly-2024-03-12
kim-em Mar 12, 2024
a5128fc
chore: adaptations for nightly-2024-03-12 (#693)
kim-em Mar 12, 2024
b963be3
merge nightly-testing-2024-03-12
kim-em Mar 13, 2024
c59e73d
Trigger CI for https://github.com/leanprover/lean4/pull/3579
leanprover-community-mathlib4-bot Mar 13, 2024
e002a96
bump toolchain
kim-em Mar 13, 2024
d2b6687
merge lean-pr-testing-3579
kim-em Mar 13, 2024
576d053
chore: adaptations for nightly-2024-03-13 (#695)
kim-em Mar 13, 2024
707b99b
Merge main into nightly-testing
leanprover-community-mathlib4-bot Mar 14, 2024
b0cb780
Merge main into nightly-testing
leanprover-community-mathlib4-bot Mar 15, 2024
5bcbfa4
chore: bump to nightly-2024-03-15
leanprover-community-mathlib4-bot Mar 15, 2024
c3bbed0
fixes
kim-em Mar 15, 2024
3294e73
fix deprecated code action
kim-em Mar 15, 2024
2c55b6b
check for reserved names in isAutoDecl
kim-em Mar 15, 2024
1411c74
Merge main into nightly-testing
leanprover-community-mathlib4-bot Mar 15, 2024
05f0ca9
chore: bump to nightly-2024-03-16
leanprover-community-mathlib4-bot Mar 16, 2024
ecee90f
chore: bump to nightly-2024-03-17
leanprover-community-mathlib4-bot Mar 17, 2024
85cae1f
Merge main into nightly-testing
leanprover-community-mathlib4-bot Mar 18, 2024
c922570
Merge main into nightly-testing
leanprover-community-mathlib4-bot Mar 18, 2024
c318688
chore: bump to nightly-2024-03-18
leanprover-community-mathlib4-bot Mar 18, 2024
70c816d
fix
kim-em Mar 18, 2024
f56b1f9
merge main
kim-em Mar 18, 2024
972eaa9
Trigger CI for https://github.com/leanprover/lean4/pull/3589
leanprover-community-mathlib4-bot Mar 18, 2024
48ebe8f
chore: bump to nightly-2024-03-19
leanprover-community-mathlib4-bot Mar 19, 2024
f6441c8
Merge main into nightly-testing
leanprover-community-mathlib4-bot Mar 19, 2024
784c0ae
Merge main into nightly-testing
leanprover-community-mathlib4-bot Mar 20, 2024
edb7a9d
fixes
kim-em Mar 20, 2024
976093e
chore: adaptations for nightly-2024-03-19
kim-em Mar 20, 2024
27fa4af
Merge remote-tracking branch 'origin/main' into bump/v4.8.0
kim-em Mar 20, 2024
af5681b
Merge main into nightly-testing
leanprover-community-mathlib4-bot Mar 20, 2024
7084c23
Merge remote-tracking branch 'origin/main' into bump/v4.8.0
kim-em Mar 20, 2024
241c0fa
Merge branch 'bump/v4.8.0' into bump/nightly-2024-03-19
kim-em Mar 20, 2024
3aa0736
Merge branch 'bump/nightly-2024-03-19' into nightly-testing
kim-em Mar 20, 2024
865c48e
fix
kim-em Mar 21, 2024
54afc1e
Merge main into nightly-testing
leanprover-community-mathlib4-bot Mar 21, 2024
df2d21b
Merge main into nightly-testing
leanprover-community-mathlib4-bot Mar 21, 2024
4ccec46
chore: bump to nightly-2024-03-21
leanprover-community-mathlib4-bot Mar 21, 2024
6de82f1
Merge main into nightly-testing
leanprover-community-mathlib4-bot Mar 21, 2024
06a7bcb
Merge main into nightly-testing
leanprover-community-mathlib4-bot Mar 21, 2024
cda53ac
fix
kim-em Mar 22, 2024
44bd9ba
Merge main into nightly-testing
leanprover-community-mathlib4-bot Mar 22, 2024
09e0f3e
Merge main into nightly-testing
leanprover-community-mathlib4-bot Mar 22, 2024
3930d30
Merge main into nightly-testing
leanprover-community-mathlib4-bot Mar 22, 2024
93ed0a8
Merge main into nightly-testing
leanprover-community-mathlib4-bot Mar 22, 2024
702be0d
bump
kim-em Mar 22, 2024
0f0374b
merge lean-pr-testing-3589
kim-em Mar 22, 2024
4dbc8fa
unused variable
kim-em Mar 22, 2024
eadf616
fix test
kim-em Mar 22, 2024
36473ef
fix check_imports script
kim-em Mar 22, 2024
5161bf2
chore: bump to nightly-2024-03-23
leanprover-community-mathlib4-bot Mar 23, 2024
96a5ca9
fix test
kim-em Mar 23, 2024
9a1aa2d
chore: bump to nightly-2024-03-24
leanprover-community-mathlib4-bot Mar 24, 2024
2e31efe
chore: bump to nightly-2024-03-25
leanprover-community-mathlib4-bot Mar 25, 2024
0efce25
Merge main into nightly-testing
leanprover-community-mathlib4-bot Mar 26, 2024
f9dbfb5
bump
kim-em Mar 26, 2024
f274ebd
Merge main into nightly-testing
leanprover-community-mathlib4-bot Mar 26, 2024
e0ab3b1
chore: bump to nightly-2024-03-27
leanprover-community-mathlib4-bot Mar 27, 2024
74f80f5
chore: bump to nightly-2024-03-28
leanprover-community-mathlib4-bot Mar 28, 2024
406fe30
fix: remove upstreamed defs and fix some proofs
joehendrix Mar 28, 2024
1c9e0fb
chore: bump to nightly-2024-03-29
leanprover-community-mathlib4-bot Mar 29, 2024
4ebd51a
Merge main into nightly-testing
leanprover-community-mathlib4-bot Mar 29, 2024
c780117
Merge main into nightly-testing
leanprover-community-mathlib4-bot Mar 29, 2024
aec0741
chore: bump to nightly-2024-03-30
leanprover-community-mathlib4-bot Mar 30, 2024
06f06f9
chore: bump to nightly-2024-04-01
leanprover-community-mathlib4-bot Apr 1, 2024
1838f35
Merge main into nightly-testing
leanprover-community-mathlib4-bot Apr 1, 2024
ebaf319
Merge main into nightly-testing
leanprover-community-mathlib4-bot Apr 1, 2024
3676120
Merge main into nightly-testing
leanprover-community-mathlib4-bot Apr 1, 2024
5bca7bd
Merge main into nightly-testing
leanprover-community-mathlib4-bot Apr 1, 2024
fac121c
chore: bump to nightly-2024-04-02
leanprover-community-mathlib4-bot Apr 2, 2024
0af134a
fixes
kim-em Apr 2, 2024
bbd71a6
Merge main into nightly-testing
leanprover-community-mathlib4-bot Apr 3, 2024
8ac01e7
chore: bump to nightly-2024-04-03
leanprover-community-mathlib4-bot Apr 3, 2024
e0eb309
chore: bump to nightly-2024-04-04
leanprover-community-mathlib4-bot Apr 4, 2024
4d33b75
chore: bump to nightly-2024-04-05
leanprover-community-mathlib4-bot Apr 5, 2024
956e5c6
wip: list migration
joehendrix Mar 29, 2024
f47b0fb
chore: bump to nightly-2024-04-07
leanprover-community-mathlib4-bot Apr 7, 2024
7514475
chore: bump to nightly-2024-04-08
leanprover-community-mathlib4-bot Apr 8, 2024
324d76c
chore: bump to nightly-2024-04-09
leanprover-community-mathlib4-bot Apr 9, 2024
1352583
chore: bump to nightly-2024-04-11
leanprover-community-mathlib4-bot Apr 11, 2024
e9b95dc
chore: bump to nightly-2024-04-12
leanprover-community-mathlib4-bot Apr 12, 2024
36f9315
Merge main into nightly-testing
leanprover-community-mathlib4-bot Apr 12, 2024
e6a371f
chore: bump to nightly-2024-04-13
leanprover-community-mathlib4-bot Apr 13, 2024
9a0a8c9
Merge main into nightly-testing
leanprover-community-mathlib4-bot Apr 13, 2024
146806d
Merge main into nightly-testing
leanprover-community-mathlib4-bot Apr 13, 2024
9fd499b
Merge main into nightly-testing
leanprover-community-mathlib4-bot Apr 13, 2024
7e974b7
Merge main into nightly-testing
leanprover-community-mathlib4-bot Apr 14, 2024
ea64e2b
chore: bump to nightly-2024-04-14
leanprover-community-mathlib4-bot Apr 14, 2024
6fd186c
fix: for lean4#3851 (#741)
kmill Apr 14, 2024
7022446
fix: for std4#727 interacting with lean4#3625
kmill Apr 14, 2024
325d548
Merge main into nightly-testing
leanprover-community-mathlib4-bot Apr 15, 2024
fba4f4a
update to #734
kim-em Apr 15, 2024
f032d36
chore: bump to nightly-2024-04-16
leanprover-community-mathlib4-bot Apr 16, 2024
f612c22
Merge main into nightly-testing
leanprover-community-mathlib4-bot Apr 17, 2024
ffbec9e
Merge main into nightly-testing
leanprover-community-mathlib4-bot Apr 17, 2024
96ab0e6
Merge main into nightly-testing
leanprover-community-mathlib4-bot Apr 17, 2024
5b38c68
Merge main into nightly-testing
leanprover-community-mathlib4-bot Apr 17, 2024
92a9eda
fix
kim-em Apr 17, 2024
7e7cdb7
Merge main into nightly-testing
leanprover-community-mathlib4-bot Apr 17, 2024
d9fed9f
chore: bump to nightly-2024-04-17
leanprover-community-mathlib4-bot Apr 17, 2024
6850c9e
Merge main into nightly-testing
leanprover-community-mathlib4-bot Apr 17, 2024
1ace586
fix imports
kim-em Apr 18, 2024
b684c84
Merge main into nightly-testing
leanprover-community-mathlib4-bot Apr 18, 2024
e2e923c
fix: Data.List.Lemmas shoud import Data.List.Init.Lemmas on nightly-t…
TwoFX Apr 18, 2024
f6fedbb
Merge main into nightly-testing
leanprover-community-mathlib4-bot Apr 18, 2024
d2a064d
Merge main into nightly-testing
leanprover-community-mathlib4-bot Apr 18, 2024
6b9dbea
fix
kim-em Apr 18, 2024
c0de883
chore: bump to nightly-2024-04-19
leanprover-community-mathlib4-bot Apr 19, 2024
3d0b06e
Merge main into nightly-testing
leanprover-community-mathlib4-bot Apr 20, 2024
b7b1a63
fix test
kim-em Apr 20, 2024
3db0ad2
fix test
kim-em Apr 20, 2024
fa755eb
fix tests
kim-em Apr 20, 2024
51b853d
chore: bump to nightly-2024-04-20
leanprover-community-mathlib4-bot Apr 20, 2024
46d1879
chore: bump to nightly-2024-04-21
leanprover-community-mathlib4-bot Apr 21, 2024
48e3619
fix
kim-em Apr 21, 2024
d90cfcd
rest
kim-em Apr 21, 2024
4c85c89
chore: adaptations for leanprover/lean4#3756
FR-vdash-bot Apr 24, 2024
3aec33e
revert
FR-vdash-bot Apr 25, 2024
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
Prev Previous commit
Next Next commit
chore: bump to nightly-2024-04-17
  • Loading branch information
leanprover-community-mathlib4-bot committed Apr 17, 2024

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
commit d9fed9f6d8d15df2aca4d649579fe9b8c2c18a8a
2 changes: 1 addition & 1 deletion lean-toolchain
Original file line number Diff line number Diff line change
@@ -1 +1 @@
leanprover/lean4:nightly-2024-04-16
leanprover/lean4:nightly-2024-04-17