-
Notifications
You must be signed in to change notification settings - Fork 299
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] - ci(scripts/*): linting for copyright, imports, module docstrings, line length #4486
[Merged by Bors] - ci(scripts/*): linting for copyright, imports, module docstrings, line length #4486
Changes from 22 commits
0296cb5
8b2a6a6
d6b96b8
0d90a8c
54c69c7
f1d572b
0947fef
8664a96
466623c
99bdeb8
d41c321
5caa01f
f080aaa
d1df3b9
c510fbc
319c624
6d3d425
ffb10a8
6560f6a
9eed9ec
9b251b6
0e3f228
5484cca
f9492d1
8377549
fcb6e59
72bbc94
12d651c
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -30,8 +30,8 @@ jobs: | |
set -o pipefail | ||
curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y | ||
~/.elan/bin/lean --version | ||
echo "::add-path::$HOME/.elan/bin" | ||
echo "::set-env name=short_lean_version::$(~/.elan/bin/lean --run scripts/lean_version.lean)" | ||
echo "$HOME/.elan/bin" >> $GITHUB_PATH | ||
echo "short_lean_version=$(~/.elan/bin/lean --run scripts/lean_version.lean)" >> $GITHUB_ENV | ||
|
||
- name: install azcopy | ||
run: | | ||
|
@@ -94,7 +94,7 @@ jobs: | |
set -o pipefail | ||
curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y | ||
~/.elan/bin/lean --version | ||
echo "::add-path::$HOME/.elan/bin" | ||
echo "$HOME/.elan/bin" >> $GITHUB_PATH | ||
|
||
- name: lint | ||
run: | | ||
|
@@ -119,7 +119,7 @@ jobs: | |
set -o pipefail | ||
curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh -s -- --default-toolchain none -y | ||
~/.elan/bin/lean --version | ||
echo "::add-path::$HOME/.elan/bin" | ||
echo "$HOME/.elan/bin" >> $GITHUB_PATH | ||
|
||
- name: install Python | ||
uses: actions/setup-python@v1 | ||
|
@@ -144,3 +144,7 @@ jobs: | |
python scripts/yaml_check.py docs/100.yaml docs/overview.yaml docs/undergrad.yaml | ||
bash scripts/mk_all.sh | ||
lean --run scripts/yaml_check.lean | ||
|
||
- name: check for copyright headers and module docstrings | ||
run: | | ||
Comment on lines
+147
to
+149
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Can this be run before any of the really slow build steps? I don't want to wait hours for a build, only for it to then say my line is too long and have to start all over again because the file I wrapped the line in needs rebuilding. There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. My reasoning was the opposite; since fixing the issues caught by this script shouldn't typically create new build / linter issues, it's better to report those "more serious" problems first so that those can be addressed / discussed. For example, fixing a build / linter issue (e.g. from a github suggestion) might temporarily make a line too long, and I think it'd be better to first check that the suggestion "works" rather than force people to reflow everything up front. Feel free to bring this up on Zulip, I'd be curious to hear others' thoughts on this as well. Note that you should be able to run this script manually by executing |
||
./scripts/lint-copy-mod-doc.sh |
Large diffs are not rendered by default.
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,122 @@ | ||
#!/usr/bin/env python3 | ||
|
||
import sys | ||
|
||
fns = sys.argv[1:] | ||
|
||
ERR_COP = 0 | ||
ERR_IMP = 1 | ||
ERR_MOD = 2 | ||
|
||
exceptions = [] | ||
|
||
with open("scripts/copy-mod-doc-exceptions-short.txt") as f: | ||
lines = f.readlines() | ||
for line in lines: | ||
(fn, c, errno) = line.split() | ||
jcommelin marked this conversation as resolved.
Show resolved
Hide resolved
|
||
if errno == "ERR_COP": | ||
exceptions += [(ERR_COP, fn)] | ||
if errno == "ERR_IMP": | ||
exceptions += [(ERR_IMP, fn)] | ||
if errno == "ERR_MOD": | ||
exceptions += [(ERR_MOD, fn)] | ||
|
||
new_exceptions = False | ||
|
||
def import_only_check(lines, fn): | ||
import_only_file = True | ||
errors = [] | ||
line_nr = 0 | ||
in_comment = False | ||
for line_nr, line in enumerate(lines, 1): | ||
if "/-" in line: | ||
in_comment = True | ||
if "-/" in line: | ||
in_comment = False | ||
continue | ||
if line == "\n" or in_comment: | ||
continue | ||
imports = line.split() | ||
if imports[0] == "--": | ||
continue | ||
if imports[0] != "import": | ||
import_only_file = False | ||
break | ||
if len(imports) > 2: | ||
if imports[2] == "--": | ||
continue | ||
else: | ||
errors += [(ERR_IMP, line_nr, fn)] | ||
return (import_only_file, errors) | ||
|
||
def regular_check(lines, fn): | ||
errors = [] | ||
copy_started = False | ||
copy_done = False | ||
copy_start_line_nr = 0 | ||
copy_lines = "" | ||
for line_nr, line in enumerate(lines, 1): | ||
if not copy_started and line == "\n": | ||
errors += [(ERR_COP, copy_start_line_nr, fn)] | ||
continue | ||
if not copy_started and line == "/-\n": | ||
copy_started = True | ||
copy_start_line_nr = line_nr | ||
continue | ||
if not copy_started: | ||
errors += [(ERR_COP, line_nr, fn)] | ||
if copy_started and not copy_done: | ||
copy_lines += line | ||
if line == "-/\n": | ||
if ((not "Copyright" in copy_lines) or | ||
(not "Apache" in copy_lines) or | ||
(not "Author" in copy_lines)): | ||
errors += [(ERR_COP, copy_start_line_nr, fn)] | ||
copy_done = True | ||
continue | ||
if copy_done and line == "\n": | ||
continue | ||
words = line.split() | ||
if words[0] != "import" and words[0] != "/-!": | ||
errors += [(ERR_MOD, line_nr, fn)] | ||
break | ||
if words[0] == "/-!": | ||
break | ||
# final case: words[0] == "import" | ||
if len(words) > 2: | ||
if words[2] != "--": | ||
errors += [(ERR_IMP, line_nr, fn)] | ||
return errors | ||
|
||
def format_errors(errors): | ||
global new_exceptions | ||
for (errno, line_nr, fn) in errors: | ||
if (errno, fn) in exceptions: | ||
continue | ||
new_exceptions = True | ||
# filename first, then line so that we can call "sort" on the output | ||
if errno == ERR_COP: | ||
print("{} : line {} : ERR_COP : Malformed or missing copyright header".format(fn, line_nr)) | ||
if errno == ERR_IMP: | ||
print("{} : line {} : ERR_IMP : More than one file imported per line".format(fn, line_nr)) | ||
if errno == ERR_MOD: | ||
print("{} : line {} : ERR_MOD : Module docstring missing, or too late".format(fn, line_nr)) | ||
|
||
def lint(fn): | ||
with open(fn) as f: | ||
lines = f.readlines() | ||
(b, errs) = import_only_check(lines, fn) | ||
if b: | ||
format_errors(errs) | ||
return | ||
errs = regular_check(lines, fn) | ||
format_errors(errs) | ||
|
||
for fn in fns: | ||
lint(fn) | ||
|
||
# if "exceptions" is empty, | ||
# we're trying to generate copy-mod-doc-exceptions.txt, | ||
# so new exceptions are expected | ||
if new_exceptions and len(exceptions) > 0: | ||
exit(1) |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,12 @@ | ||
#!/usr/bin/env bash | ||
|
||
# This is a little wrapper around the python script | ||
# lint-copy-mod-doc.py | ||
|
||
touch scripts/copy-mod-doc-exceptions.txt | ||
|
||
cut -d: -f1,3 < scripts/copy-mod-doc-exceptions.txt > scripts/copy-mod-doc-exceptions-short.txt | ||
|
||
find src archive -name '*.lean' | xargs ./scripts/lint-copy-mod-doc.py | ||
|
||
rm scripts/copy-mod-doc-exceptions-short.txt |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
#!/usr/bin/env bash | ||
|
||
# This is a little wrapper around the python script | ||
# lint-copy-mod-doc.py | ||
|
||
# we want an empty "exceptions" array in lint-copy-mod-doc.py | ||
> scripts/copy-mod-doc-exceptions-short.txt | ||
|
||
find src archive -name '*.lean' | xargs ./scripts/lint-copy-mod-doc.py | sort > scripts/copy-mod-doc-exceptions.txt | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I appreciate the creative use of the There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Is it too evil? There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. It should be be fine. I don't know if the shell guarantees to open the file before launching the subprocesses, but even if it doesn't There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. Hmm, it looks like the |
||
|
||
rm scripts/copy-mod-doc-exceptions-short.txt | ||
jcommelin marked this conversation as resolved.
Show resolved
Hide resolved
|
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.
Not unhappy with the change, but it's completely unrelated, right?
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.
Yes, Bryan mentioned a link to a GH blog post about some vulnerability that is fixed by this change.