Relative technical debt in PRs

Stream: mathlib4

[Damiano Testa]

As of a couple of minutes ago, the PR summary comment that is automatically added to PRs should contain a final tab summarizing the change in technical debt of the PR.

[Damiano Testa]

The statistics are the same as the ones used by the weekly Technical Debt Report.

[Damiano Testa]

Most PRs will say No changes to technical debt., but some may have a report of something that changed.

[Damiano Testa]

If you notice any strange behaviour associated with this new summary, please report it! In particular, every PR that uses the action that is on current master should have this section, so a missing section might also be a bug (or simply a weird GitHub issue that used an old workflow for a new PR).

[Damiano Testa]

Looking at the PRs, the most common issue that arises is that CI reports a failure in the Post PR summary comment step. This is most likely due to the fact that the file that contains the script is "old", while the action that CI runs assumes that it has the "new" script. In such cases, simply merging the current version of master and pushing again should resolve the issue.

[Anne Baanen]

This is a great addition, thanks Damiano! However, I think it might be easy to overlook the tech debt message when first opening a PR. What do you think of a label that gets added to a PR if it increases a tech debt counter?

[Damiano Testa]

I am indeed heading in that direction: exposing the "weighted" technical debt change is a test to see whether adding a label would make sense.

[Anne Baanen]

Great :D

[Damiano Testa]

(Btw, all this automation is joint with Johan.)

[Damiano Testa]

So, basically, I want to see that the measure that is currently used is a good heuristic to add a tech-debt-increase/decrease label.