Zulip Chat Archive

Stream: new members

Topic: Just installed Lean

Sailor Haddad (Mar 01 2022 at 19:02):

Hi ! I just installed Lean following the instructions, and then installed the tutorial project following these instructions but why vs code is throwing me errors ? image.png image.png

Sailor Haddad (Mar 01 2022 at 19:03):

image.png

Martin Dvořák (Mar 01 2022 at 19:05):

Can you please show the content of the folder target in the main directory of your project?

Sailor Haddad (Mar 01 2022 at 19:06):

image.png

Martin Dvořák (Mar 01 2022 at 19:07):

Does deps contain mathlib inside?

Sailor Haddad (Mar 01 2022 at 19:07):

yes

Martin Dvořák (Mar 01 2022 at 19:07):

What happens when you run leanproject build on the command line?

Sailor Haddad (Mar 01 2022 at 19:08):

how can i do that

Martin Dvořák (Mar 01 2022 at 19:09):

Try to write it in the same command line that you used for leanproject get tutorials before.

Sailor Haddad (Mar 01 2022 at 19:10):

could not find a leanpkg.toml

Last updated: Dec 20 2023 at 11:08 UTC