chore: minimize all imports#160
Conversation
|
Presumably you used a script to identify the changes in this PR? If so, perhaps that script can be added to the repo so that everyone can run it. I for one often forget to run |
|
I actually did this by hand because it wasn't that long... but now that you mention it, I think |
|
Okay, that was pretty simple, great idea @ctchou! Now if you run This slightly conflicts with imports in #157 and #158. Probably easier to review/merge those first. |
|
On second thought, if the notation changes in those other PRs are problematic maybe we should merge this first to minimize merge conflicts. |
|
At Kim's suggestion I have changed @fmontesi As an added bonus, this removes the syntax conflicts in #157 and #158! I still slightly worry that it could cause trouble down the line, but we are not forced to make that decision now (and it is relatively simple to change) so I am closing those PRs for now. |
This PR does the following: - remove a full `import Mathlib` from `Cslib.Foundations.Lint.Basic` that was then transitively imported everywhere - add `import Mathlib.Tactic.Common` to `Cslib.Init.lean` so that we don't need to manually import these tactics each time while also reducing the number of build jobs - when appropriate, change the imports of every file to match what is given by `lake exe shake` or record an exception in `scripts/noshake.json` - Add `lake exe shake` in CI to maintain this going forward.
This PR does the following: - remove a full `import Mathlib` from `Cslib.Foundations.Lint.Basic` that was then transitively imported everywhere - add `import Mathlib.Tactic.Common` to `Cslib.Init.lean` so that we don't need to manually import these tactics each time while also reducing the number of build jobs - when appropriate, change the imports of every file to match what is given by `lake exe shake` or record an exception in `scripts/noshake.json` - Add `lake exe shake` in CI to maintain this going forward.
4 participants
This PR does the following:
import MathlibfromCslib.Foundations.Lint.Basicthat was then transitively imported everywhereimport Mathlib.Tactic.CommontoCslib.Init.leanso that we don't need to manually import these tactics each time while also reducing the number of build jobslake exe shakeor record an exception inscripts/noshake.jsonlake exe shakein CI to maintain this going forward.