-
Notifications
You must be signed in to change notification settings - Fork 251
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
[Merged by Bors] - fix: reduce imports for scripts #6716
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
bors d+
Thanks!
✌️ digama0 can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
As [noted on Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/lake.20exe.20cache.20get.20broken.3F/near/386489865), a from-scratch build of mathlib after `lake exe cache get` will compile all of `Std` due to some unnecessary imports. With a few well chosen import reductions we only end up having to compile ~20 files instead of ~300 files (compile meaning `Compiling`, generating the arch-dependent `.o` files that are not in the cache).
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
As noted on Zulip, a from-scratch build of mathlib after
lake exe cache get
will compile all ofStd
due to some unnecessary imports. With a few well chosen import reductions we only end up having to compile ~20 files instead of ~300 files (compile meaningCompiling
, generating the arch-dependent.o
files that are not in the cache).