Zulip Chat Archive

Stream: new members

Topic: Unable to import

Pedro Castilho (Oct 31 2020 at 22:15):

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": [

anyone knows what should I do?

Bryan Gin-ge Chen (Oct 31 2020 at 22:20):

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 (Oct 31 2020 at 22:21):

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 (Oct 31 2020 at 22:26):

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

Bryan Gin-ge Chen (Oct 31 2020 at 22:27):

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 (Oct 31 2020 at 22:28):

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

Pedro Castilho (Nov 01 2020 at 01:49):

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

Last updated: Dec 20 2023 at 11:08 UTC