Skip to content

chore: try to change argument order#38038

Closed
sgouezel wants to merge 2 commits intoleanprover-community:masterfrom
sgouezel:SG_testCore
Closed

chore: try to change argument order#38038
sgouezel wants to merge 2 commits intoleanprover-community:masterfrom
sgouezel:SG_testCore

Conversation

@sgouezel
Copy link
Copy Markdown
Contributor


Open in Gitpod

@sgouezel sgouezel marked this pull request as draft April 14, 2026 11:27
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 14, 2026

This pull request is now in draft mode. No active bors state needed cleanup.

While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like bors r+ or bors try.

@github-actions
Copy link
Copy Markdown

PR summary 50d5513e83

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ foo
+ foot
+ instNormedAddCommGroup1
+ instNormedAddCommGroup2
+ instNormedAddCommGroup3
+ instNormedAddCommGroup4
- instNormedAddCommGroup

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.


Decrease in tech debt: (relative, absolute) = (2.31, 0.01)
Current number Change Type
6752 -1 backward.isDefEq.respectTransparency
800 -5 backward.privateInPublic
414 -1 backward.privateInPublic.warn

Current commit ec782f4506
Reference commit 50d5513e83

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

@github-actions github-actions bot added the t-analysis Analysis (normed *, calculus) label Apr 14, 2026
@sgouezel sgouezel closed this Apr 14, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

t-analysis Analysis (normed *, calculus)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants