Zulip Chat Archive

Stream: lean4

Topic: How to setup lean4 viscose extension

view this post on Zulip Lim, Thing-han (Feb 24 2021 at 08:26):

I followed the instructions of the lean4 viscose extensions, run npm install then open VS Code on the folder, then Press Ctrl + Shift + B to compile.
However it then reports Error: Can't resolve './src/extension.ts'.
Do I misunderstand something? how can I setup the vscode extension?

view this post on Zulip Sebastian Ullrich (Feb 24 2021 at 08:57):

You should get the extension from the marketplace if you're not interested in extending it

view this post on Zulip Marc Huisinga (Feb 24 2021 at 09:34):

Or open the extensions menu on the left in VSCode and type in lean4, then install the extension.

Last updated: May 07 2021 at 11:09 UTC