Skip to content

feat: respect user provided borrow annotations#12830

Draft
hargoniX wants to merge 2 commits intomasterfrom
hbv/lcnf_preserve_infer_annotations
Draft

feat: respect user provided borrow annotations#12830
hargoniX wants to merge 2 commits intomasterfrom
hbv/lcnf_preserve_infer_annotations

Conversation

@hargoniX
Copy link
Contributor

@hargoniX hargoniX commented Mar 6, 2026

  • preserve in early pipeline
  • first attempt

@hargoniX
Copy link
Contributor Author

hargoniX commented Mar 6, 2026

!bench

@leanprover-radar
Copy link

leanprover-radar commented Mar 6, 2026

Benchmark results for d72df3e against 68ea28c are in! @hargoniX

  • 🟥 build//instructions: +2.1G (+0.02%)

Small changes (2🟥)

  • 🟥 build/module/Lean.Compiler.LCNF.InferBorrow//instructions: +395.0M (+6.04%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Compiler.LCNF.ToLCNF//instructions: +395.3M (+2.09%) (reduced significance based on *//lines)

@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 6, 2026
@mathlib-lean-pr-testing
Copy link

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 68ea28c24f9ce74272a8f6aa88ad5bbc70f4034f --onto 333ab1c6f0ce11f33551d6a736054cb72812cad9. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-06 17:27:51)

@leanprover-bot
Copy link
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 68ea28c24f9ce74272a8f6aa88ad5bbc70f4034f --onto cda84702e9b31165f1f83c657b532f36f34e0bd0. You can force reference manual CI using the force-manual-ci label. (2026-03-06 17:27:53)

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