From 01e17a9d8e48a9b1b36fd4f1d26922bf687d0193 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Tue, 5 Jan 2021 18:04:51 +0000 Subject: [PATCH] feat(scripts/lint-style.sh): check that Lean files don't have executable bit (#5606) --- scripts/lint-style.sh | 28 +++++++++++++++++-- .../computation/approximations.lean | 0 .../computation/basic.lean | 0 .../computation/correctness_terminating.lean | 0 .../computation/translations.lean | 0 src/topology/path_connected.lean | 0 6 files changed, 25 insertions(+), 3 deletions(-) mode change 100755 => 100644 src/algebra/continued_fractions/computation/approximations.lean mode change 100755 => 100644 src/algebra/continued_fractions/computation/basic.lean mode change 100755 => 100644 src/algebra/continued_fractions/computation/correctness_terminating.lean mode change 100755 => 100644 src/algebra/continued_fractions/computation/translations.lean mode change 100755 => 100644 src/topology/path_connected.lean 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