Closed
Conversation
PR summary ca235292b4Import changesNo significant changes to the import graph Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>
## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit> |
85d815a to
c5d47b4
Compare
15 tasks
As all module names do not contain path separators, splitting on file paths is actually fine :-)
thus, we *could* error on invalid lines, in principle.
Add a --github flag (false by default): if true, the script produces errors wrappable by the github matchers, but if false, it produces human-readable and clickable output!
This means a separate mode variable is not necessary: yay for proper inductive types; these are amazing!
If none are specified, all files are linted.
037fe17 to
fa3ee22
Compare
de13713 to
7ad105d
Compare
…tions and replace the contents of style-exceptions by the new output. Call the Python linter with an external shell script, which is simpler than update-style-exceptions.py. Replace all uses of update-style-exceptions by lake exe lint_style --regenerate.
7ad105d to
36d4ea1
Compare
|
This PR/issue depends on: |
Merge branch 'master' into MR-prettier-file-length-errors
Closed
1 task
Contributor
Author
|
This has been implemented now (except for just linting individual files, which can be added later). Closing. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Produce prettier output on errors for the Lean style linter:
On top of this, re-implements the
update_style_exceptionsscript in Lean, aslean exe lint_style --regenerate. As long as there are Python style linters, this calls into the Python linters to update the output.When the dependent PR lands, this will be split into a follow-up.
Likewise, just re-ordering the style exceptions could be split into its own PR as well.
This only covers the text-based linter in Lean, sorry: if you crave for better errors, you can help by reviewing my PRs to rewrite the Python lints in Lean :-)
Feedback on naming the flag is welcome: for instance, is
--ignore(matchingshake) better than--update?This has the side effect of re-ordering the existing style exceptions: now, they are (essentially) sorted by error type first.
I'd argue this is more useful in practice. If you want me to split this re-ordering into a separate PR, I can do so.
update-style-exceptions.py; produce human-readable output by default #14012 for adding human-readable output (the first part)