Skip to content

perf: mark inhabited arguments to extern as borrowed#13094

Merged
hargoniX merged 2 commits intomasterfrom
hbv/borrow_inhabited
Mar 24, 2026
Merged

perf: mark inhabited arguments to extern as borrowed#13094
hargoniX merged 2 commits intomasterfrom
hbv/borrow_inhabited

Conversation

@hargoniX
Copy link
Copy Markdown
Contributor

This PR marks the Inhabited arguments of all functions in core marked as extern as borrowed
(panicking array accessors and panic! itself). This in turn causes a transitive effect throughout
the codebase and promotes most, if not all, Inhabited arguments to functions to borrowed.

@hargoniX hargoniX added the changelog-compiler Compiler, runtime, and FFI label Mar 24, 2026
@hargoniX
Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 24, 2026

Benchmark results for 3f4bbe5 against 5054448 are in. Significant changes detected! @hargoniX

  • build//instructions: -16.8G (-0.14%)

Large changes (1✅)

  • compiled/qsort//instructions: -63.8M (-0.34%)

Medium changes (1✅)

  • compiled/parser//instructions: -49.2M (-0.13%)

Small changes (8✅, 1🟥)

  • build/module/Init.Data.Nat.ToString//instructions: -76.4M (-0.24%)
  • build/module/Lean.Elab.Do.Legacy//instructions: -100.2M (-0.18%)
  • build/module/Lean.Elab.DocString//instructions: -81.7M (-0.17%)
  • build/module/Lean.Meta.Tactic.Grind.Types//instructions: -86.6M (-0.21%)
  • build/module/Std.Data.DHashMap.RawLemmas//instructions: -268.5M (-0.18%)
  • build/module/Std.Data.DTreeMap.Raw.Lemmas//instructions: -113.7M (-0.14%)
  • 🟥 compiled/rbmap_checkpoint//instructions: +3.8M (+0.03%)
  • elab/big_do//instructions: -36.0M (-0.15%)
  • elab/bv_decide_realworld//wall-clock: -47ms (-3.92%)

@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 Mar 24, 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 50544489a9634d6842c64deeb284e62fe6ae523c --onto e6df474dd9c3ad0e21771eaa808c53f66222216d. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-24 11:30:31)

@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 50544489a9634d6842c64deeb284e62fe6ae523c --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-24 11:30:32)

@hargoniX hargoniX enabled auto-merge March 24, 2026 12:19
@hargoniX hargoniX added this pull request to the merge queue Mar 24, 2026
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks Mar 24, 2026
@hargoniX hargoniX force-pushed the hbv/borrow_inhabited branch from 73515fd to 97d58ca Compare March 24, 2026 13:27
@hargoniX hargoniX enabled auto-merge March 24, 2026 13:27
@hargoniX hargoniX added this pull request to the merge queue Mar 24, 2026
Merged via the queue into master with commit d0aa7d2 Mar 24, 2026
17 checks passed
@hargoniX hargoniX deleted the hbv/borrow_inhabited branch March 24, 2026 20:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-compiler Compiler, runtime, and FFI 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