[Merged by Bors] - fix(scripts): make lint-style.* work on macos and windows #6047
Conversation
This is hard to test in CI without mangling an intentionally broken locale I think, so unfortunately just shoving it in there...
bryangingechen
added
awaiting-review
scripts/lint_style_sanity_test.py
Outdated
| Running it exits with successful return code. | ||
| """ | ||
|
|
||
| subprocess.run(["./scripts/lint-style.sh"], check=True, cwd=ROOT_DIR) |
There was a problem hiding this comment.
If a commit has a style linting error, will this test also fail?
There was a problem hiding this comment.
Good catch. Yes, but I put in a way to make that not happen now. (One which involves running the linter yet another time, but without this I think it'd be hard to know that wasn't the case -- the shell script uses xargs, so you can't say check a particular return code because xargs changes the return code).
There was a problem hiding this comment.
If someone accidentally commits a .lean file with the executable bit set, this test will still fail, right?
Would it be better to create a temporary mostly-empty skeleton directory to run the test scripts in?
There was a problem hiding this comment.
Ech yes I suppose so.
Would it be better to create a temporary mostly-empty skeleton directory to run the test scripts in?
I guess, though it seems also potentially fragile since the script depends on arbitrary other files in the checkout (e.g. it blows up currently if style-exceptions.txt isn't present, and also depends on src/tactics/reserved_notation.lean...). Will give it a shot I suppose.
There was a problem hiding this comment.
Thanks again! I'm fully open to other suggestions, by the way. The main concern I have here is the experience for the typical user who doesn't want to think about the style linter unless it fails in GitHub Actions, so ideally the self-tests should never fail if someone doesn't touch the linting script in their commit.
There was a problem hiding this comment.
Yeah of course! I agree random folks will be confused if they see this test fail.
The other thing that occurred to me is possibly running this self-test against the src and archive directories from master, no matter what branch is running (but still use that branch's scripts directory). I'm letting it "steep" in my head to see which thing makes me feel least icky.
There was a problem hiding this comment.
Actually I guess it occurs to me that GH Actions I believe supports some syntax for saying when to run a particular job, so perhaps yet another way would be only running the self-test at all when the scripts directory has changes.
There was a problem hiding this comment.
Actually I guess it occurs to me that GH Actions I believe supports some syntax for saying when to run a particular job, so perhaps yet another way would be only running the self-test at all when the
scriptsdirectory has changes.
Right, this could work as well, though I think you would have a "run-always" preliminary step that checks for changes in scripts/, since from what I remember GHA doesn't have anything built-in that can tell you that.
However, one of the key issues here seems to be how to deal with all the assumptions the script makes about the directory / file structure of mathlib. I think it's probably better to make them explicit in Python in a test somehow rather than in the GHA workflow.
There was a problem hiding this comment.
OK went with running the script in a separate tree entirely...
Not too painful. Small chance of false negatives due to not having a "real" enough directory tree but maybe it's the best option. Let me know what you think.
Julian
force-pushed
the
linter-take-three
branch
from
e870edc
to
fcc3591
Compare
github-actions
bot
added
ready-to-merge
Make lint-style.sh use a POSIX-portable way of checking for executable bits, and make it always open files as UTF-8. Also makes CI run the sanity checks across all 3 OSes to ensure this stays working.
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
Make lint-style.sh use a POSIX-portable way of checking for executable bits, and make it always open files as UTF-8. Also makes CI run the sanity checks across all 3 OSes to ensure this stays working.
Make lint-style.sh use a POSIX-portable way of checking for executable bits, and make it always open files as UTF-8.
Also makes CI run the sanity checks across all 3 OSes to ensure this stays working.