Memory handling in WithRpcRef

Stream: metaprogramming / tactics

[Mirek Olšák]

Does someone know how exactly / well WithRpcRef is capable of avoiding memory leakage? WithRpcRef allows Lean sending a reference to a Lean object to Javascript so that Javascript code can then pass such a reference back to Lean functions tagged with @[server_rpc_method]. Now, these functions could return such references again, so there could be a sophisticated Javascript code operating on Lean data.
However, I am worried if Lean would be able to notice that Javascript has dropped such a reference, so it is safe to release it from memory on Lean side too.
Is my worry correct that such RPC references should not be overused, or can I just assume that memory will be handled automatically for me (as it often is in high level programming languages)?

[Sebastian Ullrich]

Yes, garbage collection of RPC references is automated, see https://github.com/leanprover/vscode-lean4/blob/c2b1918778b84162536d4a6533a9a8e6735c0c88/lean4-infoview-api/src/rpcSessions.ts#L72-L91

[Mirek Olšák]

Cool, thanks!