Skip to content

perf: empty array - #15016

Draft
TwoFX wants to merge 1 commit into
leanprover:masterfrom
TwoFX:julia/empty-array
Draft

perf: empty array#15016
TwoFX wants to merge 1 commit into
leanprover:masterfrom
TwoFX:julia/empty-array

Conversation

@TwoFX

@TwoFX TwoFX commented Sep 4, 2026

Copy link
Copy Markdown
Member

No description provided.

@TwoFX

TwoFX commented Sep 4, 2026

Copy link
Copy Markdown
Member Author

!radar

@leanprover-radar

leanprover-radar commented Sep 4, 2026

Copy link
Copy Markdown

Benchmark results for 1c51097 against 67526ae are in. No significant results found. @TwoFX

  • build//instructions: -3.7G (-0.03%)

Medium changes (1✅)

  • compiled/parser//instructions: -105.6M (-0.30%)

@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 Sep 4, 2026
@mathlib-lean-pr-testing

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 67526ae54d733251644d5cebb9fa5a77318fecc4 --onto c632a0a0e434a951cdcf61bb4da3344abadd5587. You can force Mathlib CI using the force-mathlib-ci label. (2026-09-04 11:09:28)

@leanprover-bot

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 67526ae54d733251644d5cebb9fa5a77318fecc4 --onto 58774429865502f05c63239266aac30ef1e91ef7. You can force reference manual CI using the force-manual-ci label. (2026-09-04 11:09:30)

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

Labels

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