Skip to content

Conversation

@grunweg
Copy link
Collaborator

@grunweg grunweg commented Jan 16, 2026

It is empty now.


Open in Gitpod

@grunweg grunweg added easy < 20s of review time. See the lifecycle page for guidelines. tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip labels Jan 16, 2026
@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Jan 16, 2026
@github-actions
Copy link

PR summary 2b4c6152f1

Import changes exceeding 2%

% File
+4.17% Mathlib.Data.Tree.RBMap

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.Data.Tree.RBMap 48 50 +2 (+4.17%)
Import changes for all files
Files Import difference
Mathlib.Data.Tree.RBMap 2

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/declarations_diff.sh <optional_commit>

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

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


No changes to technical debt.

You can run this locally as

./scripts/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).

@github-actions github-actions bot added the t-data Data (lists, quotients, numbers, etc) label Jan 16, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

easy < 20s of review time. See the lifecycle page for guidelines. large-import Automatically added label for PRs with a significant increase in transitive imports t-data Data (lists, quotients, numbers, etc) tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant