diff --git a/.github/workflows/bors.yml b/.github/workflows/bors.yml index e3a683620ffa6..c5a421e26f3ef 100644 --- a/.github/workflows/bors.yml +++ b/.github/workflows/bors.yml @@ -44,6 +44,17 @@ jobs: - name: Look for ignored files uses: credfeto/action-no-ignored-files@v1.1.0 + - name: "Check for Lean files with the executable bit set" + shell: bash + run: | + executable_files="$(find . -name '*.lean' -type f \( -perm -u=x -o -perm -g=x -o -perm -o=x \))" + if [[ -n "$executable_files" ]] + then + echo "ERROR: The following Lean files have the executable bit set." + echo "$executable_files" + exit 1 + fi + - name: install Python if: ${{ 'bors' == 'ubuntu-latest' }} uses: actions/setup-python@v5 @@ -57,9 +68,9 @@ jobs: ./elan-init -y --default-toolchain none echo "$HOME/.elan/bin" >> "${GITHUB_PATH}" - - name: "run style linters: Python ones and their Lean rewrite" + - name: "run style linters" run: | - ./scripts/lint-style.sh + lake exe lint-style - name: Install bibtool if: ${{ 'bors' == 'ubuntu-latest' }} diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 6bceb029713e4..bbeef2b24530e 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -51,6 +51,17 @@ jobs: - name: Look for ignored files uses: credfeto/action-no-ignored-files@v1.1.0 + - name: "Check for Lean files with the executable bit set" + shell: bash + run: | + executable_files="$(find . -name '*.lean' -type f \( -perm -u=x -o -perm -g=x -o -perm -o=x \))" + if [[ -n "$executable_files" ]] + then + echo "ERROR: The following Lean files have the executable bit set." + echo "$executable_files" + exit 1 + fi + - name: install Python if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }} uses: actions/setup-python@v5 @@ -64,9 +75,9 @@ jobs: ./elan-init -y --default-toolchain none echo "$HOME/.elan/bin" >> "${GITHUB_PATH}" - - name: "run style linters: Python ones and their Lean rewrite" + - name: "run style linters" run: | - ./scripts/lint-style.sh + lake exe lint-style - name: Install bibtool if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }} diff --git a/.github/workflows/build.yml.in b/.github/workflows/build.yml.in index 02dd04d95f5f5..37ec2538a43ce 100644 --- a/.github/workflows/build.yml.in +++ b/.github/workflows/build.yml.in @@ -30,6 +30,17 @@ jobs: - name: Look for ignored files uses: credfeto/action-no-ignored-files@v1.1.0 + - name: "Check for Lean files with the executable bit set" + shell: bash + run: | + executable_files="$(find . -name '*.lean' -type f \( -perm -u=x -o -perm -g=x -o -perm -o=x \))" + if [[ -n "$executable_files" ]] + then + echo "ERROR: The following Lean files have the executable bit set." + echo "$executable_files" + exit 1 + fi + - name: install Python if: ${{ 'STYLE_LINT_RUNNER' == 'ubuntu-latest' }} uses: actions/setup-python@v5 @@ -43,9 +54,9 @@ jobs: ./elan-init -y --default-toolchain none echo "$HOME/.elan/bin" >> "${GITHUB_PATH}" - - name: "run style linters: Python ones and their Lean rewrite" + - name: "run style linters" run: | - ./scripts/lint-style.sh + lake exe lint-style - name: Install bibtool if: ${{ 'STYLE_LINT_RUNNER' == 'ubuntu-latest' }} diff --git a/.github/workflows/build_fork.yml b/.github/workflows/build_fork.yml index 344c91f9a8747..0a2c6fe778dfc 100644 --- a/.github/workflows/build_fork.yml +++ b/.github/workflows/build_fork.yml @@ -48,6 +48,17 @@ jobs: - name: Look for ignored files uses: credfeto/action-no-ignored-files@v1.1.0 + - name: "Check for Lean files with the executable bit set" + shell: bash + run: | + executable_files="$(find . -name '*.lean' -type f \( -perm -u=x -o -perm -g=x -o -perm -o=x \))" + if [[ -n "$executable_files" ]] + then + echo "ERROR: The following Lean files have the executable bit set." + echo "$executable_files" + exit 1 + fi + - name: install Python if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }} uses: actions/setup-python@v5 @@ -61,9 +72,9 @@ jobs: ./elan-init -y --default-toolchain none echo "$HOME/.elan/bin" >> "${GITHUB_PATH}" - - name: "run style linters: Python ones and their Lean rewrite" + - name: "run style linters" run: | - ./scripts/lint-style.sh + lake exe lint-style - name: Install bibtool if: ${{ 'ubuntu-latest' == 'ubuntu-latest' }} diff --git a/.github/workflows/lint_and_suggest_pr.yml b/.github/workflows/lint_and_suggest_pr.yml index 64f06540402cd..52888f7128e32 100644 --- a/.github/workflows/lint_and_suggest_pr.yml +++ b/.github/workflows/lint_and_suggest_pr.yml @@ -31,7 +31,7 @@ jobs: - name: lint continue-on-error: true # allows the following `reviewdog` step to add GitHub suggestions run: | - ./scripts/lint-style.sh --fix + lake exe lint-style --fix - name: suggester / lint-style uses: reviewdog/action-suggester@v1 diff --git a/Mathlib/Tactic/Linter/TextBased.lean b/Mathlib/Tactic/Linter/TextBased.lean index 38204f9292cc3..544f44eb1d63c 100644 --- a/Mathlib/Tactic/Linter/TextBased.lean +++ b/Mathlib/Tactic/Linter/TextBased.lean @@ -11,11 +11,21 @@ import Mathlib.Data.Nat.Notation ## Text-based linters This file defines various mathlib linters which are based on reading the source code only. -In practice, only style linters will have this form. -All of these have been rewritten from the `lint-style.py` script. +In practice, all such linters check for code style issues. -For now, this only contains the linters for the copyright and author headers and large files: -further linters will be ported in subsequent PRs. +For now, this only contains linters checking +- that the copyright header and authors line are correctly formatted +- existence of module docstrings (in the right place) +- for certain disallowed imports +- if the string "adaptation note" is used instead of the command #adaptation_note +- lines are at most 100 characters long (except for URLs) +- files are at most 1500 lines long (unless specifically allowed). + +For historic reasons, some of these checks are still written in a Python script `lint-style.py`: +these are gradually being rewritten in Lean. + +This linter maintains a list of exceptions, for legacy reasons. +Ideally, the length of the list of exceptions tends to 0. An executable running all these linters is defined in `scripts/lint-style.lean`. -/ @@ -392,7 +402,6 @@ def lintFile (path : FilePath) (sizeLimit : Option ℕ) (exceptions : Array Erro IO (Array ErrorContext) := do let lines ← IO.FS.lines path -- We don't need to run any checks on imports-only files. - -- NB. The Python script used to still run a few linters; this is in fact not necessary. if isImportsOnlyFile lines then return #[] let mut errors := #[] @@ -409,8 +418,9 @@ Print formatted errors for all unexpected style violations to standard output; update the list of style exceptions if configured so. Return the number of files which had new style errors. `moduleNames` are all the modules to lint, -`mode` specifies what kind of output this script should produce. -/ -def lintModules (moduleNames : Array String) (mode : OutputSetting) : IO UInt32 := do +`mode` specifies what kind of output this script should produce, +`fix` configures whether fixable errors should be corrected in-place. -/ +def lintModules (moduleNames : Array String) (mode : OutputSetting) (fix : Bool) : IO UInt32 := do -- Read the style exceptions file. -- We also have a `nolints` file with manual exceptions for the linter. let exceptionsFilePath : FilePath := "scripts" / "style-exceptions.txt" @@ -441,6 +451,12 @@ def lintModules (moduleNames : Array String) (mode : OutputSetting) : IO UInt32 numberErrorFiles := numberErrorFiles + 1 match mode with | OutputSetting.print style => + -- Run the remaining python linters. It is easier to just run on all files. + -- If this poses an issue, I can either filter the output + -- or wait until lint-style.py is fully rewritten in Lean. + let args := if fix then #["--fix"] else #[] + let pythonOutput ← IO.Process.run { cmd := "./scripts/print-style-errors.sh", args := args } + if pythonOutput != "" then IO.println pythonOutput formatErrors allUnexpectedErrors style if numberErrorFiles > 0 && mode matches OutputSetting.print _ then IO.println s!"error: found {allUnexpectedErrors.size} new style errors\n\ diff --git a/scripts/lint-style.lean b/scripts/lint-style.lean index 6367daa796ac2..5c7ab0d34064f 100644 --- a/scripts/lint-style.lean +++ b/scripts/lint-style.lean @@ -25,10 +25,10 @@ def lintStyleCli (args : Cli.Parsed) : IO UInt32 := do -- Read all module names to lint. let mut allModules := #[] for s in ["Archive.lean", "Counterexamples.lean", "Mathlib.lean"] do - -- note: since we manually add "Batteries" to "Mathlib.lean", we remove it here manually - allModules := allModules.append ((← IO.FS.lines s).filter (!·.containsSubstr "Batteries") - |>.map (·.stripPrefix "import ")) - let numberErrorFiles ← lintModules allModules mode + allModules := allModules.append ((← IO.FS.lines s).map (·.stripPrefix "import ")) + -- note: since we manually add "Batteries" to "Mathlib.lean", we remove it here manually + allModules := allModules.erase "Batteries" + let numberErrorFiles ← lintModules allModules mode (args.hasFlag "fix") -- Make sure to return an exit code of at most 125, so this return value can be used further -- in shell scripts. return min numberErrorFiles 125 @@ -48,6 +48,7 @@ def lintStyle : Cmd := `[Cli| and tries to not modify exception entries unless necessary. To fully regenerate the list of style exceptions, delete `style-exceptions.txt` and run this script again with this flag." + fix; "Automatically fix the style error, if possible" ] /-- The entry point to the `lake exe lint-style` command. -/ diff --git a/scripts/lint-style.sh b/scripts/lint-style.sh deleted file mode 100755 index 91d550ab65b55..0000000000000 --- a/scripts/lint-style.sh +++ /dev/null @@ -1,57 +0,0 @@ -#!/usr/bin/env bash - -set -exo pipefail - -# # Style linter - -# ## Usage - -# Run this script from the root of mathlib using: -# ./scripts/lint-style.sh - -# ## Purpose - -# The style linter checks for new style issues, -# and maintains a list of exceptions for legacy reasons. -# Ideally, the length of the list of exceptions tends to 0. - -# Examples of issues that are checked for are: -# * existence of copyright header -# * existence of module docstrings (in the right place) -# * line length <= 100 (unless URL) - -# ## Implementation details - -# There are two parts. -# 1. A Python script `scripts/lint-style.py` that lints the contents of a Lean file. -# This script is called below on all Lean files in the repository. -# Exceptions are maintained in `scripts/style-exceptions.txt`. -# (Rewriting these checks in Lean is work in progress.) -# 2. The remainder of this shell script -# contains a lint on the global repository. -# -# TODO: This is adapted from the linter for mathlib3. It should be rewritten in Lean. - -################################################################################ - -# 1. Call the Lean file linter, implemented in Python - -touch scripts/style-exceptions.txt - -git ls-files 'Mathlib/*.lean' | xargs ./scripts/lint-style.py "$@" -git ls-files 'Archive/*.lean' | xargs ./scripts/lint-style.py "$@" -git ls-files 'Counterexamples/*.lean' | xargs ./scripts/lint-style.py "$@" - -# Call the in-progress Lean rewrite of these Python lints. -lake exe lint-style --github - -# 2. Global checks on the mathlib repository - -executable_files="$(find . -name '*.lean' -type f \( -perm -u=x -o -perm -g=x -o -perm -o=x \))" - -if [[ -n "$executable_files" ]] -then - echo "ERROR: The following Lean files have the executable bit set." - echo "$executable_files" - exit 1 -fi diff --git a/scripts/print-style-errors.sh b/scripts/print-style-errors.sh index 1eda2b5b93663..f9a9e1c1b42c8 100755 --- a/scripts/print-style-errors.sh +++ b/scripts/print-style-errors.sh @@ -7,3 +7,5 @@ # use C locale so that sorting is the same on macOS and Linux # see https://unix.stackexchange.com/questions/362728/why-does-gnu-sort-sort-differently-on-my-osx-machine-and-linux-machine find Mathlib -name '*.lean' | xargs ./scripts/lint-style.py | LC_ALL=C sort +find Archive -name '*.lean' | xargs ./scripts/lint-style.py | LC_ALL=C sort +find Counterexamples -name '*.lean' | xargs ./scripts/lint-style.py | LC_ALL=C sort