Zulip Chat Archive

Stream: new members

Topic: no _target

Coda (Jul 06 2022 at 19:53):

When I click open fold and upload the existing project, there was no folder "_target", whereas I saw others had. Probably because of this reason, when any import led to errors. What should I do?

Coda (Jul 06 2022 at 19:53):

image.png

Kevin Buzzard (Jul 06 2022 at 20:06):

You need to correctly install a project onto your machine with leanproject and then open the root directory of the project with VS Code.

SwollenBerks (Jul 07 2022 at 02:24):

opened the HelloWorld sample in the lean4-samples repo and this is the error I get image.png

SwollenBerks (Jul 07 2022 at 02:30):

this is the file it seems to be complaining about image.png

Kevin Buzzard (Jul 07 2022 at 06:35):

Your first question was about a Lean 3 repo (which I'm competent to answer) and your second is about a Lean 4 one (which I'm not).

SwollenBerks (Jul 07 2022 at 22:14):

sorry, I meant to make a new topic

Last updated: Dec 20 2023 at 11:08 UTC