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

bryangingechen · 2020-10-06T22:47:45Z

This PR adds some scripts to check the .lean files in src/ and archive/ for the following issues (which are out of scope for the current linter):

Malformed or missing copyright header
More than one file imported per line
Module docstring missing, or too late
Lines of length > 100 (unless they contain http)

The scripts are run at the end of our "tests" job since the "lint" job usually takes longer to run. (This isn't a big deal though, since they're quick.)

Current problems are saved in the file scripts/copy-mod-doc-exceptions.txt and ignored so that we don't have to fix everything up front. Over time, this should get shorter as we fix things!

Separately, this also fixes some warnings in our GitHub actions workflow (see this blog post).

Co-authored-by: Johan Commelin johan@commelin.net

We could potentially add a line-length linter to this. Any other ideas?

Reminder for myself; after this is merged, add a step that calls scripts/update-copy-mod-doc-exceptions.sh to the nolints workflow in azure-scripts.

…ings

scripts/lint-copy-mod-doc.py

fpvandoorn · 2020-10-06T23:14:54Z

Any other ideas

It could test a lot of the style guide automatically. However, at that point, we might want to integrate it into a syntactic linter that runs continuously when editing a file.
Some easy ideas: Spaces (or ` in comments) after (a fixed list of) binders, spaces around (a fixed list of) infix operators.

bryangingechen · 2020-10-07T00:33:20Z

I played around with adding "ERR_LLN" to catch lines > 100 characters. The script counted >3000 long lines in src/ and archive/. Thinking about it more though, there are a number of cases where long lines are OK (e.g. long URLs in comments, various cases where reflowing code would make it more difficult to read) and making contributors edit the exceptions file by hand could be a pain, so I'm not sure we want to strictly enforce this now.

If we want to warn about new long lines but still allow merging, we could do something complicated like only check for long lines when the branch isn't staging or master, but I'm not sure that would be worth it.

fpvandoorn · 2020-10-07T00:55:21Z

Makes sense, there are indeed allowed exceptions for long lines.

Here is another interesting Copyright header failure: https://github.com/leanprover-community/mathlib/blob/master/archive/sensitivity.lean
Most other failures seem to be the old style to have a 1-line description of the file in the same comment as the copyright header (example). Those failures are all probably caught by the missing module docstring test, so you could consider removing the test for copy_start_line_nr + 4.

bryangingechen · 2020-10-07T01:15:37Z

Oh good catch. That actually reminds me, I committed a file today that fails this too: 7948b5a#diff-e6caf1da183d89ccee7cd7361943f0d7.

I think I'll just try to collect all lines between copy_started and copy_done into one string and then search that for the magic keywords "Copyright (c)", "Apache" and "Author". (Hoping that nobody tries to do anything really strange just to get around this...)

bryangingechen · 2020-10-07T01:39:33Z

Here's another case of a valid copyright header that fails because the opening /- is not on its own line:

mathlib/src/measure_theory/category/Meas.lean

Line 1 in 7488f8e

I guess there's an argument for making these more uniform though.

jcommelin · 2020-10-07T04:51:48Z

My idea was indeed to have a non-urgent effort to make the copyright headers more uniform.
Arguably we could even ask that there are no empty lines above the copyright header.

bryangingechen · 2020-10-07T05:07:35Z

Arguably we could even ask that there are no empty lines above the copyright header.

I'd be fine with that. (Feel free to push more commits to this branch if you have more tweaks you'd like to make, I'm done until tomorrow.)

jcommelin

I'm happy with this

A few files with missing copyright headers in #4477 came from splitting up older files, so the attribution was incorrect: - `data/setoid/partition.lean` was split from `data/setoid.lean` in #2853. - `data/finset/order.lean` was split from `algebra/big_operators.lean` in #3495. - `group_theory/submonoid/operations.lean` was split from `group_theory/submonoid.lean` in #3058.

…t{_prop} (#4464) This is the first PR in a series on a fundamental theorem for Witt polynomials. Co-Authored-By: Rob Y. Lewis <rob.y.lewis@gmail.com>

…, their support and their nat_degrees (#4475)

…(support f) > 0 (#4410) Also add a few supporting lemmas

Add the lemma that, for natural numbers, if `a < b` and `c < d` then `a + c + 1 < b + d` (i.e. a stronger version of `add_lt_add` for the natural number case). `library_search` did not find this in mathlib.

Docstrings in `ring_theory/ideal/operations`, `ring_theory/multiplicity`, and `ring_theory/ring_invo`.

…ations (#4487) Added composition law for applicative transformations, added rest of interface for coercion of applicative transformations to functions (lifted from `monoid_hom`), and proved composition was associative and has an identity. Also corrected some documentation.

Adds docstrings to `rel_embedding.nat_lt` and `rel_embedding.nat_gt`

gebner · 2020-10-07T07:38:36Z

.github/workflows/build.yml

@@ -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


Not unhappy with the change, but it's completely unrelated, right?

Yes, Bryan mentioned a link to a GH blog post about some vulnerability that is fixed by this change.

scripts/lint-copy-mod-doc.py

scripts/nolints.txt

src/control/traversable/basic.lean

Adds missing docstrings in `group_theory/perm/cycles` and `group_theory/perm/sign`.

An inhabited instance for `presented_group` Docstrings in `group_theory/abelianization` and `group_theory/congruence`. Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

jcommelin · 2020-10-07T08:00:54Z

.github/workflows/build.yml

@@ -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


Yes, Bryan mentioned a link to a GH blog post about some vulnerability that is fixed by this change.

scripts/update-copy-mod-doc-exceptions.sh

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

gebner · 2020-10-07T10:58:39Z

scripts/update-copy-mod-doc-exceptions.sh

+# This is a little wrapper around the python script
+# lint-copy-mod-doc.py
+
+find src archive -name '*.lean' | xargs ./scripts/lint-copy-mod-doc.py | sort > scripts/copy-mod-doc-exceptions.txt


I appreciate the creative use of the > operator that makes lint-copy-mod-doc.py read its own output, which happens to be empty at first.

Is it too evil?

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 find takes long enough to prevent the race condition in practice.

Hmm, it looks like the > line got removed. I'd prefer to have that done in this script. I'll open a new PR.

gebner · 2020-10-07T11:02:22Z

bors r+

…e length (#4486) This PR adds some scripts to check the `.lean` files in `src/` and `archive/` for the following issues (which are out of scope for the current linter): - Malformed or missing copyright header - More than one file imported per line - Module docstring missing, or too late - Lines of length > 100 (unless they contain `http`) The scripts are run at the end of our "tests" job since the "lint" job usually takes longer to run. (This isn't a big deal though, since they're quick.) Current problems are saved in the file `scripts/copy-mod-doc-exceptions.txt` and ignored so that we don't have to fix everything up front. Over time, this should get shorter as we fix things! Separately, this also fixes some warnings in our GitHub actions workflow (see [this blog post](https://github.blog/changelog/2020-10-01-github-actions-deprecating-set-env-and-add-path-commands/)). Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: damiano <adomani@gmail.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Joseph Myers <jsm@polyomino.org.uk> Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: Aaron Anderson <awainverse@gmail.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: leanprover-community-bot <leanprover.community@gmail.com>

bors · 2020-10-07T14:06:17Z

Build failed (retrying...):

Run tests

gebner · 2020-10-07T14:19:52Z

This PR shouldn't cause any recompilation, so we're probably better off merging it by itself before it is batched together with yet another long-lined PR.

bors p=10

…e length (#4486) This PR adds some scripts to check the `.lean` files in `src/` and `archive/` for the following issues (which are out of scope for the current linter): - Malformed or missing copyright header - More than one file imported per line - Module docstring missing, or too late - Lines of length > 100 (unless they contain `http`) The scripts are run at the end of our "tests" job since the "lint" job usually takes longer to run. (This isn't a big deal though, since they're quick.) Current problems are saved in the file `scripts/copy-mod-doc-exceptions.txt` and ignored so that we don't have to fix everything up front. Over time, this should get shorter as we fix things! Separately, this also fixes some warnings in our GitHub actions workflow (see [this blog post](https://github.blog/changelog/2020-10-01-github-actions-deprecating-set-env-and-add-path-commands/)). Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com> Co-authored-by: damiano <adomani@gmail.com> Co-authored-by: Yury G. Kudryashov <urkud@urkud.name> Co-authored-by: Joseph Myers <jsm@polyomino.org.uk> Co-authored-by: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: Aaron Anderson <awainverse@gmail.com> Co-authored-by: Kyle Miller <kmill31415@gmail.com> Co-authored-by: leanprover-community-bot <leanprover.community@gmail.com>

eric-wieser · 2020-10-07T14:38:20Z

.github/workflows/build.yml

+
+      - name: check for copyright headers and module docstrings
+        run: |


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.

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.

eric-wieser · 2020-10-07T14:39:49Z

Current problems are saved in the file scripts/copy-mod-doc-exceptions.txt and ignored so that we don't have to fix everything up front. Over time, this should get shorter as we fix things!

Does this handle the case where new lines are inserted and the line numbers change?

bryangingechen · 2020-10-07T14:50:32Z

Does this handle the case where new lines are inserted and the line numbers change?

Line numbers are ignored when reading exceptions back, so yes.

gebner · 2020-10-07T15:24:06Z

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.

It might actually be best to run it in a separate actions workflow/job altogether since it doesn't even depend on the build step. The build step should still be run even if the linter fails.

But please do that in a new PR. This one is almost merged.

bors · 2020-10-07T16:07:51Z

Pull request successfully merged into master.

Build succeeded:

…ions.sh (#4513) Followup to #4486: - run the linter in a separate parallel job, per request - the update-*.sh script now correctly generates a full exceptions file - add some more comments to the shell scripts

jcommelin and others added 4 commits October 6, 2020 20:43

chore(scripts/*): crude linting for copyright, imports, module docstr…

0296cb5

…ings

Merge branch 'community-master' into mod-doc-lint

8b2a6a6

rework scripts and output format

d6b96b8

update github workflow and update_nolints.sh

0d90a8c

bryangingechen added awaiting-review The author would like community review of the PR CI This issue or PR is about continuous integration labels Oct 6, 2020

bryangingechen requested review from gebner and robertylewis October 6, 2020 22:47

fpvandoorn reviewed Oct 6, 2020

View reviewed changes

scripts/lint-copy-mod-doc.py Outdated Show resolved Hide resolved

bryangingechen added 2 commits October 6, 2020 19:34

allow "Author(s):"

54c69c7

use enumerate

f1d572b

update exceptions

0947fef

fix enumerate index, relax copyright header check

8664a96

jcommelin approved these changes Oct 7, 2020

View reviewed changes

bryangingechen and others added 9 commits October 7, 2020 06:27

feat(ring_theory/witt_vector/structure_polynomial): witt_structure_ra…

99bdeb8

…t{_prop} (#4464) This is the first PR in a series on a fundamental theorem for Witt polynomials. Co-Authored-By: Rob Y. Lewis <rob.y.lewis@gmail.com>

feat(data/polynomial/degree/basic): add lemmas dealing with monomials…

d41c321

…, their support and their nat_degrees (#4475)

feat(measure_theory): integral of a non-negative function is >0 iff μ…

5caa01f

…(support f) > 0 (#4410) Also add a few supporting lemmas

feat(data/nat/basic): add_succ_lt_add (#4483)

f080aaa

Add the lemma that, for natural numbers, if `a < b` and `c < d` then `a + c + 1 < b + d` (i.e. a stronger version of `add_lt_add` for the natural number case). `library_search` did not find this in mathlib.

lint(order/bounded_lattice): docstring (#4484)

d1df3b9

lint(ring_theory/*): docstrings (#4485)

c510fbc

Docstrings in `ring_theory/ideal/operations`, `ring_theory/multiplicity`, and `ring_theory/ring_invo`.

lint(order/order_iso_nat): docstrings (#4488)

6d3d425

Adds docstrings to `rel_embedding.nat_lt` and `rel_embedding.nat_gt`

jcommelin added 3 commits October 7, 2020 06:27

Allow comments in import-only files

9eed9ec

Allow unicode copyright symbol in headers

9b251b6

Don't allow empty lines before copyright header

0e3f228

gebner reviewed Oct 7, 2020

View reviewed changes

awainverse and others added 3 commits October 7, 2020 07:59

lint(group_theory/perm/*): docstrings (#4492)

5484cca

Adds missing docstrings in `group_theory/perm/cycles` and `group_theory/perm/sign`.

Merge branch 'master' into mod-doc-lint

8377549

jcommelin reviewed Oct 7, 2020

View reviewed changes

jcommelin and others added 3 commits October 7, 2020 10:03

Apply suggestions from code review

fcb6e59

Co-authored-by: Gabriel Ebner <gebner@gebner.org>

fix errors

72bbc94

lint for long lines

12d651c

gebner reviewed Oct 7, 2020

View reviewed changes

jcommelin changed the title ~~ci(scripts/*): linting for copyright, imports, module docstrings~~ ci(scripts/*): linting for copyright, imports, module docstrings, line length Oct 7, 2020

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Oct 7, 2020

eric-wieser reviewed Oct 7, 2020

View reviewed changes

bors bot changed the title ~~ci(scripts/*): linting for copyright, imports, module docstrings, line length~~ [Merged by Bors] - ci(scripts/*): linting for copyright, imports, module docstrings, line length Oct 7, 2020

bors bot closed this Oct 7, 2020

bors bot deleted the mod-doc-lint branch October 7, 2020 16:07

bryangingechen mentioned this pull request Oct 7, 2020

[Merged by Bors] - ci(*): run style lint in parallel job, fix update-copy-mod-doc-exceptions.sh #4513

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[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

bryangingechen commented Oct 6, 2020 •

edited by jcommelin

fpvandoorn commented Oct 6, 2020

bryangingechen commented Oct 7, 2020 •

edited

fpvandoorn commented Oct 7, 2020

bryangingechen commented Oct 7, 2020

bryangingechen commented Oct 7, 2020

jcommelin commented Oct 7, 2020

bryangingechen commented Oct 7, 2020

jcommelin left a comment

gebner Oct 7, 2020

jcommelin Oct 7, 2020

jcommelin Oct 7, 2020

gebner Oct 7, 2020

jcommelin Oct 7, 2020

gebner Oct 7, 2020

bryangingechen Oct 7, 2020

gebner commented Oct 7, 2020

bors bot commented Oct 7, 2020

gebner commented Oct 7, 2020

eric-wieser Oct 7, 2020 •

edited

bryangingechen Oct 7, 2020

eric-wieser commented Oct 7, 2020

bryangingechen commented Oct 7, 2020

gebner commented Oct 7, 2020

bors bot commented Oct 7, 2020


		- name: check for copyright headers and module docstrings
		run: \|

[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

Conversation

bryangingechen commented Oct 6, 2020 • edited by jcommelin

fpvandoorn commented Oct 6, 2020

bryangingechen commented Oct 7, 2020 • edited

fpvandoorn commented Oct 7, 2020

bryangingechen commented Oct 7, 2020

bryangingechen commented Oct 7, 2020

jcommelin commented Oct 7, 2020

bryangingechen commented Oct 7, 2020

jcommelin left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

gebner commented Oct 7, 2020

bors bot commented Oct 7, 2020

gebner commented Oct 7, 2020

eric-wieser Oct 7, 2020 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

eric-wieser commented Oct 7, 2020

bryangingechen commented Oct 7, 2020

gebner commented Oct 7, 2020

bors bot commented Oct 7, 2020

bryangingechen commented Oct 6, 2020 •

edited by jcommelin

bryangingechen commented Oct 7, 2020 •

edited

eric-wieser Oct 7, 2020 •

edited