[Merged by Bors] - chore: import Mathlib.Init in all files#18277
[Merged by Bors] - chore: import Mathlib.Init in all files#18277
Conversation
PR summary 658bbaaae9Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Data.Nat.BinaryRec | 1 | 18 | +17 (+1700.00%) |
| Mathlib.Data.Stream.Defs | 1 | 18 | +17 (+1700.00%) |
| Mathlib.Deprecated.Logic | 1 | 18 | +17 (+1700.00%) |
| Mathlib.Std.Data.HashMap | 1 | 18 | +17 (+1700.00%) |
| Mathlib.Tactic.CategoryTheory.Coherence.Datatypes | 1 | 18 | +17 (+1700.00%) |
| Mathlib.Util.AssertExistsExt | 1 | 18 | +17 (+1700.00%) |
| Mathlib.Tactic.Linter.AdmitLinter | 1 | 17 | +16 (+1600.00%) |
| Mathlib.Tactic.StacksAttribute | 1 | 17 | +16 (+1600.00%) |
| Mathlib.Tactic.Linter.FlexibleLinter | 2 | 18 | +16 (+800.00%) |
Import changes for all files
| Files | Import difference |
|---|---|
3 filesMathlib.Tactic.StacksAttribute Mathlib.Tactic.Linter.AdmitLinter Mathlib.Tactic.Linter.FlexibleLinter |
16 |
14 filesMathlib.Data.Int.DivMod Mathlib.Tactic.CategoryTheory.Coherence.Datatypes Mathlib.Data.Nat.BinaryRec Mathlib.Tactic.CC.Lemmas Mathlib.Tactic.CategoryTheory.Coherence.PureCoherence Mathlib.Tactic.Linter.TextBased Mathlib.Std.Data.HashMap Mathlib.Util.AssertExistsExt Mathlib.Deprecated.Combinator Mathlib.Logic.OpClass Mathlib.Tactic.CategoryTheory.Coherence.Normalize Mathlib.Data.Stream.Defs Mathlib.Deprecated.Logic Mathlib.Data.Nat.Notation |
17 |
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/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for script/declarations_diff.sh contains some details about this script.
This manually adds 'import Mathlib.Init' to all files which are currently missing this. A future PR will add an automatic check for this.
02436ae to
fbc0b2d
Compare
Stream'.corec' was pre-existing; add it to the exceptions list
Ruben-VandeVelde
left a comment
There was a problem hiding this comment.
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by Ruben-VandeVelde. |
|
I'm guessing the motivation is this thread? Could you add a word or two to the PR description about it? |
|
In fact, my motivation is unrelated to that: as I understand it, upon Mathlib.Init''s creation, the idea was that every file in Mathlib should import it --- this was just postponed to a later PR and never enforced so far. This PR is an easy way to enforce it. |
|
If you think the zulip thread you reference is also useful motivation, feel free to add it to the description! |
|
Reading over the thread again, I'm not sure that it's relevant anymore... I guess there's a tradeoff here between making the imports consistent and keeping a handful of files slightly lighter (many of them seem like they won't be imported without the rest of mathlib anyways). bors d=adomani |
|
✌️ adomani can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Thanks! Another consequence of importing Init everywhere is that the style linters will lint most files. bors merge |
This manually adds 'import Mathlib.Init' to all files which are currently missing this. A future PR will add an automatic check for this.
|
Build failed (retrying...): |
This manually adds 'import Mathlib.Init' to all files which are currently missing this. A future PR will add an automatic check for this.
|
Build failed (retrying...): |
This manually adds 'import Mathlib.Init' to all files which are currently missing this. A future PR will add an automatic check for this.
|
Pull request successfully merged into master. Build succeeded: |
This manually adds 'import Mathlib.Init' to all files which are currently missing this.
A future PR will add an automatic check for this.
This PR itself is easy to review: it just adds that one import. The fact that everything builds shows there is no import cycle.
The
large-importschanges are by design (and show this change does something).