Lean install problems

Stream: general

[Aron]

Hovering over import statements in the tutorial files says that the imports can't resolve.

$ lean --path
{
  "is_user_leanpkg_path": true,
  "leanpkg_path_file": "/Users/atobi16/.lean/leanpkg.path",
  "path": [
    "/Users/atobi16/.elan/toolchains/stable/bin/../library",
    "/Users/atobi16/.elan/toolchains/stable/bin/../lib/lean/library"
  ]
}

Isn't this where lean is supposed to be looking?

[Johan Commelin]

How did you get the tutorials?

[Johan Commelin]

Are you missing the mathlib dependency, by chance?

[Johan Commelin]

Did you git clone the repo, or did you use leanproject?

[Aron]

I used leanproject.

[Aron]

I used the regular Lean OSX install.

[Bryan Gin-ge Chen]

Which directory are you running lean --path in? If I navigate to my tutorials folder and run lean --path, I see:

{
  "is_user_leanpkg_path": false,
  "leanpkg_path_file": "/Users/chb/Documents/lean/tutorials/leanpkg.path",
  "path": [
    "/Users/chb/.elan/toolchains/leanprover-community-lean-3.20.0/bin/../library",
    "/Users/chb/.elan/toolchains/leanprover-community-lean-3.20.0/bin/../lib/lean/library",
    "/Users/chb/Documents/lean/tutorials/_target/deps/mathlib/src",
    "/Users/chb/Documents/lean/tutorials/./src/solutions"
  ]
}

[Bryan Gin-ge Chen]

Also, you did open the entire tutorials/ directory in VS Code, right? If you only open a single file in VS Code, the extension won't be able to find the imports.

[Aron]

I did open the whole directory, and I ran --path in the parent directory.
In the tutorials folder it yields:

{
  "is_user_leanpkg_path": false,
  "leanpkg_path_file": "/Users/atobi16/programs/lean/tutorials/leanpkg.path",
  "path": [
    "/Users/atobi16/.elan/toolchains/leanprover-community-lean-3.20.0/bin/../library",
    "/Users/atobi16/.elan/toolchains/leanprover-community-lean-3.20.0/bin/../lib/lean/library",
    "/Users/atobi16/programs/lean/tutorials/_target/deps/mathlib/src",
    "/Users/atobi16/programs/lean/tutorials/./src/solutions"
  ]
}

[Bryan Gin-ge Chen]

And you opened the tutorials/ directory in VS Code? If you open the parent directory of tutorials/, it won't work either. Maybe also try running leanproject get-mathlib-cache again inside the tutorials/ directory, although this shouldn't be necessary if you originally ran leanproject get tutorials.

[Aron]

Hey, it works. Thanks.

[Bryan Gin-ge Chen]

No problem - let us know if you have any suggestions for the install instructions!