-
Notifications
You must be signed in to change notification settings - Fork 331
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
[Merged by Bors] - move: new Mathlib.Tactic.Linter
dir
#11807
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Linter
might be better than Linters
, to match how we have Tactic
not Tactics
.
Eric, thanks! I made the change |
Mathlib/Tactic/Common.lean
Outdated
@@ -60,7 +60,7 @@ import Mathlib.Tactic.InferParam | |||
import Mathlib.Tactic.Inhabit | |||
import Mathlib.Tactic.IrreducibleDef | |||
import Mathlib.Tactic.Lift | |||
import Mathlib.Tactic.Lint | |||
import Mathlib.Linter.Lint |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think we should put this in a section under ProofWidgets just to keep this file organized (since it's no longer in alphabetical order), so that it looks something roughly like
...
-- Hopefully `lake` will be able to handle tests later.
import ProofWidgets
-- Import Mathlib-specific linters.
import Mathlib.Linter.Lint
-- Now import all tactics defined in Mathlib that do not require theory files.
import Mathlib.Mathport.Rename
...
likely also with a change to the module doc
...
We include some commented out imports here, with an explanation of their theory requirements,
to save some time for anyone wondering why they are not here.
We also import theory-free linters, commands, and utilities which are useful to have low in the
import hierarchy.
-/
...
(Sorry, the fact that github doesn't let me make suggestions on non-modified code is relevant once more... 😅)
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks! If I implemented your suggestions, assuming that I understood them correctly!
This also seems blocked on zulip consensus. |
Per zulip, it seems there is sufficient consensus to go ahead with this one (with an e.g. awaiting-author |
@grunweg: I updated a little bit in auto-pilot mode. Is this what you had in mind? I wonder if, as a consequence of the |
Mathlib.Linter
dirMathlib.Tactic.Linter
dir
@adomani Thanks; I think I meant something like this.
Long-term, I think separate files for style linters, text-based ones and environment linters, for example, could be a useful classification. At the moment, there a few landed linters, so splitting could also happen later imho. |
It could be useful to think where e.g. all your in-flight linters want to land in the end - if the structure can house them, I think it's good enough! |
Ok, I'll leave this as is for now and we can discuss how many "generic linter import" files we have later on. I will probably have to update shake to "ignoreAll/..." the new path also. |
Fine with me - re-organising linters can also happen in a future PR. |
🚀 Pull request has been placed on the maintainer queue by grunweg. |
Somehow, I've thought more about this --- here's a more detailed proposal how mathlib's linters could end up. (For a follow-up PR.) In the medium to long term, I see at least three useful categories of linters:
Accordingly, I can imagine grouping
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks 🎉
bors merge
Pull request successfully merged into master. Build succeeded: |
Mathlib.Tactic.Linter
dirMathlib.Tactic.Linter
dir
-- Currently we don't need to import all of ProofWidgets, | ||
-- but without this, if you don't run `lake build ProofWidgets` then `make test` will fail. | ||
-- Hopefully `lake` will be able to handle tests later. | ||
import ProofWidgets |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Why did this come back?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think that this comment made me add it. I suspect that it was there at the time that this PR was opened, then the other PR was merged, the import possibly removed, but when this PR was looked at again, no one noticed that it was still here.
Create a new
Mathlib/Tactic/Linter
dir and move there the linters. Currently the new dir contains only one file, but there are more linters in PRs.This was brought up by @thorimur in the context of #11019. The suggestion there was to add a
Mathlib.Command.Linters
dir, but maybe the extraCommand
layer can be skipped -- at least for now.