fix LEAN_PATH

Stream: general

[garySebastian]

I've tried to get lean to work on Xubuntu, macOS, and nixos; all three are having the same issue where importing anything (including standard), yields an error: "file standard not found in the LEAN_PATH". I've done a lot of looking around and can't find any relevant information on LEAN_PATH. I have lean in my system PATH. I'm not sure what it wants from me.

[Simon Hudon]

Do you use leanpkg?

[garySebastian]

I've tried creating a new project and doing configure/messing with the leankpkg.path, but it doesn't seem to do anything.

[Simon Hudon]

Setting LEAN_PATH by hand leads to nothing but trouble so I suggest you unset it (if you set it yourself), create a Lean project with leanpkg initand using leanpkg add for your dependencies

[garySebastian]

Thank you for the advice so far, but I'm still getting the same error after trying both leanpkg add https://github.com/leanprover/mathlib and https://github.com/leanprover/stdlib.git. They're both in the _build directory within the project, and they were both added to the leanpkg.path file and leanpkg.toml files.

[Simon Hudon]

can you show me your leanpkg.toml file and tell me where you put your source file?

[Patrick Massot]

@Sebastian Ullrich and @Gabriel Ebner This is one more motivating example for you. We really need to make it simpler for people to start using Lean

[Kenny Lau]

I concur

[Patrick Massot]

I mean: I know you are working hard, I only want to point out further encouragement.

[Kevin Buzzard]

Doesn't this all depend on how you are running Lean?

[Kevin Buzzard]

For example, I _think_ that if you use VS Code and open a folder

[Kevin Buzzard]

and there's e.g. some leanpkg.path file in the root of that folder

[Kevin Buzzard]

then I think VS Code will look at that file before it looks at the LEAN_PATH environment variable [NB but apparently I am wrong]

[Kevin Buzzard]

What is this _build directory you're talking about @garySebastian ?

[Gabriel Ebner]

Neither vscode nor emacs touches the LEAN_PATH environment variable. If it is set, it takes precedence over any leanpkg.path file. Please don't set the LEAN_PATH environment variable.

[Kevin Buzzard]

If you just follow the step by step instructions for making a new project and adding mathlib, I think it will add mathlib into a directory called _target

[Kevin Buzzard]

(I am talking about using leanpkg)

[Kevin Buzzard]

and everything should magically work because leanpkg will get your leanpkg.path right and you won't need to set LEAN_PATH at all by the looks of things