Skip to content

fix: potential Array.get!Internal leaks part 2#13148

Merged
hargoniX merged 1 commit intomasterfrom
hbv/fix_getbang_p2
Mar 27, 2026
Merged

fix: potential Array.get!Internal leaks part 2#13148
hargoniX merged 1 commit intomasterfrom
hbv/fix_getbang_p2

Conversation

@hargoniX
Copy link
Copy Markdown
Contributor

@hargoniX hargoniX commented Mar 27, 2026

Part 2 for #13147, adding the necessary constant semantics to the interpreter.

fix interpreter

add test

foo
@hargoniX hargoniX added changelog-no Do not include this PR in the release changelog 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 27, 2026
@hargoniX hargoniX enabled auto-merge March 27, 2026 01:19
@hargoniX hargoniX added this pull request to the merge queue Mar 27, 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 Mar 27, 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 bc5210d52a97c485ace1e4abc95ed7da6ba5b707 --onto 4786e082dca22873d14d2a5b9b7c8843380c6e78. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-27 03:04:25)

@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 bc5210d52a97c485ace1e4abc95ed7da6ba5b707 --onto cfa8c5a036d6990635c6ec50b02d0e806995cec3. You can force reference manual CI using the force-manual-ci label. (2026-03-27 03:04:26)

Merged via the queue into master with commit fee2d7a Mar 27, 2026
44 of 52 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-no Do not include this PR in the release changelog fast-ci Forces the use of large runners so that e.g. PR releases are created faster release-ci Enable all CI checks for a PR, like is done for releases 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.

2 participants