[Merged by Bors] - fix(scripts/{lint_style,mk_all}): limit return value to 125#14272
[Merged by Bors] - fix(scripts/{lint_style,mk_all}): limit return value to 125#14272
Conversation
so the executable's exit code can be used further in shell scripts, such as mathlib's CI. See https://unix.stackexchange.com/a/418802 for background why a maximum of 125 is safest (on Linux).
PR summary 0342e28cefImport 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> |
|
@adomani Since you raised this issue (thanks again for pointing me in this direction!), would you like to take a look? |
| return numberErrorFiles | ||
| -- Make sure to return an exit code of at most 125, so this return value can be used further | ||
| -- in shell scripts. | ||
| return min numberErrorFiles 125 |
There was a problem hiding this comment.
| return min numberErrorFiles 125 | |
| return min (numberErrorFiles % 128) 125 |
I wonder whether this can be (ever so slightly) more meaningful:
- reduce module 128=2^7 (since 126 and 127 are excluded for other reasons, but 128 appears to be the meaningful number);
- truncate at 125 to avoid 126 and 127.
There was a problem hiding this comment.
But this would mishandle the case of exactly 128 errors, right? I just pushed a commit allowing 128 explicitly - it is somewhat longer. Do you think returning an exit code of 128 is an important feature? I am not convinced the longer code is worth it, but could be swayed otherwise.
There was a problem hiding this comment.
Sorry, I got this wrong. We should special-case actual value 0 and everything else.
How about something like
if numberErrorFiles == 0 then return 0 else
return max 1 (numberErrorFiles % 125)There was a problem hiding this comment.
This makes more sense! Why should we do modulo though, instead of saturating? I'd prefer 130 files to return a code of 125 over 2 (or 5), WDYT?
There was a problem hiding this comment.
Sure, I do not have a preference. There might even be some value into specifying that exit code 1 means there were some errors and leave other error codes for potentially other meanings. Feel free to pick what you prefer: let's simply make sure that exit code 0 is if and only if numberErrorFiles = 0! 😄
There was a problem hiding this comment.
I'll let a maintainer weigh in on their preference: I have a weak preference for simply reverting the most recent commit (just pushed this); I'm happy to do either of the other options.
There was a problem hiding this comment.
Saturation sounds better to me, but we're in the weeds here. :-)
|
🚀 Pull request has been placed on the maintainer queue by adomani. |
1 similar comment
|
🚀 Pull request has been placed on the maintainer queue by adomani. |
|
🚀 Pull request has been placed on the maintainer queue by adomani. |
|
bors d+ |
|
✌️ grunweg can now approve this pull request. To approve and merge a pull request, simply reply with |
|
It seems that the current solution satisfies everybody - let's land this. Thanks for the reviews and the keen comments! |
so the executable's exit code can be used further in shell scripts, such as mathlib's CI. See https://unix.stackexchange.com/a/418802 for background why a maximum of 125 is safest (on Linux).
|
Build failed (retrying...): |
so the executable's exit code can be used further in shell scripts, such as mathlib's CI. See https://unix.stackexchange.com/a/418802 for background why a maximum of 125 is safest (on Linux).
|
Pull request successfully merged into master. Build succeeded: |
so the executable's exit code can be used further in shell scripts, such as mathlib's CI. See https://unix.stackexchange.com/a/418802 for background why a maximum of 125 is safest (on Linux).
so the executable's exit code can be used further in shell scripts, such as mathlib's CI.
See https://unix.stackexchange.com/a/418802 for background why a maximum of 125 is safest (on Linux).