Skip to content

feat: shake: make Mathlib-ready #11496

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.

Sign up for GitHub

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

Merged
Kha merged 47 commits into from
Dec 5, 2025
Merged

feat: shake: make Mathlib-ready #11496

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
47 commits
Select commit Hold shift + click to select a range
e849cb8
chore: fix deprecations
Kha Nov 10, 2025
cea2186
feat: allow `module -- shake: keep` to preserve downstream uses
Kha Nov 10, 2025
01b12c3
feat: `--keep-public`
Kha Nov 10, 2025
8a82869
feat: `--add-public`
Kha Nov 10, 2025
d308d5d
fix: do not process modules outside package
Kha Nov 10, 2025
a5c0911
fix: ignore reserved names (until they all become private anyway)
Kha Nov 10, 2025
d178a04
chore: avoid error message
Kha Nov 11, 2025
f03b5be
direct preserve?
Kha Nov 11, 2025
1e6efb2
better ordering
Kha Nov 11, 2025
97d018f
shake: keep-all/downstream
Kha Nov 11, 2025
23561b9
fix addPublic
Kha Nov 12, 2025
dc67759
chore: use `isDeclMeta`
Kha Nov 11, 2025
b1e6e72
fix: isDeclMeta does not cover enough decls
Kha Nov 14, 2025
58fd86d
keep foreign imports
Kha Nov 14, 2025
2e292ce
fix addPublic + preserve
Kha Nov 20, 2025
771614a
fix preserve + `meta`
Kha Nov 20, 2025
d3c7c73
fix minimization of newly added imports, has always been broken?
Kha Nov 20, 2025
d941659
ignore `_simp_`
Kha Nov 21, 2025
762140a
fix --add-public
Kha Nov 21, 2025
060ff8d
fix: shake: only record non-builtin simprocs
Kha Nov 24, 2025
431afc1
merge simp fix
Kha Nov 24, 2025
a61cd2c
do not keep all foreign imports after all, we certainly don't want to…
Kha Nov 24, 2025
f17ea4f
feat: shake: record tactic elaborators
Kha Nov 24, 2025
a83285d
keep aesop?
Kha Nov 24, 2025
dd97cc9
fix: do not remove `import all X` in favor of `public import X`
Kha Nov 24, 2025
32c6781
fix: output ordering
Kha Nov 25, 2025
3398a3c
add `--keep-implied`
Kha Nov 28, 2025
7700f2a
merge upstream/nightly-with-mathlib
Kha Nov 28, 2025
dce62b2
fix: update preserve for extern packages as well
Kha Nov 28, 2025
35f32c6
feat: `--keep-prefix`
Kha Nov 28, 2025
8e11622
feat: `--trace`
Kha Nov 29, 2025
50b85e9
fix keep-prefix
Kha Nov 29, 2025
ee94eae
`public meta` ~> `public` for folder-nested
Kha Nov 29, 2025
b7bc38c
more progress
Kha Nov 29, 2025
0521c57
trace extra rev uses
Kha Nov 29, 2025
229e945
fix folder-nested conversion
Kha Nov 29, 2025
d43f8c6
feat: `recordIndirectModUse`
Kha Nov 30, 2025
96ebe71
refactor: statify
Kha Nov 30, 2025
1408345
calculate indirect uses on shake side
Kha Nov 30, 2025
58ce86f
feat: shake: record `attribute` references
Kha Dec 2, 2025
0fbbbf4
make keep-prefix transitive
Kha Dec 2, 2025
fbbad89
cleanup
Kha Dec 3, 2025
10f4ea1
merge upstream/nightly-with-mathlib
Kha Dec 3, 2025
1916f4d
clean up
Kha Dec 3, 2025
d411d9e
more trace
Kha Dec 4, 2025
4007930
merge upstream/nightly-with-mathlib
Kha Dec 4, 2025
8754f96
fix test
Kha Dec 4, 2025
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
Loading
Loading