Zulip Chat Archive

Stream: general

Topic: Unable to build vscode.lean


Daniel Donnelly (Aug 30 2019 at 16:58):

Hi. I've cloned the repository on git. I had it cloned and running before, except I need to start over fresh to get through some other bugs.

So starting fresh, I hit F5 to debug, and get the following:

pasted image

Bryan Gin-ge Chen (Aug 30 2019 at 17:14):

Did you rerun npm install?

Daniel Donnelly (Aug 30 2019 at 17:17):

Yep, thank you! That was the problem. :)

Daniel Donnelly (Aug 30 2019 at 20:58):

Got pretty far so far. It's official, VSCode is opening Bancats alongside Lean:
pasted image

Jesse Michael Han (Aug 31 2019 at 01:25):

(deleted)


Last updated: Dec 20 2023 at 11:08 UTC