Skip to content

perf: assorted compiler annotations#13357

Merged
hargoniX merged 1 commit intomasterfrom
hbv/systematic_annotations
Apr 10, 2026
Merged

perf: assorted compiler annotations#13357
hargoniX merged 1 commit intomasterfrom
hbv/systematic_annotations

Conversation

@hargoniX
Copy link
Copy Markdown
Contributor

@hargoniX hargoniX commented Apr 10, 2026

This PR is based on a systematic review of all read-only operations on the default containers in core. Where sensible it applies specialize annotations on higher order operations that lack them or borrow annotations on parameters that should morally be borrowed (e.g. the container when iterating over it).

@hargoniX
Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Apr 10, 2026

Benchmark results for c1c6492 against e0a29f4 are in. Significant changes detected! @hargoniX

  • build//instructions: -108.3G (-0.90%)

Large changes (1✅)

  • misc/leanchecker --fresh Init//instructions: -8.7G (-2.31%)

Medium changes (29✅)

Too many entries to display here. View the full report on radar instead.

Small changes (1002✅, 3🟥)

Too many entries to display here. View the full report on radar instead.

@hargoniX hargoniX changed the title perf: assorted borrowing annotations perf: assorted compiler annotations Apr 10, 2026
@hargoniX hargoniX added the changelog-library Library label Apr 10, 2026
@hargoniX hargoniX marked this pull request as ready for review April 10, 2026 11:42
@hargoniX hargoniX requested a review from kim-em as a code owner April 10, 2026 11:42
@hargoniX hargoniX added this pull request to the merge queue Apr 10, 2026
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Apr 10, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-04-10 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-10 12:00:44)

@leanprover-bot
Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-04-10 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-04-10 12:00:45)

Merged via the queue into master with commit bc2da2d Apr 10, 2026
32 checks passed
@hargoniX hargoniX deleted the hbv/systematic_annotations branch April 10, 2026 12:21
volodeyka pushed a commit that referenced this pull request Apr 16, 2026
This PR is based on a systematic review of all read-only operations on
the default containers in core. Where sensible it applies specialize
annotations on higher order operations that lack them or borrow
annotations on parameters that should morally be borrowed (e.g. the
container when iterating over it).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants