Skip to content

Commit

Permalink
fix: count long files, instead of printing all of them (leanprover-co…
Browse files Browse the repository at this point in the history
  • Loading branch information
adomani committed Sep 3, 2024
1 parent 8525fd6 commit 3a97fe9
Showing 1 changed file with 2 additions and 3 deletions.
5 changes: 2 additions & 3 deletions scripts/technical-debt-metrics.sh
Original file line number Diff line number Diff line change
Expand Up @@ -54,9 +54,8 @@ for i in ${!titlesAndRegexes[@]}; do
done

printf '%s|%s\n' "$(grep -c 'docBlame' scripts/nolints.json)" "documentation nolint entries"
# the exceptions for files exceeding the 1500 line limit are split between the `longFile` and
# the text-based linters.
printf '%s|%s\n' "$(grep -c '^set_option linter.style.longFile [0-9]*' $(git ls-files '*.lean'))" "large files"
# We count the number of large files, making sure to avoid counting the test file `test/Lint.lean`.
printf '%s|%s\n' "$(git grep '^set_option linter.style.longFile [0-9]*' Mathlib | wc -l)" "large files"
printf '%s|%s\n' "$(git grep "^open .*Classical" | grep -v " in$" -c)" "bare open (scoped) Classical"
# We print the number of files, not the number of matches --- hence, the nested grep.
printf '%s|%s\n' "$(git grep -c 'autoImplicit true' | grep -c -v 'test')" "non-test files with autoImplicit true"
Expand Down

0 comments on commit 3a97fe9

Please sign in to comment.