Unable to import

Stream: new members

[Pedro Castilho]

Am trying to import data.set but its not working, I tried following the guides of https://leanprover-community.github.io/file-not-found.html but couldn't make work either.

it seem like my path is ok:

pedro@MacBook-Pro-de-Pedro ~ % lean --path
{
  "is_user_leanpkg_path": true,
  "leanpkg_path_file": "/Users/pedro/.lean/leanpkg.path",
  "path": [
    "/Users/pedro/.elan/toolchains/stable/bin/../library",
    "/Users/pedro/.elan/toolchains/stable/bin/../lib/lean/library"
  ]
}

anyone knows what should I do?

[Bryan Gin-ge Chen]

If you're trying to import mathlib's data.set then that path doesn't look OK, since it doesn't include any copy of mathlib.

You're working inside a Lean project that you created with leanproject new, right?

[Bryan Gin-ge Chen]

If you ran leanproject new your_project_name, then you need to open the your_project_name directory in VS Code, not just some file in it.

[Pedro Castilho]

Am not creating a new project, I imported a list o problems from GitHub and opened them with vs code

[Bryan Gin-ge Chen]

OK, I recommend you create a new project with leanproject new and put your file in that project. See our page on Lean projects.

[Pedro Castilho]

Ok, thanks @Bryan Gin-ge Chen am going to try that

[Pedro Castilho]

@Bryan Gin-ge Chen everything went well, ended up downloading the same thing twice but its running hahaha, thx for the help!