feat(scripts/lint-style.sh): check that Lean files don't have executa…

…ble bit (#5606)

scripts/lint-style.sh

@@ -1,5 +1,7 @@
 #!/usr/bin/env bash
 
+set -exo pipefail
+
 # # Style linter
 
 # ## Usage
@@ -20,11 +22,31 @@
 
 # ## Implementation details
 
-# 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`.
+# 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`.
+# 2. The remainder of this shell script
+#    contains some lints on the global repository.
+
+################################################################################
+
+# 1. Call the Lean file linter, implemented in Python
 
 touch scripts/style-exceptions.txt
 
 find src archive -name '*.lean' | xargs ./scripts/lint-style.py
 
+# 2. Global checks on the mathlib repository
+
+# 2.1 Check for executable bit on Lean files
+
+executable_files="$(find . -name '*.lean' -type f -executable)"
+
+if [[ -n "$executable_files" ]]
+then
+	echo "ERROR: The following Lean files have the executable bit set."
+	echo "$executable_files"
+	exit 1
+fi
+