Zulip Chat Archive

Stream: new members

Topic: File not found in LEAN_PATH


view this post on Zulip Maxim Gerspach (May 11 2019 at 14:08):

Hi,

I just installed Lean on Windows 10 (and it seems to be working fine) using elan, and I followed the instructions on how to start a new package with mathlib. However, imports do not seem to be working for me, it tells me that the file could not be found in the LEAN_PATH. I'm not exactly sure what the reason for this is. leanpkg.path is in the root directory of the project.

view this post on Zulip Johan Commelin (May 11 2019 at 14:12):

How did you install? Using the Lean extension for VScode? Or did you manually install elan?

view this post on Zulip Maxim Gerspach (May 11 2019 at 14:17):

I used the Lean extension for VScode.

view this post on Zulip Bryan Gin-ge Chen (May 11 2019 at 14:21):

What does leanpkg.path contain and what are you trying to import

view this post on Zulip Bryan Gin-ge Chen (May 11 2019 at 14:23):

Are you doing something more like Scenario 1 or 2 here ?

view this post on Zulip Maxim Gerspach (May 11 2019 at 14:28):

I followed scenario 1.
leanpkg.path says

builtin_path
path _target/deps/mathlib/src
path ./src

view this post on Zulip Maxim Gerspach (May 11 2019 at 14:32):

It doesn't really seem to depend on what I try to import, e.g. import theory.set_theory gives me this error, but also all kinds of other imports.

view this post on Zulip Reid Barton (May 11 2019 at 14:34):

There's no such thing as theory.set_theory; where are you getting that?

view this post on Zulip Reid Barton (May 11 2019 at 14:40):

Try for example import algebra.ring

view this post on Zulip Maxim Gerspach (May 11 2019 at 14:42):

Maybe I got confused about something. But import algebra.ring does not work either, with the same error.

view this post on Zulip Bryan Gin-ge Chen (May 11 2019 at 14:50):

I'm assuming you've looked in _target/deps/mathlib/src and everything was there? And the files you're editing are in the src subdirectory of your package?

view this post on Zulip Maxim Gerspach (May 11 2019 at 15:39):

Indeed I have, and both my file is in the src subdirectory of the package and ring.lean is in _target/deps/mathlib/src/algebra.

view this post on Zulip Kevin Buzzard (May 11 2019 at 15:59):

Did you "open folder" in VS Code?

view this post on Zulip Kevin Buzzard (May 11 2019 at 15:59):

VS Code might not be looking at your leanpkg.path if you don't open the project like this.

view this post on Zulip Simon Hudon (May 11 2019 at 16:14):

Did you set the LEAN_PATH environment variable. I used to set it and get the same problem

view this post on Zulip Maxim Gerspach (May 11 2019 at 16:17):

Oh, I think I pressed "open folder" on the folder above; now it is working properly. Thanks for the help!

view this post on Zulip Maxim Gerspach (May 11 2019 at 16:18):

And thanks for the talk at Warwick yesterday, Kevin!

view this post on Zulip Kevin Buzzard (May 11 2019 at 16:18):

Hah! Thanks for coming!

view this post on Zulip Kevin Buzzard (May 11 2019 at 16:18):

I'm sorry it's so difficult to get started without someone who knows what's going on in the same room as you. I don't know what to do about this really.

view this post on Zulip Moses Schönfinkel (May 11 2019 at 16:19):

Distribute a Linux distro image with preinstalled Lean, of course :).

view this post on Zulip Patrick Massot (May 11 2019 at 16:20):

Moses, we already have https://github.com/leanprover-community/mathlib/blob/master/docs/install_debian.md The real issue is people using Windows

view this post on Zulip Moses Schönfinkel (May 11 2019 at 16:20):

Ah, I had no idea! Well done.

view this post on Zulip Patrick Massot (May 11 2019 at 16:21):

I'm working on finding a Windows image I could use in VirtualBox to create something easy for windows users

view this post on Zulip Kevin Buzzard (May 11 2019 at 16:21):

Even with preinstalled Lean it's not going to stop people from opening projects in the wrong way. This is not an uncommon problem.

view this post on Zulip Patrick Massot (May 11 2019 at 16:21):

Yes, it's amazing how people have a hard time understanding that part of the instructions

view this post on Zulip Moses Schönfinkel (May 11 2019 at 16:22):

Windows images run into licensing / legal issues I would guess.

view this post on Zulip Patrick Massot (May 11 2019 at 16:23):

I'm trying to figure out how I can get a license paid by my university in order to have a windows in a virtual machine in my office. Then at least we'll be able to work on install instructions

view this post on Zulip Andrew Ashworth (May 11 2019 at 18:50):

Microsoft releases Dev images every so often, no license required. https://developer.microsoft.com/en-us/windows/downloads/virtual-machines

view this post on Zulip Andrew Ashworth (May 11 2019 at 18:52):

What's inconvenient isn't licensing but the fact that they only offer a complete image that's many GB big.

view this post on Zulip Mario Carneiro (May 12 2019 at 06:51):

Maybe put some bold text in this section of the instructions: If there is a blue button "open folder" on the left you haven't done it right

view this post on Zulip Mario Carneiro (May 12 2019 at 06:52):

Or add a section common problems: "file not found in LEAN_PATH" -> did you open the folder in VSCode?

view this post on Zulip Scott Morrison (May 12 2019 at 07:00):

I wonder if we can provide some help via the Lean extension.

view this post on Zulip Scott Morrison (May 12 2019 at 07:01):

e.g. if you open any Lean file, but then open folder does not directly contain a leanpkg.toml, pop-up a warning message

view this post on Zulip Scott Morrison (May 12 2019 at 07:01):

It seems one always always wants a leanpkg.toml file, so hopefully this wouldn't by annoying to anyone.

view this post on Zulip Mario Carneiro (May 12 2019 at 07:02):

speaking of the lean extension, whenever the lean server crashes I get a "install lean" button in the popup; is this intentional?

view this post on Zulip Mario Carneiro (May 12 2019 at 07:03):

you can use loose lean files though if you've set up your profile folder appropriately

view this post on Zulip Johan Commelin (May 12 2019 at 07:03):

I think I had some crashes recently, and didn't see that button.

view this post on Zulip Scott Morrison (May 12 2019 at 07:03):

grah, no, that's not intentional.

view this post on Zulip Scott Morrison (May 12 2019 at 07:04):

I haven't been seeing that (on mine or my students' computers; although I've been seeing crashes on both!)

view this post on Zulip Mario Carneiro (May 12 2019 at 07:05):

pasted image

view this post on Zulip Mario Carneiro (May 12 2019 at 07:05):

that's just after force quitting lean from task manager

view this post on Zulip Mario Carneiro (May 12 2019 at 07:06):

maybe it's a windows thing?

view this post on Zulip Keeley Hoek (May 12 2019 at 12:11):

It happens to me on Ubuntu too

view this post on Zulip Kevin Buzzard (May 12 2019 at 12:12):

Oh I've never seen this on Ubuntu -- how to make it happen?

view this post on Zulip Patrick Massot (May 12 2019 at 12:13):

Unfortunately this whole idea of installing Lean from VScode never worked reliably. That's why it's no longer mentioned in our documentation. I think providing one-line (or one-click) installation procedure (as in https://github.com/leanprover-community/mathlib/blob/master/docs/install/debian.md) is a much better idea.

view this post on Zulip Patrick Massot (May 12 2019 at 12:15):

Note that this one line procedure includes installing VScode and the Lean extension

view this post on Zulip Scott Morrison (May 12 2019 at 23:14):

@Patrick Massot, do you want to rip out the code from the VSCode extension that offers to do this, then?

view this post on Zulip Quinn Culver (Oct 20 2019 at 01:54):

I'm having difficulty surmounting the "file not found in the LEAN_PATH" error. i get the error in emacs and vscode. my guess is i need to set the LEAN_PATH variable, but I don't know what to set it to. any assistance would be much appreciated.

view this post on Zulip Mario Carneiro (Oct 20 2019 at 01:59):

you shouldn't actually set the LEAN_PATH variable

view this post on Zulip Bryan Gin-ge Chen (Oct 20 2019 at 01:59):

What steps did you follow before you got this error? Are you working with a Lean project that you created with leanpkg?

view this post on Zulip Mario Carneiro (Oct 20 2019 at 02:00):

the way lean learns where files are is through a leanpkg.path file that should be in some parent directory of the .lean file

view this post on Zulip Mario Carneiro (Oct 20 2019 at 02:00):

it is automatically created by leanpkg

view this post on Zulip Bryan Gin-ge Chen (Oct 20 2019 at 02:00):

You can get this error if you open a Lean file directly in VS Code. You should always open the directory containing a Lean package in VS Code.

view this post on Zulip Quinn Culver (Oct 20 2019 at 02:07):

I'm pretty sure I opened the directory

view this post on Zulip Quinn Culver (Oct 20 2019 at 02:08):

first I tried just downloading the tar.gz file containing the binary, extracting it, and then installing lean mode. that worked, in that it could compile things like "constant : m nat."

view this post on Zulip Quinn Culver (Oct 20 2019 at 02:09):

but "import standard" gave the aformentioned error

view this post on Zulip Quinn Culver (Oct 20 2019 at 02:09):

so i tried messing with the LEAN_PATH variable (to no avail). and then just ran the script here: https://github.com/leanprover-community/mathlib/blob/master/docs/install/debian.md.

view this post on Zulip Quinn Culver (Oct 20 2019 at 02:10):

and then followed the instructions here: https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md.

view this post on Zulip Mario Carneiro (Oct 20 2019 at 02:13):

I don't know what import standard is

view this post on Zulip Mario Carneiro (Oct 20 2019 at 02:13):

do you have a lean file called standard.lean?

view this post on Zulip Mario Carneiro (Oct 20 2019 at 02:14):

There is a default import, called init. It is as if you wrote import init at the top of the file. If you don't see an error on an empty file, then it was at least able to find the core library

view this post on Zulip Mario Carneiro (Oct 20 2019 at 02:14):

What are you trying to import? Mathlib? or one of your own files?

view this post on Zulip Mario Carneiro (Oct 20 2019 at 02:15):

If you have mathlib (it sounds like you don't) then things like import logic.basic should work

view this post on Zulip Mario Carneiro (Oct 20 2019 at 02:16):

If you want to test out imports from the core library, try import data.buffer

view this post on Zulip Quinn Culver (Oct 20 2019 at 02:17):

i think i found "import standard" in the tutorial; but I also got the same error when using "import topology.basic", which I got from the second link I posted above. it says there to use that to test if everything is working.

view this post on Zulip Mario Carneiro (Oct 20 2019 at 02:17):

Do you have a file called leanpkg.path at your project root?

view this post on Zulip Mario Carneiro (Oct 20 2019 at 02:17):

what is in it?

view this post on Zulip Quinn Culver (Oct 20 2019 at 02:18):

builtin_path
path ./src

view this post on Zulip Mario Carneiro (Oct 20 2019 at 02:20):

that means that leanpkg ran but it did not add mathlib as a dependency

view this post on Zulip Quinn Culver (Oct 20 2019 at 02:20):

(if you have tips on how to better typeset the quoting of that file or other code, i'd be happy to know)

view this post on Zulip Mario Carneiro (Oct 20 2019 at 02:20):

do you have a leanpkg.toml file?

view this post on Zulip Mario Carneiro (Oct 20 2019 at 02:20):

Use backquotes to enclose code, and triple backquote to enclose multiline code

view this post on Zulip Bryan Gin-ge Chen (Oct 20 2019 at 02:20):

Try running these steps again, from the root of your my_project directory:

 leanpkg add leanprover-community/mathlib
 update-mathlib

view this post on Zulip Mario Carneiro (Oct 20 2019 at 02:21):

```lean ... ``` gives you syntax highlighting for lean

view this post on Zulip Bryan Gin-ge Chen (Oct 20 2019 at 02:22):

(There's also formatting help if you click on the "A" icon below the text input in Zulip.)

view this post on Zulip Quinn Culver (Oct 20 2019 at 02:24):

@Mario Carneiro yes, I see also in the my_project directory a leanpkg.toml file

view this post on Zulip Quinn Culver (Oct 20 2019 at 02:25):

its contents are

[package]
name = "my_project"
version = "0.1"
lean_version = "3.4.2"
path = "src"

[dependencies]

view this post on Zulip Mario Carneiro (Oct 20 2019 at 02:25):

there should be a line like this one from the tutorial:

[dependencies]
mathlib = {git = "https://github.com/leanprover-community/mathlib", rev = "27515619bcd834006f2936b292021135496b4efb"}

view this post on Zulip Mario Carneiro (Oct 20 2019 at 02:25):

triple backquote on its own line

view this post on Zulip Bryan Gin-ge Chen (Oct 20 2019 at 02:26):

The [dependencies] section should get filled in when you run leanpkg add leanprover-community/mathlib

view this post on Zulip Quinn Culver (Oct 20 2019 at 02:26):

I will try that @Bryan Gin-ge Chen.

view this post on Zulip Mario Carneiro (Oct 20 2019 at 02:27):

for some reason that command is missing from the install directions?

view this post on Zulip Bryan Gin-ge Chen (Oct 20 2019 at 02:27):

No, it's there.

view this post on Zulip Mario Carneiro (Oct 20 2019 at 02:28):

oh I see, it's not in the tutorial example, but that already has mathlib

view this post on Zulip Bryan Gin-ge Chen (Oct 20 2019 at 02:28):

Yeah, I'm just looking at the first part of docs/install/project.md.

view this post on Zulip Quinn Culver (Oct 20 2019 at 02:29):

Success! @Bryan Gin-ge Chen @Mario Carneiro

view this post on Zulip Quinn Culver (Oct 20 2019 at 02:29):

(deleted)

view this post on Zulip Quinn Culver (Oct 20 2019 at 02:30):

quinn@quinn-lemus:~/Documents/Lean/my_project/src$ lean learnlean.lean
topological_space : Type u_1 → Type u_1

view this post on Zulip Quinn Culver (Oct 20 2019 at 02:30):

<3

view this post on Zulip Quinn Culver (Oct 20 2019 at 02:30):

Thanks a lot, guys.


Last updated: May 08 2021 at 03:17 UTC