[GoLUG] PSA for VSCode: SSH plugin lets the remote end run arbitrary local commands

Barry Fishman barry at ecubist.org
Mon Sep 28 09:52:55 EDT 2026


On 2026-09-27 17:38:51 -04, Hendrik Boom wrote:
> For a while now I've been wanting to try out LEAN, the tool that
> makes it feasible to write and check forma mathematical proofs.
>
> The LEAN documetation tells me to start by installing VScode.
>
> This note deters me from doing any of this, locking me out of
> current mathematical research.

Isn't there a lean setup for emacs:

https://github.com/cmknapp/lean/blob/master/src/emacs/README.md

And for nvim:

https://github.com/Julian/lean.nvim

Although I have not tried Lean myself.
-- 
Barry Fishman


More information about the GoLUG mailing list