Comment by fooker

This has also been my experience with lean4.

I don't understand the forced vscode path, just let me get it as normal software in a convenient way and run it as a tool