-
Notifications
You must be signed in to change notification settings - Fork 330
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
feat: check that every file imports Mathlib.Init #18281
base: master
Are you sure you want to change the base?
Conversation
This manually adds 'import Mathlib.Init' to all files which are currently missing this. A future PR will add an automatic check for this.
Stream'.corec' was pre-existing; add it to the exceptions list
PR summary bebfe32f0eImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
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 |
Right now the module doc of Mathlib.Init says something like "this file is imported by virtually every file in Mathlib". If we add this linter, perhaps we should update that text and also mention that it's enforced by litner. |
Good point, updated the doc-string! |
We add a text-based check to the
lint-style
script, that every file either (transivively) imports Mathlib.Init, or is (transitively) imported by it.