Skip to content

bench: get decls by decl range#37240

Draft
thorimur wants to merge 5 commits intoleanprover-community:masterfrom
thorimur:byDeclRange-bench
Draft

bench: get decls by decl range#37240
thorimur wants to merge 5 commits intoleanprover-community:masterfrom
thorimur:byDeclRange-bench

Conversation

@thorimur
Copy link
Contributor

For benching.


Open in Gitpod

Copy link
Contributor Author

@thorimur thorimur left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

.

@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Mar 26, 2026
@github-actions
Copy link

github-actions bot commented Mar 26, 2026

PR summary 57d1f5519b

Import changes exceeding 2%

% File
+12.00% Mathlib.Init

Import changes for modified files

Dependency changes

File Base Count Head Count Change
Mathlib.Init 50 56 +6 (+12.00%)
Mathlib.Tactic 3117 3123 +6 (+0.19%)
Import changes for all files
Files Import difference
There are 7801 files with changed transitive imports taking up over 338002 characters: this is too many to display!
You can run ci-tools/scripts/pr_summary/import_trans_difference.sh all locally to see the whole output.

Declarations diff

+ getNamesAndRanges
+ workLinter

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

@github-actions github-actions bot added the t-linter Linter label Mar 26, 2026
@thorimur
Copy link
Contributor Author

!bench

@leanprover-radar
Copy link

leanprover-radar commented Mar 26, 2026

Benchmark results for d5187cb against 57d1f55 are in. There are no significant changes. @thorimur

  • 🟥 build//instructions: +134.8G (+0.08%)

Small changes (1✅)

  • build/module/Mathlib.RingTheory.KrullDimension.Polynomial//instructions: -390.9M (-2.23%)

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

Labels

large-import Automatically added label for PRs with a significant increase in transitive imports t-linter Linter

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants