feat: remove lint-style.sh (#15051)

In detail, this PR
- moves the executable bit check into the .yml files, instead of the shell script
- adds a `--fix` flag to `lint-style`, for fixing style errors (when possible)
- moves calling `lint-style.py` into `lake exe lint-style`, and
- switches the CI workflow to call `lake exe lint-style` instead, and removes `lint-style.sh`

Ideally, `lint-style.py` will be completely rewritten in Lean soon, so this calling of an external process is only temporary.

Helps with #14539.

.github/workflows/bors.yml

@@ -44,6 +44,17 @@ jobs:
       - name: Look for ignored files
         uses: credfeto/[email protected]
 
+      - 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' }}

.github/workflows/build.yml

@@ -51,6 +51,17 @@ jobs:
       - name: Look for ignored files
         uses: credfeto/[email protected]
 
+      - 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' }}

.github/workflows/build.yml.in

@@ -30,6 +30,17 @@ jobs:
       - name: Look for ignored files
         uses: credfeto/[email protected]
 
+      - 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' }}

.github/workflows/build_fork.yml

@@ -48,6 +48,17 @@ jobs:
       - name: Look for ignored files
         uses: credfeto/[email protected]
 
+      - 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' }}

.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

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\

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

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