Skip to content

fix: interaction of extern annotations and calls to functions with borrowed parameters#13052

Merged
hargoniX merged 1 commit intomasterfrom
hbv/borrow_inference_export
Mar 23, 2026
Merged

fix: interaction of extern annotations and calls to functions with borrowed parameters#13052
hargoniX merged 1 commit intomasterfrom
hbv/borrow_inference_export

Conversation

@hargoniX
Copy link
Copy Markdown
Contributor

This PR fixes a bug in the borrow inference in connection with export annotations.

Previously parameters of export functions were presumed as owned from the beginning of the
analysis. However, they were not added into the set of owned parameters and thus sometimes failed to
force necessary changes to borrowedness of other values that the parameters flowed into.

@hargoniX hargoniX requested a review from leodemoura as a code owner March 23, 2026 08:48
@hargoniX hargoniX added release-ci Enable all CI checks for a PR, like is done for releases changelog-compiler Compiler, runtime, and FFI fast-ci Forces the use of large runners so that e.g. PR releases are created faster labels Mar 23, 2026
@hargoniX
Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented Mar 23, 2026

Benchmark results for b3e83d2 against 189cea9 are in. There are no significant changes. @hargoniX

  • 🟥 build//instructions: +1.0G (+0.01%)

Medium changes (1✅)

  • interpreted/identifier_completion//instructions: -1.1G (-1.42%)

Small changes (1✅, 2🟥)

  • 🟥 build/module/Lean.Compiler.LCNF.InferBorrow//instructions: +270.1M (+4.14%) (reduced significance based on *//lines)
  • 🟥 compiled/rbmap_checkpoint//instructions: +3.0M (+0.02%)
  • interpreted/identifier_completion//wall-clock: -105ms (-2.49%)

@hargoniX hargoniX force-pushed the hbv/borrow_inference_export branch from b3e83d2 to 5a96d04 Compare March 23, 2026 09:12
@hargoniX hargoniX removed release-ci Enable all CI checks for a PR, like is done for releases fast-ci Forces the use of large runners so that e.g. PR releases are created faster labels Mar 23, 2026
@hargoniX hargoniX force-pushed the hbv/borrow_inference_export branch from 5a96d04 to 4a007bb Compare March 23, 2026 09:51
@hargoniX hargoniX enabled auto-merge March 23, 2026 09:51
@hargoniX hargoniX added this pull request to the merge queue Mar 23, 2026
Merged via the queue into master with commit 08595c5 Mar 23, 2026
18 of 22 checks passed
@hargoniX hargoniX deleted the hbv/borrow_inference_export branch March 23, 2026 12:12
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

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants