[Merged by Bors] - chore: move lint_style executable to the scripts directory#14057
[Merged by Bors] - chore: move lint_style executable to the scripts directory#14057
lint_style executable to the scripts directory#14057Conversation
Otherwise, importing `Mathlib.Tactic` makes defining own executables impossible, as the `main` function in `Linter.TextBased` would collide with any other main function. Move the code for the lint_style executable to scripts (which arguably might be a better place anyway); we leave the text-based linters in Tactic/Linter.
PR summary 5e2a43cf4cImport changesDependency changes
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> |
|
maintainer merge LGTM, but let's get a second pair of eyes. |
|
🚀 Pull request has been placed on the maintainer queue by eric-wieser. |
| for s in ["Archive.lean", "Counterexamples.lean", "Mathlib.lean"] do | ||
| let n ← lintAllFiles (System.mkFilePath [s]) errorStyle | ||
| numberErrorFiles := numberErrorFiles + n | ||
| return numberErrorFiles |
There was a problem hiding this comment.
Does this end up being the exit code of the function? Should the value make sure that it is not a non-zero multiple of 256, to avoid returning 0 when in reality there is an error?
There was a problem hiding this comment.
Good catch, in principle!
In practice, I don't think this issue is likely: UInt8 overflows at 256, but UInt32 like this and the other functions return overflows at 2^32. I think at this point, we'll have other problems... so I'll approve this for now. I you think this requires fixing, let me know and I'll change it in a follow-up!
There was a problem hiding this comment.
I am quite outside of my comfort zone here, but isn't this number reported back to the shell? I think that there, reduction mod 256 still happens:
$ ( exit 255 ); echo $?
255
$ ( exit 256 ); echo $?
0There was a problem hiding this comment.
Oh, that is a good point. (I wasn't aware of this detail about shell exit codes... TIL!) A quick search confirms that limiting to an exit code of at most 125 is the safest option.
https://unix.stackexchange.com/questions/418784/what-is-the-min-and-max-values-of-exit-codes-in-linux
Let me send a follow-up PR soon, and adapt mk_all at the same time.
|
bors d+ Please fix the exit code issue, but otherwise LGTM! |
|
✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Thanks for the review! Per my comment above, let me |
Otherwise, importing `Mathlib.Tactic` makes defining own executables impossible, as the `main` function in `Linter.TextBased` would collide with any other main function. Move the code for the lint_style executable to scripts (which arguably might be a better place anyway); we leave the text-based linters in Tactic/Linter.
|
Build failed (retrying...): |
Otherwise, importing `Mathlib.Tactic` makes defining own executables impossible, as the `main` function in `Linter.TextBased` would collide with any other main function. Move the code for the lint_style executable to scripts (which arguably might be a better place anyway); we leave the text-based linters in Tactic/Linter.
|
This PR was included in a batch that was canceled, it will be automatically retried |
Otherwise, importing `Mathlib.Tactic` makes defining own executables impossible, as the `main` function in `Linter.TextBased` would collide with any other main function. Move the code for the lint_style executable to scripts (which arguably might be a better place anyway); we leave the text-based linters in Tactic/Linter.
|
Pull request successfully merged into master. Build succeeded: |
lint_style executable to the scripts directorylint_style executable to the scripts directory
Otherwise, importing `Mathlib.Tactic` makes defining own executables impossible, as the `main` function in `Linter.TextBased` would collide with any other main function. Move the code for the lint_style executable to scripts (which arguably might be a better place anyway); we leave the text-based linters in Tactic/Linter.
Otherwise, importing `Mathlib.Tactic` makes defining own executables impossible, as the `main` function in `Linter.TextBased` would collide with any other main function. Move the code for the lint_style executable to scripts (which arguably might be a better place anyway); we leave the text-based linters in Tactic/Linter.
Otherwise, importing
Mathlib.Tacticmakes defining own executables impossible, as themainfunction inLinter.TextBasedwould collide with any other main function. Move the code for the lint_style executable to scripts (which arguably might be a better place anyway); we leave the text-based linters in Tactic/Linter.