chore(lean): minimize imports in Base/Arith
#328
Draft
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This is a methodology employed by the Mathlib community to improve the build performance of Mathlib. The idea is to exploit the ImportGraph library which has a command `#min_imports` and `#redundant_imports` to figure out what imports to trim down. See: https://reservoir.lean-lang.org/@leanprover-community/importGraph for the docs. This is the result of this process for `Base/Arith`. Signed-off-by: Ryan Lahfa <[email protected]>
Member
|
I think this is a great idea! You don't have to do this for the whole library, but it would be good to document this somewhere, perhaps in the README or in a CONTRIBUTING.md file ? |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This is a methodology employed by the Mathlib community to improve the build performance of Mathlib.
The idea is to exploit the ImportGraph library which has a command
#min_importsand#redundant_importsto figure out what imports to trim down.See: https://reservoir.lean-lang.org/@leanprover-community/importGraph for the docs.
This is the result of this process for
Base/Arith.@sonmarcho If you are happy with the idea, I can minimize the rest of the library. This will be helpful with the documentation PR to minimize the build times as well (as we won't build unnecessary Mathlib modules in Nix).