Skip to content

[Merged by Bors] - chore: reduce use of backward.privateInPublic option#33089

Closed
grunweg wants to merge 2 commits intoleanprover-community:masterfrom
grunweg:privacy
Closed

[Merged by Bors] - chore: reduce use of backward.privateInPublic option#33089
grunweg wants to merge 2 commits intoleanprover-community:masterfrom
grunweg:privacy

Conversation

@grunweg
Copy link
Collaborator

@grunweg grunweg commented Dec 19, 2025


Open in Gitpod

@grunweg grunweg added the tech debt Tracking cross-cutting technical debt, see e.g. the "Technical debt counters" stream on zulip label Dec 19, 2025
@github-actions github-actions bot added the t-data Data (lists, quotients, numbers, etc) label Dec 19, 2025
@github-actions
Copy link

github-actions bot commented Dec 19, 2025

PR summary c7f3e346ed

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

- xgcdAux_P

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.


Decrease in tech debt: (relative, absolute) = (3.00, 0.00)
Current number Change Type
1551 -3 backwards compatibility flags
1504 -3 privateInPublic flags

Current commit 34e50e4c8e
Reference commit c7f3e346ed

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

@grunweg grunweg added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Dec 19, 2025
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Dec 19, 2025
@jcommelin
Copy link
Member

Thanks 🎉

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Dec 19, 2025
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Dec 19, 2025

This PR was included in a batch that was canceled, it will be automatically retried

@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Dec 19, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: reduce use of backward.privateInPublic option [Merged by Bors] - chore: reduce use of backward.privateInPublic option Dec 19, 2025
@mathlib-bors mathlib-bors bot closed this Dec 19, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

ready-to-merge This PR has been sent to bors. 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.

2 participants