Skip to content

fix: keep findOLean's root cache valid across withImportModules - #16320

Merged
Kha merged 1 commit into
masterfrom
fix-olean-root-cache-freed-name
Nov 6, 2026
Merged

Kha merged 1 commit into
masterfrom
fix-olean-root-cache-freed-name

Conversation

@Kha

@Kha Kha commented Nov 6, 2026

Copy link
Copy Markdown
Member

This PR fixes a segfault when withImportModules is called a second time in one process and the imported module imports another package root, a regression from #15291.

findOLean cached package roots keyed by Names that may live in an imported .olean region, which withImportModules frees after use. The cache now stores Runtime.deepCopys of these names.

Fixes #16267

This PR fixes a segfault when `withImportModules` is called a second time in one process and the imported module imports another package root, a regression from #15291.

`findOLean` cached package roots keyed by `Name`s that may live in an imported `.olean` region, which `withImportModules` frees after use. The cache now stores `Runtime.deepCopy`s of these names.

Fixes #16267

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@Kha Kha added the changelog-language Language features and metaprograms label Nov 6, 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 Nov 6, 2026
@Kha
Kha marked this pull request as ready for review November 6, 2026 18:18
@Kha
Kha added this pull request to the merge queue Nov 6, 2026
Merged via the queue into master with commit a2f1a64 Nov 6, 2026
25 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-language Language features and metaprograms 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.

Segfault on the second withImportModules in one process: findOLean's root cache keeps a Name from a freed .olean region (regression in 4.36.0-rc1)

1 participant