Running LSP from VSCode under rr

Stream: lean4

[namibj]

I'm trying to debug what from a coredumpctl debug point of view appears to be a double-free in a C/C++ FFI library, which I recompiled with debug settings before reproducing the crash to get to the mentioned preliminary conclusion.

What I don't see a straight-forward way for is how to wrap the LSP process execution in an rr record, so I can inspect the problem without causing pain from VSCode and it's GPU acceleration.
Does anyone have a guide/instructions for how to do this (run Lean4 LSP under rr record to then reproduce issue via the same UI interactions in VSCode, so that the rr recording can be properly debugged)?

Previous situations like this always had a convenient override for the LSP binary/command line whre I could have put a script or even directly prefixed the command with rr record; but the Lean4 Extension doesn't seem to have that config option.

(This is for Lean Copilot, if anyone's wondering; I'm trying to get RAG working and encountered a reproducible ("on my system", at least) segfault that I don't want to debug without rr.)

[Marc Huisinga]

I haven't tested any of these, but you could make lean point to your rr record invocation by changing the toolchain with Elan (override) or using the toolchain file. Alternatively there are also the "Lean4: Server Env Paths", "Lean4: Toolchain Path" and "Lean4: Lake Path" settings that can be adjusted in the VS Code extension.

[namibj]

Marc Huisinga said:

I haven't tested any of these, but you could make lean point to your rr record invocation by changing the toolchain with Elan (override) or using the toolchain file. Alternatively there are also the "Lean4: Server Env Paths", "Lean4: Toolchain Path" and "Lean4: Lake Path" settings that can be adjusted in the VS Code extension.

I saw the toolchain and lake path opportunities; but the interceptor script they'd seem to require feels quite ugly.
I guess the server env paths option might allow an LD_PRELOAD approach. I don't remember that being accessible for rr; but there's probably a generic .so that listens to a magic env var that's a s/foo/bar/-style regex replacement to detect a certain execve and re-write it before actually letting the execve go through to the kernel.

I just hoped this would be somewhat well-trodden as rr has been mentioned several times as the weapon of choice when low-level/memory management things go wrong in Lean4, and "the LSP" is a major part of Lean4 from the user's POV.

[Marc Huisinga]

I think it's rare that we actually debug Lean from within the LSP process. In most cases, a regular terminal lean invocation is what's being debugged.

For LSP, the invocation flow is roughly as follows: The VS Code extension invokes lake --serve, which in turn invokes lean --server.

[namibj]

Marc Huisinga said:

I think it's rare that we actually debug Lean from within the LSP process. In most cases, a regular terminal lean invocation is what's being debugged.

"Debugging from within the LSP process"... technically you're not quite wrong, but I wouldn't really call "get an rr recording for offline inspection" _debugging_ in a sense that can be within a process.

For LSP, the invocation flow is roughly as follows: The VS Code extension invokes lake --serve, which in turn invokes lean --server.

I saw as much in htop. I guess I'll try to intercept/shim the lake --serve.

[Marc Huisinga]

It's perhaps also worth pointing out that the language server launches further processes for every single file using lean --worker.