## Stream: new members

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

#### Johan Commelin (May 11 2019 at 14:12):

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

#### Maxim Gerspach (May 11 2019 at 14:17):

I used the Lean extension for VScode.

#### Bryan Gin-ge Chen (May 11 2019 at 14:21):

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

#### Bryan Gin-ge Chen (May 11 2019 at 14:23):

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

#### Maxim Gerspach (May 11 2019 at 14:28):

I followed scenario 1.
leanpkg.path says

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

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

#### Reid Barton (May 11 2019 at 14:34):

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

#### Reid Barton (May 11 2019 at 14:40):

Try for example import algebra.ring

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

#### 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?

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

#### Kevin Buzzard (May 11 2019 at 15:59):

Did you "open folder" in VS Code?

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

#### 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

#### 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!

#### Maxim Gerspach (May 11 2019 at 16:18):

And thanks for the talk at Warwick yesterday, Kevin!

#### Kevin Buzzard (May 11 2019 at 16:18):

Hah! Thanks for coming!

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

#### Moses Schönfinkel (May 11 2019 at 16:19):

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

#### 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

#### Moses Schönfinkel (May 11 2019 at 16:20):

Ah, I had no idea! Well done.

#### 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

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

#### Patrick Massot (May 11 2019 at 16:21):

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

#### Moses Schönfinkel (May 11 2019 at 16:22):

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

#### 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

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

#### 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

#### 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?

#### Scott Morrison (May 12 2019 at 07:00):

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

#### 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

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

#### 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?

#### Mario Carneiro (May 12 2019 at 07:03):

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

#### Johan Commelin (May 12 2019 at 07:03):

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

#### Scott Morrison (May 12 2019 at 07:03):

grah, no, that's not intentional.

#### 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!)

pasted image

#### Mario Carneiro (May 12 2019 at 07:05):

that's just after force quitting lean from task manager

#### Mario Carneiro (May 12 2019 at 07:06):

maybe it's a windows thing?

#### Keeley Hoek (May 12 2019 at 12:11):

It happens to me on Ubuntu too

#### Kevin Buzzard (May 12 2019 at 12:12):

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

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

#### Patrick Massot (May 12 2019 at 12:15):

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

#### 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?

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

#### Mario Carneiro (Oct 20 2019 at 01:59):

you shouldn't actually set the LEAN_PATH variable

#### 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?

#### 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

#### Mario Carneiro (Oct 20 2019 at 02:00):

it is automatically created by leanpkg

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

#### Quinn Culver (Oct 20 2019 at 02:07):

I'm pretty sure I opened the directory

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

#### Quinn Culver (Oct 20 2019 at 02:09):

but "import standard" gave the aformentioned error

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

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

#### Mario Carneiro (Oct 20 2019 at 02:13):

I don't know what import standard is

#### Mario Carneiro (Oct 20 2019 at 02:13):

do you have a lean file called standard.lean?

#### 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

#### Mario Carneiro (Oct 20 2019 at 02:14):

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

#### 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

#### Mario Carneiro (Oct 20 2019 at 02:16):

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

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

#### Mario Carneiro (Oct 20 2019 at 02:17):

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

what is in it?

builtin_path
path ./src

#### Mario Carneiro (Oct 20 2019 at 02:20):

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

#### 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)

#### Mario Carneiro (Oct 20 2019 at 02:20):

do you have a leanpkg.toml file?

#### Mario Carneiro (Oct 20 2019 at 02:20):

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

#### 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


#### Mario Carneiro (Oct 20 2019 at 02:21):

 lean ...   gives you syntax highlighting for lean

#### 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.)

#### Quinn Culver (Oct 20 2019 at 02:24):

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

#### 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]


#### 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"}


#### Mario Carneiro (Oct 20 2019 at 02:25):

triple backquote on its own line

#### 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

#### Quinn Culver (Oct 20 2019 at 02:26):

I will try that @Bryan Gin-ge Chen.

#### Mario Carneiro (Oct 20 2019 at 02:27):

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

No, it's there.

#### Mario Carneiro (Oct 20 2019 at 02:28):

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

#### Bryan Gin-ge Chen (Oct 20 2019 at 02:28):

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

#### Quinn Culver (Oct 20 2019 at 02:29):

Success! @Bryan Gin-ge Chen @Mario Carneiro

(deleted)

#### 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


<3

#### Quinn Culver (Oct 20 2019 at 02:30):

Thanks a lot, guys.

Last updated: May 08 2021 at 03:17 UTC