Skip to content

[Merged by Bors] - chore(LongestPole): private an import to reduce the rebuild pole#39609

Closed
b-mehta wants to merge 6 commits into
leanprover-community:masterfrom
b-mehta:test-pole
Closed

[Merged by Bors] - chore(LongestPole): private an import to reduce the rebuild pole#39609
b-mehta wants to merge 6 commits into
leanprover-community:masterfrom
b-mehta:test-pole

Conversation

@b-mehta

@b-mehta b-mehta commented May 20, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

The aim of this PR is to make tweaks to imports to make the rebuild time shorter by making more use of the module system. This is measured in the "lakeprof" report in the radar: https://speed.lean-lang.org/mathlib4-out/396c763262259f066f3837c32643dd752994ca6d/
The first block shows the longest pole when building mathlib, and the second shows it when a rebuild occurs; and as a result of this PR, the relative difference is increased by quite a bit. Note that the "lakeprof/longest rebuild path//wall-clock" is somewhat noisy, but the relative difference should be measured with somewhat less noise.

This was done manually, by taking the second-slowest file in the rebuild path, and tweaking imports around it.

Open in Gitpod

@b-mehta b-mehta added the awaiting-bench This PR needs to be benchmarked before merging label May 20, 2026
@b-mehta

b-mehta commented May 20, 2026

Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar

leanprover-radar commented May 20, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for dccd48f against 260979c are in. No significant results found. @b-mehta

  • 🟥 build//instructions: +40.2G (+0.02%)

Small changes (2🟥)

  • 🟥 build//wall-clock: +6s (+1.20%)
  • 🟥 build/profile/import//wall-clock: +1m 33s (+1.35%)

@github-actions github-actions Bot added the t-analysis Analysis (normed *, calculus) label May 20, 2026
@github-actions

github-actions Bot commented May 20, 2026 •
edited
Loading

Copy link
Copy Markdown

PR summary 626240c7a9

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

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

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.
No changes to weak technical debt.

@b-mehta

b-mehta commented May 20, 2026

Copy link
Copy Markdown
Contributor Author

!radar

@leanprover-radar

leanprover-radar commented May 20, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for 1fa69ac against 260979c are in. No significant results found. @b-mehta

  • 🟥 build//instructions: +44.2G (+0.03%)

Small changes (2🟥)

  • 🟥 build/module/Mathlib.Analysis.Distribution.TemperateGrowth//instructions: +2.0G (+2.84%)
  • 🟥 build/profile/import//wall-clock: +1m 41s (+1.47%)

@b-mehta

b-mehta commented May 20, 2026

Copy link
Copy Markdown
Contributor Author

!radar

@leanprover-radar

leanprover-radar commented May 20, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for 9347371 against 260979c are in. No significant results found. @b-mehta

  • 🟥 build//instructions: +37.2G (+0.02%)

Small changes (1🟥)

  • 🟥 build/module/Mathlib.Analysis.Distribution.TemperateGrowth//instructions: +2.0G (+2.88%)

@b-mehta

b-mehta commented May 20, 2026

Copy link
Copy Markdown
Contributor Author

!radar

@leanprover-radar

leanprover-radar commented May 20, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for 9fe1db7 against 260979c are in. No significant results found. @b-mehta

  • 🟥 build//instructions: +44.8G (+0.03%)

Small changes (1✅, 2🟥)

  • ✅ build/lakeprof/longest rebuild path//wall-clock: -24s (-4.57%)
  • 🟥 build/module/Mathlib.Analysis.Distribution.TemperateGrowth//instructions: +2.1G (+3.01%)
  • 🟥 build/profile/import//wall-clock: +1m 39s (+1.44%)

@b-mehta

b-mehta commented May 20, 2026

Copy link
Copy Markdown
Contributor Author

!radar

@leanprover-radar

leanprover-radar commented May 20, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for 396c763 against 260979c are in. No significant results found. @b-mehta

  • 🟥 build//instructions: +36.6G (+0.02%)

Small changes (1✅, 3🟥)

  • 🟥 build//wall-clock: +6s (+1.18%)
  • ✅ build/lakeprof/longest rebuild path//wall-clock: -20s (-3.71%)
  • 🟥 build/module/Mathlib.Analysis.Distribution.TemperateGrowth//instructions: +2.0G (+2.87%)
  • 🟥 build/profile/import//wall-clock: +1m 44s (+1.51%)

grunweg
grunweg reviewed May 22, 2026
View reviewed changes

@grunweg grunweg left a comment

Copy link
Copy Markdown
Contributor

Choose a reason for hiding this comment

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

LGTM with nits addressed; thanks for doing this!

Comment thread Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean
Comment thread Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean Outdated
Comment thread Mathlib/Analysis/Distribution/TemperateGrowth.lean Outdated
Comment thread Mathlib/Analysis/SpecialFunctions/Gaussian/PoissonSummation.lean Outdated
Comment thread Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean Outdated
@grunweg grunweg added tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip awaiting-author A reviewer has asked the author a question or requested changes. labels May 22, 2026
@grunweg grunweg self-assigned this May 22, 2026
b-mehta
b-mehta commented May 22, 2026
View reviewed changes

@b-mehta b-mehta left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

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

Some of the imports in these files were already not ordered, so I have adjusted those too.

@b-mehta b-mehta removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 22, 2026
@b-mehta
b-mehta requested a review from grunweg May 22, 2026 15:14
@grunweg grunweg removed the awaiting-bench This PR needs to be benchmarked before merging label May 22, 2026
@grunweg

grunweg commented May 22, 2026

Copy link
Copy Markdown
Contributor

Thanks for doing this; LGTM!
bors merge

mathlib-bors Bot pushed a commit that referenced this pull request May 22, 2026
@b-mehta
chore(LongestPole): private an import to reduce the rebuild pole (#39609
5032702 
)

The aim of this PR is to make tweaks to imports to make the *rebuild* time shorter by making more use of the module system. This is measured in the "lakeprof" report in the radar: https://speed.lean-lang.org/mathlib4-out/396c763262259f066f3837c32643dd752994ca6d/
The first block shows the longest pole when building mathlib, and the second shows it when a rebuild occurs; and as a result of this PR, the relative difference is increased by quite a bit. Note that the "lakeprof/longest rebuild path//wall-clock" is somewhat noisy, but the relative difference should be measured with somewhat less noise.

This was done manually, by taking the second-slowest file in the rebuild path, and tweaking imports around it.
@mathlib-triage mathlib-triage Bot added the ready-to-merge This PR has been sent to bors. label May 22, 2026
@mathlib-bors

mathlib-bors Bot commented May 22, 2026

Copy link
Copy Markdown
Contributor

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors Bot changed the title chore(LongestPole): private an import to reduce the rebuild pole [Merged by Bors] - chore(LongestPole): private an import to reduce the rebuild pole May 22, 2026
@mathlib-bors mathlib-bors Bot closed this May 22, 2026
@b-mehta
b-mehta deleted the test-pole branch May 22, 2026 17:02
RaggedR pushed a commit to RaggedR/mathlib4 that referenced this pull request May 24, 2026
@b-mehta @RaggedR
chore(LongestPole): private an import to reduce the rebuild pole (lea…
8a1b0d1 
…nprover-community#39609)

The aim of this PR is to make tweaks to imports to make the *rebuild* time shorter by making more use of the module system. This is measured in the "lakeprof" report in the radar: https://speed.lean-lang.org/mathlib4-out/396c763262259f066f3837c32643dd752994ca6d/
The first block shows the longest pole when building mathlib, and the second shows it when a rebuild occurs; and as a result of this PR, the relative difference is increased by quite a bit. Note that the "lakeprof/longest rebuild path//wall-clock" is somewhat noisy, but the relative difference should be measured with somewhat less noise.

This was done manually, by taking the second-slowest file in the rebuild path, and tweaking imports around it.
b-mehta added a commit to b-mehta/mathlib4 that referenced this pull request Jun 2, 2026
@b-mehta
chore(LongestPole): private an import to reduce the rebuild pole (lea…
cf887a6 
…nprover-community#39609)

The aim of this PR is to make tweaks to imports to make the *rebuild* time shorter by making more use of the module system. This is measured in the "lakeprof" report in the radar: https://speed.lean-lang.org/mathlib4-out/396c763262259f066f3837c32643dd752994ca6d/
The first block shows the longest pole when building mathlib, and the second shows it when a rebuild occurs; and as a result of this PR, the relative difference is increased by quite a bit. Note that the "lakeprof/longest rebuild path//wall-clock" is somewhat noisy, but the relative difference should be measured with somewhat less noise.

This was done manually, by taking the second-slowest file in the rebuild path, and tweaking imports around it.
Bergschaf pushed a commit to Bergschaf/mathlib4 that referenced this pull request Jun 3, 2026
@b-mehta @Bergschaf
chore(LongestPole): private an import to reduce the rebuild pole (lea…
a7a3230 
…nprover-community#39609)

The aim of this PR is to make tweaks to imports to make the *rebuild* time shorter by making more use of the module system. This is measured in the "lakeprof" report in the radar: https://speed.lean-lang.org/mathlib4-out/396c763262259f066f3837c32643dd752994ca6d/
The first block shows the longest pole when building mathlib, and the second shows it when a rebuild occurs; and as a result of this PR, the relative difference is increased by quite a bit. Note that the "lakeprof/longest rebuild path//wall-clock" is somewhat noisy, but the relative difference should be measured with somewhat less noise.

This was done manually, by taking the second-slowest file in the rebuild path, and tweaking imports around it.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@grunweg grunweg Awaiting requested review from grunweg

Assignees

@j-loreaux j-loreaux

@grunweg grunweg

Labels

ready-to-merge This PR has been sent to bors. t-analysis Analysis (normed *, calculus) tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@b-mehta @leanprover-radar @grunweg @j-loreaux