Zulip Chat Archive

Stream: general

Topic: fix LEAN_PATH

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.

Simon Hudon (Mar 31 2018 at 23:04):

Do you use leanpkg?

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.

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

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.

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?

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

Kenny Lau (Apr 01 2018 at 08:46):

I concur

Patrick Massot (Apr 01 2018 at 08:47):

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

Kevin Buzzard (Apr 01 2018 at 16:06):

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

Kevin Buzzard (Apr 01 2018 at 16:06):

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

Kevin Buzzard (Apr 01 2018 at 16:06):

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

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]

Kevin Buzzard (Apr 01 2018 at 16:07):

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

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.

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

Kevin Buzzard (Apr 01 2018 at 16:09):

(I am talking about using leanpkg)

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: Dec 20 2023 at 11:08 UTC