feat: classify tech debt into weak and strong#28
Conversation
This PR adds a "level" attribute to the tech debt reports posted weekly on Zulip and under every PR. The intention is that "weak" tech debt is allowed to increase in a PR (when reasonable), while "strong" tech debt should only increase in exceptional cases (for example, Lean updates or because we expose a new source of tech debt). I played around with a few formatting options for the report and settled on this one: show the strong tech debt and then the weak tech debt in two different tables. That should make it clear for the reader (and possible automation) if we care about a particular change or not.
grunweg
left a comment
grunweg
left a comment
There was a problem hiding this comment.
I have two comments about the classification of tech debt counts. (I did not look at the shell/awk changes carefully.)
| grep -c "deprecated .*(since")" | ||
|
|
||
| printf '%s|disabled deprecation lints\n' "$(( deprecs - doubleDeprecs ))" | ||
| printf '%s|disabled deprecation lints|strong\n' "$(( deprecs - doubleDeprecs ))" |
There was a problem hiding this comment.
As long as lean#13595 is not merged yet, this check will have false positives. Perhaps that's fine for a two-week window, but perhaps this should start as "weak" (and be changed to "strong" in two weeks)?
There was a problem hiding this comment.
It should be easy enough to change the category later, so:
| printf '%s|disabled deprecation lints|strong\n' "$(( deprecs - doubleDeprecs ))" | |
| printf '%s|disabled deprecation lints|weak\n' "$(( deprecs - doubleDeprecs ))" # TODO: upgrade to strong after false positives are fixed, https://github.com/leanprover/lean4/pull/13595 |
| printf '%s|%s|weak\n' "$(git grep '^set_option linter.style.longFile [0-9]*' Mathlib | wc -l)" "large files" | ||
|
|
||
| printf '%s|%s\n' "$(wc -l < scripts/nolints_prime_decls.txt)" "exceptions for the docPrime linter" | ||
| printf '%s|%s|strong\n' "$(wc -l < scripts/nolints_prime_decls.txt)" "exceptions for the docPrime linter" |
There was a problem hiding this comment.
Given this list is effectively not updated, I'm unsure if this reflects reality. (But it's not actively doing harm either.)
There was a problem hiding this comment.
Hmm, good point. Maybe we should instead count the set_option linter.docPrime false lines?
There was a problem hiding this comment.
(I mean, adding the line count of this file to the count of set_option linter.docPrime false. The list is used by the linter for skipping exceptions.)
There was a problem hiding this comment.
We can count just set_option linter.docPrime false (these shouldn't be introduced)... but ultimate, I don't think this items needs much thought right now, given the linter is disabled.
|
Also, let me say thank you for starting this --- I think this can be very useful! |
3 participants
This PR adds a "level" attribute to the tech debt reports posted weekly on Zulip and under every PR. The intention is that "weak" tech debt is allowed to increase in a PR (when reasonable), while "strong" tech debt should only increase in exceptional cases (for example, Lean updates or because we expose a new source of tech debt).
I played around with a few formatting options for the report and settled on this one: show the strong tech debt and then the weak tech debt in two different tables. That should make it clear for the reader (and possible automation) if we care about a particular change or not.