ci: block merging PRs that increase technical debt unless reviewed

[kim-em]

This PR adds a merge gate for technical debt increases.

When the existing technical debt metrics script reports an increase, the build job adds an increases-technical-debt label. A check-technical-debt job then adds blocked-by-increases-technical-debt, which blocks bors.

A reviewer can add allow-increases-technical-debt to unblock after confirming the increase is acceptable.

Fail-closed detection

The detection greps for the safe patterns (Decrease in tech debt: / No changes to technical debt.) rather than for Increase. If mathlib-ci changes the script's output wording, the label is added (fail closed) rather than silently skipped (fail open).

Labels (three-label pattern, same as #38225)

Label	Managed by	Purpose
increases-technical-debt	build job (tech debt script)	Factual: this PR increases debt
blocked-by-increases-technical-debt	check-technical-debt job	Operational: blocks bors
allow-increases-technical-debt	Reviewer	Override: reviewer approves the increase

Bors's block_labels has no conditional logic, so we need the derived blocked-by-increases-technical-debt label to express the conjunction "increases-technical-debt AND NOT allow-increases-technical-debt".

False positives can be reported on the mathlib4 Zulip.

🤖 Prepared with Claude Code

---

• depends on: feat: classify tech debt into weak and strong mathlib-ci#28

[github-actions]

PR summary 98261a9c88

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

---

⚠️ Workflow documentation reminder

This PR modifies files under .github/workflows/.
Please update docs/workflows.md if the workflow inventory, triggers, or behavior changed.

Modified workflow files:

• .github/workflows/PR_summary.yml

[jcommelin]

I think this might need to be more fine-grained, with an allow- and/or deny-list.
Otherwise we risk that adding the allow- label becomes routine, whereas we want it to be for exceptional cases.

Eg, long files tech debt is currently working really well. So I would like to take it out of this feature.

[joneugster]

Same here as in #38225, I fail to see the point of warning the reviewer and requesting them to confirm they've seen the warning. That's the reviewer's job. (but this concern should probably be discussed in #38225 or any linked discussion in that PR, in order not to duplicate discussions)

[kim-em]

I think this might need to be more fine-grained, with an allow- and/or deny-list. Otherwise we risk that adding the allow- label becomes routine, whereas we want it to be for exceptional cases.

Eg, long files tech debt is currently working really well. So I would like to take it out of this feature.

Johan and I discussed a split of the technical debt reports into "hard" and "soft" categories. I'm waiting to hear back on that being finalized, and then I or someone else can update this PR to only react to "hard" technical debt increases.

[joneugster]

#mathlib reviewers > Strong and weak tech debt

[grunweg]

My understanding is that this PR is blocked on such a splitting; let me label it accordingly. I've left a review comment on mathlib-ci#28 about the splitting of metrics.

[mathlib-dependent-issues]

This PR/issue depends on:

• feat: classify tech debt into weak and strong mathlib-ci#28
  By Dependent Issues (🤖). Happy coding!