Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - ci(scripts/*): linting for copyright, imports, module docstrings, line length #4486

Closed
wants to merge 28 commits into from
Closed

[Merged by Bors] - ci(scripts/*): linting for copyright, imports, module docstrings, line length #4486

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
28 commits
Select commit Hold shift + click to select a range
0296cb5
chore(scripts/*): crude linting for copyright, imports, module docstr…
jcommelin Oct 6, 2020
8b2a6a6
Merge branch 'community-master' into mod-doc-lint
bryangingechen Oct 6, 2020
d6b96b8
rework scripts and output format
bryangingechen Oct 6, 2020
0d90a8c
update github workflow and update_nolints.sh
bryangingechen Oct 6, 2020
54c69c7
allow "Author(s):"
bryangingechen Oct 6, 2020
f1d572b
use enumerate
bryangingechen Oct 7, 2020
0947fef
update exceptions
bryangingechen Oct 7, 2020
8664a96
fix enumerate index, relax copyright header check
bryangingechen Oct 7, 2020
466623c
chore(*): fix authorship for split files (#4480)
bryangingechen Oct 6, 2020
99bdeb8
feat(ring_theory/witt_vector/structure_polynomial): witt_structure_ra…
jcommelin Oct 6, 2020
d41c321
feat(data/polynomial/degree/basic): add lemmas dealing with monomials…
adomani Oct 6, 2020
5caa01f
feat(measure_theory): integral of a non-negative function is >0 iff μ…
urkud Oct 6, 2020
f080aaa
feat(data/nat/basic): add_succ_lt_add (#4483)
jsm28 Oct 6, 2020
d1df3b9
lint(order/bounded_lattice): docstring (#4484)
hrmacbeth Oct 6, 2020
c510fbc
lint(ring_theory/*): docstrings (#4485)
awainverse Oct 7, 2020
319c624
feat(control/traversable/basic): composition of applicative transform…
kmill Oct 7, 2020
6d3d425
lint(order/order_iso_nat): docstrings (#4488)
awainverse Oct 7, 2020
ffb10a8
lint(order/lexographic, pilex): docstrings (#4489)
awainverse Oct 7, 2020
6560f6a
chore(scripts): update nolints.txt (#4490)
leanprover-community-bot Oct 7, 2020
9eed9ec
Allow comments in import-only files
jcommelin Oct 7, 2020
9b251b6
Allow unicode copyright symbol in headers
jcommelin Oct 7, 2020
0e3f228
Don't allow empty lines before copyright header
jcommelin Oct 7, 2020
5484cca
lint(group_theory/perm/*): docstrings (#4492)
awainverse Oct 7, 2020
f9492d1
lint(group_theory/*): docstrings and an inhabited instance (#4493)
awainverse Oct 7, 2020
8377549
Merge branch 'master' into mod-doc-lint
jcommelin Oct 7, 2020
fcb6e59
Apply suggestions from code review
jcommelin Oct 7, 2020
72bbc94
fix errors
jcommelin Oct 7, 2020
12d651c
lint for long lines
jcommelin Oct 7, 2020
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
12 changes: 8 additions & 4 deletions .github/workflows/build.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Copy link
Member

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?

Copy link
Member

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.

echo "short_lean_version=$(~/.elan/bin/lean --run scripts/lean_version.lean)" >> $GITHUB_ENV

- name: install azcopy
run: |
Expand Down Expand Up @@ -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: |
Expand All @@ -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
Expand All @@ -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
Copy link
Member

Choose a reason for hiding this comment

The 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.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The 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.

./scripts/lint-copy-mod-doc.sh