[Merged by Bors] - fix(scripts): make lint-style.* work on macos and windows

.github/workflows/build.yml

@@ -12,6 +12,27 @@ on:
       - 'lean-3.*'
 
 jobs:
+  lint_self_test:
+    name: Ensure the linter works
+    runs-on: ${{ matrix.os }}
+    strategy:
+      fail-fast: false
+      matrix:
+        os: [macos-latest, ubuntu-latest, windows-latest]
+        python-version:
+          - name: 3.8
+          - name: 3.9
+    steps:
+      - uses: actions/checkout@v2
+      - name: Set up Python ${{ matrix.python-version.name }}
+        uses: actions/setup-python@v2
+        with:
+          python-version: ${{ matrix.python-version.name }}
+
+      - name: sanity check the linter
+        run: |
+          ./scripts/lint_style_sanity_test.py
+
   style_lint:
     name: Lint style
     runs-on: ubuntu-latest
@@ -23,10 +44,6 @@ jobs:
         with:
           python-version: 3.8
 
-      - name: sanity check the linter
-        run: |
-          ./scripts/lint_style_sanity_test.py
-
       - name: lint
         run: |
           ./scripts/lint-style.sh

scripts/lint-style.py

@@ -46,7 +46,7 @@
 RESERVED_NOTATION = ROOT_DIR / 'src/tactic/reserved_notation.lean'
 
 
-with SCRIPTS_DIR.joinpath("style-exceptions.txt").open() as f:
+with SCRIPTS_DIR.joinpath("style-exceptions.txt").open(encoding="utf-8") as f:
     for line in f:
         filename, _, _, _, _, errno, *_ = line.split()
         path = ROOT_DIR / filename
@@ -227,7 +227,7 @@ def format_errors(errors):
             output_message(path, line_nr, "ERR_OPT", "Forbidden set_option command")
 
 def lint(path):
-    with path.open() as f:
+    with path.open(encoding="utf-8") as f:
         lines = f.readlines()
         errs = long_lines_check(lines, path)
         format_errors(errs)

scripts/lint-style.sh

@@ -41,7 +41,7 @@ find src archive -name '*.lean' | xargs ./scripts/lint-style.py
 
 # 2.1 Check for executable bit on Lean files
 
-executable_files="$(find . -name '*.lean' -type f -executable)"
+executable_files="$(find . -name '*.lean' -type f \( -perm -u=x -o -perm -g=x -o -perm -o=x \))"
 
 if [[ -n "$executable_files" ]]
 then

scripts/lint_style_sanity_test.py

@@ -1,6 +1,8 @@
 #!/usr/bin/env python3
 from pathlib import Path
-from tempfile import NamedTemporaryFile
+from shutil import copy
+from tempfile import NamedTemporaryFile, TemporaryDirectory
+from textwrap import dedent
 import subprocess
 import unittest
 
@@ -130,7 +132,7 @@ def test_updating_style_exceptions_uses_relative_paths(self):
         self.assertNotIn(str(ROOT_DIR), current_contents)
         self.addCleanup(exceptions.write_text, current_contents)
 
-        result = subprocess.run(
+        subprocess.run(
             ["./scripts/update-style-exceptions.sh"],
             check=True,
             capture_output=True,
@@ -141,5 +143,41 @@ def test_updating_style_exceptions_uses_relative_paths(self):
             SCRIPTS_DIR.joinpath("style-exceptions.txt").read_text(),
         )
 
+    def test_running_the_shell_script_does_not_error(self):
+        """
+        Normally, users will run scripts/lint-style.sh, which will run the
+        linter on all files within mathlib.
+
+        Running it exits with successful return code.
+
+        This test will execute in a separate directory tree to make sure
+        it doesn't fail if there are current style warnings.
+        """
+
+        with TemporaryDirectory() as tmpdir:
+            root = Path(tmpdir)
+            for each in "scripts", "src", "archive":
+                root.joinpath(each).mkdir()
+
+            copy(SCRIPTS_DIR / "lint-style.sh", root / "scripts")
+            copy(SCRIPTS_DIR / "lint-style.py", root / "scripts")
+
+            # Give us at least one file to check
+            root.joinpath("src", "unittesting123.lean").write_text(
+                dedent(
+                    """\
+                    /-
+                    Copyright (c) 2021 Someone. All rights reserved.
+                    Released under Apache 2.0 license as described in the file LICENSE.
+                    Authors: Someone
+                    -/
+                    example : 37 = 37 := rfl
+                    """,
+                )
+            )
+
+            subprocess.run(["./scripts/lint-style.sh"], check=True, cwd=root)
+
+
 if __name__ == "__main__":
-    unittest.main()
+    unittest.main(verbosity=2)