Skip to content

Commit

Permalink
fix: do not count un-deprecations in Mathlib/Deprecated (#19184)
Browse files Browse the repository at this point in the history
  • Loading branch information
adomani committed Nov 18, 2024
1 parent 5ebc4a6 commit 7b79131
Showing 1 changed file with 11 additions and 1 deletion.
12 changes: 11 additions & 1 deletion scripts/technical-debt-metrics.sh
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,6 @@ titlesPathsAndRegexes=(
"skipAssignedInstances flags" "*" "set_option tactic.skipAssignedInstances"
"adaptation notes" "*" "adaptation_note"
"disabled simpNF lints" "*" "nolint simpNF"
"disabled deprecation lints" "*" "set_option linter.deprecated false"
"erw" "*" "erw \["
"maxHeartBeats modifications" ":^MathlibTest" "^ *set_option .*maxHeartbeats"
)
Expand All @@ -98,6 +97,17 @@ for i in ${!titlesPathsAndRegexes[@]}; do
fi
done

# count total number of `set_option linter.deprecated false` outside of `Mathlib/Deprecated`
deprecs="$(git grep -c -- "set_option linter.deprecated false" -- ":^Mathlib/Deprecated" |
awk -F: 'BEGIN{total=0} {total+=$2} END{print total}')"

# count the `linter.deprecated` exceptions that are themselves followed by `deprecated ...(since`
# we subtract these from `deprecs`
doubleDeprecs="$(git grep -A1 -- "set_option linter.deprecated false" -- ":^Mathlib/Deprecated" |
grep -c "deprecated .*(since")"

printf '%s|disabled deprecation lints\n' "$(( deprecs - doubleDeprecs ))"

printf '%s|%s\n' "$(grep -c 'docBlame' scripts/nolints.json)" "documentation nolint entries"
# We count the number of large files, making sure to avoid counting the test file `MathlibTest/Lint.lean`.
printf '%s|%s\n' "$(git grep '^set_option linter.style.longFile [0-9]*' Mathlib | wc -l)" "large files"
Expand Down

0 comments on commit 7b79131

Please sign in to comment.