Skip to content

ci: add tech debt label#40601

Open
BoltonBailey wants to merge 4 commits into
leanprover-community:masterfrom
BoltonBailey:ci-add-tech-debt-label
Open

ci: add tech debt label#40601
BoltonBailey wants to merge 4 commits into
leanprover-community:masterfrom
BoltonBailey:ci-add-tech-debt-label

Conversation

@BoltonBailey

@BoltonBailey BoltonBailey commented Jun 14, 2026

Copy link
Copy Markdown
Collaborator

This PR adds a step to the PR summary bot to make it add the "tech debt" label to PRs that decrease tech debt.

This PR was made with the assistance of Claude code

Thanks to Felix for this idea. Zulip discussion here #mathlib4 > Technical Debt Counters @ 💬


Open in Gitpod

@BoltonBailey BoltonBailey added the LLM-generated PRs with substantial input from LLMs - review accordingly label Jun 14, 2026
@github-actions

github-actions Bot commented Jun 14, 2026

Copy link
Copy Markdown

PR summary 1049e60a54

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff (regex)

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

You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.


No changes to strong technical debt.

No changes to weak technical debt.

Current commit 1049e60a54
Reference commit 77760d482b

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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

@github-actions github-actions Bot added the CI Modifies the continuous integration setup or other automation label Jun 14, 2026
@BoltonBailey BoltonBailey added the WIP Work in progress label Jun 14, 2026
Comment thread .github/workflows/PR_summary.yml
BoltonBailey and others added 2 commits June 14, 2026 14:34
Restore Mathlib/Analysis/Normed/Group/Basic.lean and
scripts/nolints_prime_decls.txt to their master state, keeping only
the CI workflow change on this branch.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@BoltonBailey BoltonBailey removed the WIP Work in progress label Jun 14, 2026
@BoltonBailey

Copy link
Copy Markdown
Collaborator Author

Presumably I can't actually test that this works because security dictates that the PR summary workflow label control should only act on maintainer approved changes. Nevertheless, it seems to me like it should work.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

CI Modifies the continuous integration setup or other automation LLM-generated PRs with substantial input from LLMs - review accordingly

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants