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

[Merged by Bors] - chore: don't import Lake under Mathlib #13779

Closed
wants to merge 14 commits into from

Conversation

mattrobball
Copy link
Collaborator

@mattrobball mattrobball commented Jun 12, 2024

The Lake.CLI.Main import was slowing down linting by ~90s/~15% on its own. We move the function getLeanLibs back to scripts/mk_all.lean to avoid the import.


Open in Gitpod

@mattrobball
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 51d110d.
There were significant changes against commit bffb043:

  Benchmark   Metric         Change
  =================================
+ lint        instructions   -12.5%
+ lint        wall-clock     -14.7%

@mattrobball
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 9d4d9e4.
There were significant changes against commit bffb043:

  Benchmark   Metric         Change
  =================================
- build       linting          5.2%
+ lint        instructions   -12.5%
+ lint        wall-clock     -14.6%

@mattrobball
Copy link
Collaborator Author

!bench

@grunweg
Copy link
Collaborator

grunweg commented Jun 13, 2024

Thanks a lot for investigating this - I would have been (and still am) completely stumped by them!

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 87579f6.
There were significant changes against commit bffb043:

  Benchmark   Metric         Change
  =================================
- build       linting          7.2%
+ lint        instructions   -12.5%
+ lint        wall-clock     -13.8%

@mattrobball
Copy link
Collaborator Author

Adding the file to nolints.json with all linters didn't make a difference in the regression

@mattrobball
Copy link
Collaborator Author

Oh wait. I'm reading this wrong. The file itself is fine.

@mattrobball
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit d2f495e.
There were no significant changes against commit bffb043.

@mattrobball
Copy link
Collaborator Author

Until it is added to Mathlib.lean, and then even blacklisting all the linters in nolints.json doesn't help

@mattrobball
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 18cb303.
There were significant changes against commit bffb043:

  Benchmark   Metric    Change
  ============================
- build       linting     6.9%

@mattrobball
Copy link
Collaborator Author

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 9ab3ce4.
There were significant changes against commit bffb043:

  Benchmark   Metric         Change
  =================================
+ lint        instructions   -12.5%
+ lint        wall-clock     -14.7%

@mattrobball
Copy link
Collaborator Author

!bench

Copy link

github-actions bot commented Jun 14, 2024

PR summary 3d9182a4a1

Import changes

Dependency changes

File Base Count Head Count Change
Mathlib.Util.GetAllModules 2 1 -1 (-50.00%)

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@mattrobball mattrobball changed the title Revert "refactor: tweak and move functionality for getting all modules out of scripts (#13339)" chore: don't import Lake under Mathlib Jun 14, 2024
@mattrobball mattrobball requested a review from grunweg June 14, 2024 12:34
@mattrobball mattrobball marked this pull request as ready for review June 14, 2024 12:37
lakefile.lean Outdated Show resolved Hide resolved
Copy link
Collaborator

@grunweg grunweg left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wow, thanks a lot for finding this! As a next step, I'll augment the Python lint to complain about any lake imports in Mathlib, referring to this issue :-)

This PR is just code motion, so looks fine to me. My original use-case #13245 doesn't need getLeanLibs anyway (and its proposed replacement won't either), so moving this function back looks good to me.

@grunweg
Copy link
Collaborator

grunweg commented Jun 14, 2024

Actually, since you marked this as awaiting-review and CI on this was successful previously, let me go straight to
maintainer merge

Copy link

🚀 Pull request has been placed on the maintainer queue by grunweg.

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 16c93ae.
There were significant changes against commit bffb043:

  Benchmark   Metric         Change
  =================================
+ lint        instructions   -12.5%
+ lint        wall-clock     -14.7%

@robertylewis
Copy link
Member

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 14, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 14, 2024
The `Lake.CLI.Main` import was slowing down linting by ~90s/~15% on its own. We move the function `getLeanLibs` back to `scripts/mk_all.lean` to avoid the import. 




Co-authored-by: Matthew Robert Ballard <[email protected]>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jun 14, 2024

Build failed (retrying...):

mathlib-bors bot pushed a commit that referenced this pull request Jun 14, 2024
The `Lake.CLI.Main` import was slowing down linting by ~90s/~15% on its own. We move the function `getLeanLibs` back to `scripts/mk_all.lean` to avoid the import. 




Co-authored-by: Matthew Robert Ballard <[email protected]>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jun 14, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: don't import Lake under Mathlib [Merged by Bors] - chore: don't import Lake under Mathlib Jun 14, 2024
@mathlib-bors mathlib-bors bot closed this Jun 14, 2024
@mathlib-bors mathlib-bors bot deleted the mrb/revert_13339 branch June 14, 2024 16:44
mathlib-bors bot pushed a commit that referenced this pull request Jun 14, 2024
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
The `Lake.CLI.Main` import was slowing down linting by ~90s/~15% on its own. We move the function `getLeanLibs` back to `scripts/mk_all.lean` to avoid the import. 




Co-authored-by: Matthew Robert Ballard <[email protected]>
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
maintainer-merge ready-to-merge This PR has been sent to bors.
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants