diff --git a/scripts/lint-style.sh b/scripts/lint-style.sh index ed5afa0af27a3..d20887efd340d 100755 --- a/scripts/lint-style.sh +++ b/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 + diff --git a/src/algebra/continued_fractions/computation/approximations.lean b/src/algebra/continued_fractions/computation/approximations.lean old mode 100755 new mode 100644 diff --git a/src/algebra/continued_fractions/computation/basic.lean b/src/algebra/continued_fractions/computation/basic.lean old mode 100755 new mode 100644 diff --git a/src/algebra/continued_fractions/computation/correctness_terminating.lean b/src/algebra/continued_fractions/computation/correctness_terminating.lean old mode 100755 new mode 100644 diff --git a/src/algebra/continued_fractions/computation/translations.lean b/src/algebra/continued_fractions/computation/translations.lean old mode 100755 new mode 100644 diff --git a/src/topology/path_connected.lean b/src/topology/path_connected.lean old mode 100755 new mode 100644