File not found in LEAN_PATH

Stream: new members

[Maxim Gerspach]

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.

[Johan Commelin]

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

[Maxim Gerspach]

I used the Lean extension for VScode.

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

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

[Maxim Gerspach]

I followed scenario 1.
leanpkg.path says

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

[Maxim Gerspach]

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.

[Reid Barton]

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

[Reid Barton]

Try for example import algebra.ring

[Maxim Gerspach]

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

[Bryan Gin-ge Chen]

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?

[Maxim Gerspach]

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.

[Kevin Buzzard]

Did you "open folder" in VS Code?

[Kevin Buzzard]

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

[Simon Hudon]

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

[Maxim Gerspach]

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

[Maxim Gerspach]

And thanks for the talk at Warwick yesterday, Kevin!

[Kevin Buzzard]

Hah! Thanks for coming!

[Kevin Buzzard]

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.

[Moses Schönfinkel]

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

[Patrick Massot]

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

[Moses Schönfinkel]

Ah, I had no idea! Well done.

[Patrick Massot]

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

[Kevin Buzzard]

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

[Patrick Massot]

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

[Moses Schönfinkel]

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

[Patrick Massot]

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

[Andrew Ashworth]

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

[Andrew Ashworth]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Scott Morrison]

grah, no, that's not intentional.

[Scott Morrison]

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

[Mario Carneiro]

pasted image

[Mario Carneiro]

that's just after force quitting lean from task manager

[Mario Carneiro]

maybe it's a windows thing?

[Keeley Hoek]

It happens to me on Ubuntu too

[Kevin Buzzard]

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

[Patrick Massot]

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.

[Patrick Massot]

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

[Scott Morrison]

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

[Quinn Culver]

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.

[Mario Carneiro]

you shouldn't actually set the LEAN_PATH variable

[Bryan Gin-ge Chen]

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

[Mario Carneiro]

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

[Mario Carneiro]

it is automatically created by leanpkg

[Bryan Gin-ge Chen]

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.

[Quinn Culver]

I'm pretty sure I opened the directory

[Quinn Culver]

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."

[Quinn Culver]

but "import standard" gave the aformentioned error

[Quinn Culver]

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.

[Quinn Culver]

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

[Mario Carneiro]

I don't know what import standard is

[Mario Carneiro]

do you have a lean file called standard.lean?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Quinn Culver]

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.

[Mario Carneiro]

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

[Mario Carneiro]

what is in it?

[Quinn Culver]

builtin_path
path ./src

[Mario Carneiro]

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

[Quinn Culver]

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

[Mario Carneiro]

do you have a leanpkg.toml file?

[Mario Carneiro]

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

[Bryan Gin-ge Chen]

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

 leanpkg add leanprover-community/mathlib
 update-mathlib

[Mario Carneiro]

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

[Bryan Gin-ge Chen]

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

[Quinn Culver]

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

[Quinn Culver]

its contents are

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

[dependencies]

[Mario Carneiro]

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

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

[Mario Carneiro]

triple backquote on its own line

[Bryan Gin-ge Chen]

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

[Quinn Culver]

I will try that @Bryan Gin-ge Chen.

[Mario Carneiro]

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

[Bryan Gin-ge Chen]

No, it's there.

[Mario Carneiro]

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

[Bryan Gin-ge Chen]

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

[Quinn Culver]

Success! @Bryan Gin-ge Chen @Mario Carneiro

[Quinn Culver]

(deleted)

[Quinn Culver]

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

[Quinn Culver]

<3

[Quinn Culver]

Thanks a lot, guys.