Skip to content

Commit

Permalink
CI: add deprecated files to tech debts counters (#15853)
Browse files Browse the repository at this point in the history
Adds information about the `Deprecated` folder to the technical debt report.

[Asked on Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Technical.20Debt.20Counters/near/462615354)
  • Loading branch information
adomani authored and bjoernkjoshanssen committed Sep 9, 2024
1 parent b14d895 commit cd83888
Showing 1 changed file with 5 additions and 0 deletions.
5 changes: 5 additions & 0 deletions scripts/technical-debt-metrics.sh
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,11 @@ printf '%s|%s\n' "$(git grep "^open .*Classical" | grep -v " in$" -c)" "bare ope
# 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"

deprecatedFiles="$(git ls-files '**/Deprecated/*.lean' | xargs wc -l | sed 's=^ *==')"

printf '%s|%s\n' "$(printf '%s' "${deprecatedFiles}" | wc -l)" "\`Deprecated\` files"
printf '%s|%s\n' "$(printf '%s\n' "${deprecatedFiles}" | grep total | sed 's= total==')" 'total LoC in `Deprecated` files'

initFiles="$(git ls-files '**/Init/*.lean' | xargs wc -l | sed 's=^ *==')"

printf '%s|%s\n' "$(printf '%s' "${initFiles}" | wc -l)" "\`Init\` files"
Expand Down

0 comments on commit cd83888

Please sign in to comment.