ssh vscode

Stream: general

[Billy Price]

Annoying tech question - I'll try make this painless. I'm trying to run lean/vscode on my server over ssh. Vscode has native remote ssh connection which I've used successfully for standard usage, but I'm failing to use it in conjunction with lean. After I trigger a restart of the lean server it just hangs for about 30 seconds on checking visible files and then vscode loses the ssh connection and reconnects over and over, OR, it stops checking and gives me

invalid import: data.option.defs
excessive memory consumption detected at 'type checker' (potential solution: increase memory consumption threshold)Lean

Since I've just installed lean via the extension on the server, I'd like to confirm that my lean installation is working before trying to marry it to the vs code remote session. Is there a way I can verify lean is working on my project just in the terminal?

[Johan Commelin]

@Mario Carneiro got this working on my server

[Johan Commelin]

You can cd to/your/lean/project and run leanpkg build to test lean

[Billy Price]

wow that's slow. Can I get it to skip the mathlib compiling part?

[Riccardo Brasca]

leanproject get-mathlib-cache should work

[Billy Price]

hmm I just realised I don't have leanproject, that's probably why

[Billy Price]

(on the server)

[Riccardo Brasca]

If I remember correctly I had to tel VS Code to use the Lean extension on the server

[Riccardo Brasca]

Yes, the server has a normal mathlib installation, with leanproject and all the other stuff

[Riccardo Brasca]

The only thing that doesn't work for me is Bracket Pair Colorizer