Skip to content

perf: lower priority of NormedAlgebraicFoo -> AlgebraicFoo instances#36844

Closed
grunweg wants to merge 1 commit intoleanprover-community:masterfrom
grunweg:normed-add-prio
Closed

perf: lower priority of NormedAlgebraicFoo -> AlgebraicFoo instances#36844
grunweg wants to merge 1 commit intoleanprover-community:masterfrom
grunweg:normed-add-prio

Conversation

@grunweg
Copy link
Copy Markdown
Contributor

@grunweg grunweg commented Mar 19, 2026

We never unbundled the normed and algebra hierarchies, and this is causing performance problems in #36299 and friends. Try if lowering the respective instance priorities helps.


Open in Gitpod

We never unbundled the normed and algebra hierarchies, and this is causing
performance problems in leanprover-community#36299 and friends. Try if lowering the respective
instance priorities helps.
@grunweg grunweg added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Mar 19, 2026
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Mar 19, 2026

!bench

@leanprover-radar
Copy link
Copy Markdown

Waiting until the label awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. is removed.

You can edit the original message until the command succeeds.

@github-actions
Copy link
Copy Markdown

PR summary 09af23f880

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

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/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-analysis Analysis (normed *, calculus) label Mar 19, 2026
@grunweg
Copy link
Copy Markdown
Contributor Author

grunweg commented Apr 10, 2026

Closing; I don't capacity right now to investigate this. The underlying slow-down for metric connections has been fixed.

@grunweg grunweg closed this Apr 10, 2026
@grunweg grunweg deleted the normed-add-prio branch April 10, 2026 16:12
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-analysis Analysis (normed *, calculus)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants