-
Notifications
You must be signed in to change notification settings - Fork 259
/
lint-style.sh
executable file
·57 lines (40 loc) · 1.73 KB
/
lint-style.sh
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
#!/usr/bin/env bash
set -exo pipefail
# # Style linter
# ## Usage
# Run this script from the root of mathlib using:
# ./scripts/lint-style.sh
# ## Purpose
# The style linter checks for new style issues,
# and maintains a list of exceptions for legacy reasons.
# Ideally, the length of the list of exceptions tends to 0.
# Examples of issues that are checked for are:
# * existence of copyright header
# * existence of module docstrings (in the right place)
# * line length <= 100 (unless URL)
# ## Implementation details
# 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`.
# (Rewriting these checks in Lean is work in progress.)
# 2. The remainder of this shell script
# contains a lint on the global repository.
#
# TODO: This is adapted from the linter for mathlib3. It should be rewritten in Lean.
################################################################################
# 1. Call the Lean file linter, implemented in Python
touch scripts/style-exceptions.txt
git ls-files 'Mathlib/*.lean' | xargs ./scripts/lint-style.py "$@"
git ls-files 'Archive/*.lean' | xargs ./scripts/lint-style.py "$@"
git ls-files 'Counterexamples/*.lean' | xargs ./scripts/lint-style.py "$@"
# Call the in-progress Lean rewrite of these Python lints.
lake exe lint_style --github
# 2. Global checks on the mathlib repository
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