chore: port tech debt metrics to Python#60
Open
Vierkantor wants to merge 2 commits into
Open
Conversation
This PR ports the technical debt reporting script to Python, keeping its behaviour as close as possible to the original. I had a hard time working on the shell script, especially because it was written in a non-portable version of Bash. (In other words, MacOS users could not run it on their machines!) The ported script should run portably on computers with Python 3.6 or higher. The shell script is now a thin wrapper around the Python script, for backwards compatibility, and could be removed eventually. I tested this script in PR report mode and weekly Zulip message mode, checking that GitHub and Zulip render the results identically (modulo some newlines and fixed bugs). This is what took most of my development time. A few bugs were fixed in the process, see the `FIXED:` comments. There are still a few bugs left in the script that would need some more substantial refactors to fix, see the `TODO:` comments. Those will be work for future PRs.
adomani
reviewed
Jul 14, 2026
|
|
||
| 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|strong\n' "$({ git grep -c 'set_option warning.simp.varHead false' -- Mathlib Archive Counterexamples || true; } | awk -F: 'BEGIN{s=0}{s+=$2} END{print s}')" "disabled varHead simp warnings" |
Contributor
There was a problem hiding this comment.
Has this check disappeared? Is it intentional?
Contributor
Author
There was a problem hiding this comment.
Good point, it was not in the original sorted list of tech debt items so that must be the reason I missed it. I'll put it back in the list at a place where it seems to belong.
Contributor
|
Other than the dropped check, everything else looks good! Note that I used substantial input from AI to help in the review, and, after extensive back and forth, the dropped stat above is the only flagged issue! |
Contributor
Author
|
Thanks for the review! |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR ports the technical debt reporting script to Python, keeping its behaviour as close as possible to the original. I had a hard time working on the shell script, especially because it was written in a non-portable version of Bash. (In other words, MacOS users could not run it on their machines!) The ported script should run portably on computers with Python 3.6 or higher. The shell script is now a thin wrapper around the Python script, for backwards compatibility, and could be removed eventually.
I tested this script in PR report mode and weekly Zulip message mode, checking that GitHub and Zulip render the results identically (modulo some newlines and fixed bugs). This is what took most of my development time.
A few bugs were fixed in the process, see the
FIXED:comments. There are still a few bugs left in the script that would need some more substantial refactors to fix, see theTODO:comments. Those will be work for future PRs.