Skip to content

Finalize Lean declaration sessions - #808

Merged
morluto merged 2 commits into
mainfrom
agent/finalize-lean-declaration-sessions
Aug 8, 2026
Merged

Finalize Lean declaration sessions#808
morluto merged 2 commits into
mainfrom
agent/finalize-lean-declaration-sessions

Conversation

@morluto

@morluto morluto commented Aug 7, 2026

Copy link
Copy Markdown
Owner

Fixes #759.

The declaration backend retains temporary-directory-backed query sessions until explicit close. Add a backend-owned weakref finalizer that closes cached sessions when the backend is collected, then detach it after explicit cleanup.

This addresses temporary-directory leakage; declaration queries use bounded one-shot processes and do not retain a live Lean subprocess.

Validation:

  • make test-component TESTS=tests/component/providers/lean/test_lean_declaration_sessions.py — 9 passed
  • make lint-full — passed

@morluto
morluto marked this pull request as ready for review August 8, 2026 04:29
@cursor

cursor Bot commented Aug 8, 2026

Copy link
Copy Markdown

Bugbot is not enabled for your account, so this pull request was not reviewed.

Enable Bugbot in the Cursor dashboard to get automatic reviews on future PRs.

@morluto
morluto merged commit 341bf4c into main Aug 8, 2026
39 checks passed
@morluto
morluto deleted the agent/finalize-lean-declaration-sessions branch August 8, 2026 04:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

[Bug]: LeanSubprocessDeclarationBackend lacks weakref finalizer, leaking subprocess sessions and temp directories

1 participant