chore: remove or annotate import alls - #42462
Conversation
PR summary 5d653388ef
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Lean.Meta.RefinedDiscrTree.Encode | 63 | 61 | -2 (-3.17%) |
| Mathlib.Tactic.GCongr.Core | 83 | 82 | -1 (-1.20%) |
| Mathlib.Data.Int.Bitwise | 403 | 400 | -3 (-0.74%) |
| Mathlib.Control.Monad.Cont | 139 | 138 | -1 (-0.72%) |
| Mathlib.Data.Fintype.Parity | 464 | 461 | -3 (-0.65%) |
| Mathlib.Tactic.PNatToNat | 489 | 486 | -3 (-0.61%) |
| Mathlib.Tactic.FieldSimp.Discharger | 514 | 512 | -2 (-0.39%) |
Import changes for all files
| Files | Import difference |
|---|---|
| ../mathlib-ci/scripts/pr_summary/import_trans_difference.sh all | |
| There are 7723 files with changed transitive imports taking up over 342728 characters: this is too many to display! | |
You can run this locally from your mathlib4 directory: |
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
Declarations diff (regex)
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.
Declarations diff (Lean)
✅ Lean-aware diff — post-build, computed from the Lean environment (commit
5da66e9).
- +0 new declarations
- −0 removed declarations
No declaration differences.
No changes to strong technical debt.
No changes to weak technical debt.
Current commit 5d653388ef
Reference commit 4d6f98930f
This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
|
!bench |
|
Benchmark results for d213f73 against 4d6f989 are in. No significant results found. @thorimur
Small changes (1✅)
|
|
See also #41389 :') |
| module | ||
|
|
||
| import all Lean.Meta.Tactic.Simp.Rewrite | ||
| import all Lean.Meta.Tactic.Simp.Rewrite -- for `Simp.dischargeUsingAssumption?` |
There was a problem hiding this comment.
while you are at it, can you order the imports in these files accordingly?
There was a problem hiding this comment.
Normally I'd say yes, I'd rather keep this PR tightly focused for easy review (and not be too much of a time sink for me!) and leave import reordering to other PRs if that's alright :)
Oops, so sorry to overlap! 😅 It'll be interesting to see if the bench comes back differently. |
|
Hmm, a smaller increase than the other PR, but still not green on instructions overall. Very weird. |
0.01% is small enough that if you run it again after empty commit, it might just get green. (generally everything under <0.07% or so I'd say) |
|
This pull request is now in draft mode. No active bors state needed cleanup. While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like |
|
But I'm still confused as to why yours takes a hit and mine doesn't 🤔 As far as I can tell the only two changes are (1) I'm going to test out these two changes, see what happens, then one way or another close this PR and maintainer merge yours :) Would you mind grabbing the three annotations from this PR? |
|
!bench |
|
Benchmark results for 5da66e9 against 4d6f989 are in. No significant results found. @thorimur
Small changes (1✅)
|
|
!bench |
|
Benchmark results for 5d65338 against 4d6f989 are in. No significant results found. @thorimur
Small changes (1✅)
|
3 participants
This PR removes immediately removable
import alland adds a comment to un-annotated unremovableimport alls explaining what they're for (except forimport all Mathlib.NumberTheory.Height.BasicinMathlib.NumberTheory.Height.MvPolynomial, which seems to depend on multiple parts of the private interface).