Zulip Chat Archive

Stream: general

Topic: fix LEAN_PATH


view this post on Zulip garySebastian (Mar 31 2018 at 22:58):

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.

view this post on Zulip Simon Hudon (Mar 31 2018 at 23:04):

Do you use leanpkg?

view this post on Zulip garySebastian (Mar 31 2018 at 23:12):

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

view this post on Zulip Simon Hudon (Mar 31 2018 at 23:16):

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

view this post on Zulip garySebastian (Mar 31 2018 at 23:50):

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.

view this post on Zulip Simon Hudon (Apr 01 2018 at 00:00):

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

view this post on Zulip Patrick Massot (Apr 01 2018 at 08:46):

@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

view this post on Zulip Kenny Lau (Apr 01 2018 at 08:46):

I concur

view this post on Zulip Patrick Massot (Apr 01 2018 at 08:47):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:06):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:06):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:06):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:06):

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]

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:07):

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

view this post on Zulip Gabriel Ebner (Apr 01 2018 at 16:07):

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.

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:09):

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

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:09):

(I am talking about using leanpkg)

view this post on Zulip Kevin Buzzard (Apr 01 2018 at 16:10):

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


Last updated: May 08 2021 at 03:17 UTC