mathlib

4db1c72f - ci(scripts/*): linting for copyright, imports, module docstrings, line length (#4486)

ci(scripts/*): linting for copyright, imports, module docstrings, line 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>