Cannot Import topology.basic

Stream: new members

[Carlo Cabrera]

Hi, I'm trying to get started with Lean, so I installed Lean, elan, and mathlib exactly as on the link here: https://github.com/leanprover-community/mathlib/blob/master/docs/install/macos.md

I then tried to follow the instructions on https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md#working-on-an-existing-package but when I tried the command "import topology.basic" I get the following error "file 'topology/basic' not found in the LEAN_PATH". (#eval 1+1 works, though.)

No idea what I'm doing wrong, and I can't find any documentation on what's supposed to be in my LEAN_PATH and how to fix it.

I've read through the discussion here, which seems to be a similar problem to mine, but I haven't gotten anywhere: https://leanprover-community.github.io/archive/stream/113489-new-members/topic/Cannot.20start.20tutorials.2C.20nor.20import.20topology.2Ebasic.2C.20nor.2E.2E.2E.html

[Johan Commelin]

Where did you try that command?

[Kevin Buzzard]

did you correctly make a new new Lean project and open the entire project in VS Code?

[Kevin Buzzard]

Can you send a screenshot?

[Patrick Massot]

The most frequent source is opening the wrong folder

[Mario Carneiro]

The docs should mention this error text

[Carlo Cabrera]

I tried the command in VS Code. I started a new Lean project. Will post a screenshot.

[Patrick Massot]

Especially a screenshot of the file explorer of VScode

[Mario Carneiro]

and also that changing the LEAN_PATH is not the answer

[Kevin Buzzard]

and if you already changed it, tell us now!

[Reid Barton]

as I understand it the line "If you launched VS Code from a menu, on the main screen, or in the File menu, click "Open folder" (just "Open" on a Mac), and choose the folder tutorials (not one of its subfolders)." should also have some kind of special emphasis

[Carlo Cabrera]

Here is a screenshot. Screenshot-2020-05-09-15.44.34.png

[Kevin Buzzard]

your package is corrupt

[Kevin Buzzard]

why are leanpkg.toml and leanpkfg.path in src? They are not Lean files

[Patrick Massot]

That looks pretty good. Did you change anything by hand inside leanpkg.toml

[Patrick Massot]

I don't think there are in src

[Reid Barton]

the triangle is :play: not :red_triangle_down:

[Patrick Massot]

The src folder seems folded

[Kevin Buzzard]

Aah, then the question becomes: why are your Lean files not in src? But that will not fix the problem :-(

[Carlo Cabrera]

Good question. I tried leanpkg build and leanproject build (no idea what those do, but I thought it was worth a try) when I got the error, and that seems to have produced those files.

Yes, the test file is not in the src folder. Of course it should be. Let me try moving it there

[Mario Carneiro]

Any comments on changing the error message to "file '" << fname << "' not found in the search path"?

[Reid Barton]

If TPWL is a non-mathlib project then shouldn't there be a _target directory?

[Patrick Massot]

Carlo, could you tell us exactly what commands you typed?

[Reid Barton]

Or does this look different in vscode somehow?

[Reid Barton]

I mean if mathlib is a dependency and has already been acquired

[Patrick Massot]

It looks like you mixed creating a new project and getting an existing one

[Kevin Buzzard]

oh wait where is _target?

[Mario Carneiro]

We could put a paragraph of explanation about maybe you didn't import mathlib but this is a very generic kind of error

[Carlo Cabrera]

TPWL was created via leanproject new TPWL.

[Kevin Buzzard]

did you get any errors when you typed that command?

[Reid Barton]

The instructions at https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md don't actually contain any commands involving mathlib, is this correct?

[Reid Barton]

Does leanproject just automatically assume you want mathlib?

[Carlo Cabrera]

Kevin Buzzard said:

did you get any errors when you typed that command?

I did not.

[Kevin Buzzard]

i thought it did, but my version just didn't

[Carlo Cabrera]

I moved test.lean to the src folder, but, as suggsted, that hasn't changed anything.

[Kevin Buzzard]

Your problem is that you are missing a maths library

[Kevin Buzzard]

which is kind of important

[Carlo Cabrera]

Kevin Buzzard said:

Your problem is that you are missing a maths library

Yes, that I understand. I just don't know how to install the needed library.

[Kevin Buzzard]

I was hoping leanproject add-mathlib would work but I can't get it to

[Patrick Massot]

leanpoject new TPWL should have done everything

[Carlo Cabrera]

The documentation (or, well, my probable misreading of it) suggested all I needed to do was install mathlibtools (and elan), but that doesn't seem to have worked

[Reid Barton]

is it related to https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/leanproject.20up.3F/near/196986746 ?

[Kevin Buzzard]

leanproject new TPWL is not downloading mathlib for me

[Patrick Massot]

Oh yes, this is this 3-11-0 bug!

[Patrick Massot]

Sorry about that, you are simply very unlucky

[Patrick Massot]

You should upgrade mathlibtools now

[Kevin Buzzard]

Is there an easy way to do that?

[Kevin Buzzard]

I don't just want to uninstall and re-install if there's a trick

[Patrick Massot]

pip install --upgrade mathlibtools

[Kevin Buzzard]

Should I type workon (something) first?

[Carlo Cabrera]

Patrick Massot said:

You should upgrade mathlibtools now

I believe I had done that before posting here. Let me try again. Is it important which folder I run it in? (Sorry, possibly dumb question, I have no idea how these packages work.)

[Kevin Buzzard]

And should I run pip3 not pip?

[Patrick Massot]

Reid Barton said:

Does leanproject just automatically assume you want mathlib?

Yes.

[Reid Barton]

Carlo Cabrera said:

Patrick Massot said:

You should upgrade mathlibtools now

I believe I had done that before posting here

In that case, you won't have downloaded the version from 3 minutes ago. :upside_down:

[Kevin Buzzard]

OK I upgraded and it's working again

[Kevin Buzzard]

(with workon and pip3)

[Patrick Massot]

Carlo Cabrera said:

Patrick Massot said:

You should upgrade mathlibtools now

I believe I had done that before posting here. Let me try again. Is it important which folder I run it in? (Sorry, possibly dumb question, I have no idea how these packages work.)

It depends on your python setup. If you don't know then most probably it's not important

[Patrick Massot]

Same for Kevin's question: whether it's pip or pip3 depends on your python setup.

[Patrick Massot]

Mario Carneiro said:

Any comments on changing the error message to "file '" << fname << "' not found in the search path"?

This is a change in Lean core, right? If we are changing this message, could we even add some troubleshooting advice? Or maybe a url (this would need to wait for the new website)?

[Carlo Cabrera]

Upgrading mathlibtools seems to have worked. Started a project from scratch. Thanks for the help!

[Patrick Massot]

You've been very unlucky. This was broken since less than 24 hours.

[Carlo Cabrera]

Patrick Massot said:

You've been very unlucky. This was broken since less than 24 hours.

Yea, I discovered this last night. Gave up on it for the night and decided to try again today. Finally came here when various Google searches didn't work.

[Patrick Massot]

Sorry about that. Have fun with Lean now!

[Mario Carneiro]

Patrick Massot said:

Mario Carneiro said:

Any comments on changing the error message to "file '" << fname << "' not found in the search path"?

This is a change in Lean core, right? If we are changing this message, could we even add some troubleshooting advice? Or maybe a url (this would need to wait for the new website)?

Sure, we could add some advice here, but keep in mind this is just the generic "file not found" message. It also shows up whenever you are adding or changing imports, or you misspelled something, and it doesn't necessarily have to do with importing a file in mathlib, it could just be the user's own file.

[Mario Carneiro]

If you can come up with useful advice that is generic over all that, be my guest

[Johan Commelin]

@Carlo Cabrera Sorry, sorry, sorry. I was the one who broke leanproject by creating an "evil" branch name in git. I apologise for the pain.

[Mario Carneiro]

How about file 'foo' not found in the search path. Use 'lean --path' to see where lean is looking, or http://leanproject.github.io/file-not-found for more

[Johan Commelin]

Mario Carneiro said:

If you can come up with useful advice that is generic over all that, be my guest

The error message could start with being generic, but could include a line towards the end:
"Are you setting up your first Lean project, and seeing this error message? The problem might be: ..."

[Johan Commelin]

Mario Carneiro said:

How about file 'foo' not found in the search path. Use 'lean --path' to see where lean is looking, or http://leanproject.github.io/file-not-found for more

Do change the URL to the community project though!

[Mario Carneiro]

oops, that is a nonsense url for more reasons than one

[Reid Barton]

it would produce an appropriate error message though

[Carlo Cabrera]

Johan Commelin said:

Carlo Cabrera Sorry, sorry, sorry. I was the one who broke leanproject by creating an "evil" branch name in git. I apologise for the pain.

No harm done. I'd been meaning to pick Lean up for quite a while now. Just says I should've picked it up properly much earlier!

[Mario Carneiro]

Obviously we would need to create this file-not-found landing page; I don't think there is a good place to link right now

[Gabriel Ebner]

Who would like to write the file-not-found page? lean#253

[Bryan Gin-ge Chen]

I made a start, but it needs more: https://github.com/leanprover-community/leanprover-community.github.io/pull/23

[Brandon Wu]

I ran pip3 install --upgrade mathlibtools and I'm getting an error invalid import: data.real.basic could not resolve import: data.real.basic on 00_first_proofs.lean. I'm unsure if this is the same issue, but I don't know why it says that I've already upgraded mathlibtools and I'm still getting it. Any help would be appreciated!

[Brandon Wu]

Update: I've just reinstalled everything and run a few commands, and I'm good now.

[Brandon Wu]

Update update: Curiously, today I tried to open up the same tutorial that was working just yesterday, and now I'm getting the same error. I'm not too sure what's going on here.

[Brandon Wu]

I'm also getting a leanpkg.path does not exist error in Code.

[Brandon Wu]

My lean --path says that my leanpkg_path_file is /home/<my_name>/.lean/leanpkg.path, except I've just verified that /home/<my_name>/.lean does not actually exist.

[Bryan Gin-ge Chen]

Did you open the directory in VS Code or just the file you were looking at? You have to open the root directory of the package for the extension to work properly.

[Brandon Wu]

I opened the directory tutorials in VS Code.

[Brandon Wu]

It prompted me for some leanpkg config on startup, so I did that, and what changed is that now on the tutorial file, VS Code hangs for a bit with some orange colors at the left, and then it gives me a ton of memory consumption errors like invalid import: data.option.defs excessive memory consumption detected at 'expression traversal' (potential solution: increase memory consumption threshold).

[Kevin Buzzard]

Restart lean?

[Brandon Wu]

I uninstalled and reinstalled the extension, if that's sufficient. I'm still getting the same error, though.

[Bryan Gin-ge Chen]

The orange colors appear if Lean can't find compiled .olean files so it starts to compile mathlib.

[Bryan Gin-ge Chen]

You may need to rerun leanproject get-mathlib-cache.

[Bryan Gin-ge Chen]

Here's a precise list of steps that should get tutorials/ working for you from scratch: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/customizing.20vscode/near/202794235

If you already have a tutorials directory, then leanproject get-mathlib-cache should download olean files for mathlib for you.

[Brandon Wu]

leanproject get-mathlib-cache appears to result in an Invalid git respository for me.

[Brandon Wu]

Additionally, removing tutorials then running leanproject get tutorials gives me a No such file or directory: 'leanpkg' (though it does make the tutorials folder come back)

[Brandon Wu]

Ok, so I tried using elan and despite the fact I have not restarted my computer (nor even closed my terminal) since the last time I had it working, elan was for some reason not recognized by my shell.
I then proceeded to again delete tutorials and use leanproject get tutorials, which actually caused it to work. I am now in the tutorial and Lean is working as usual.

[Brandon Wu]

This whole chain of events is really quite confusing and I'm not sure what's going on. I might be back tomorrow if it starts spontaneously not working again.

[Bryan Gin-ge Chen]

Sorry for the frustration. If you don't mind sharing some more information about your system (e.g. what operating system you're using, what python you're using, how you installed elan and leanproject) and what steps you took to get to the various broken states (if you can remember), that would greatly help us figure out how to help you and possibly improve our instructions as well.

[Brandon Wu]

I am running Arch Linux, python 3. I installed elan through the curl https://raw.githubusercontent.com/Kha/elan/master/elan-init.sh -sSf | sh command that was given, and I presumably obtained leanproject through sudo pip3 install mathlibtools. I essentially just followed the instructions given by https://leanprover-community.github.io/install/linux.html.

[Bryan Gin-ge Chen]

OK, so far so good. Are things still working after you ran leanproject get tutorials?

[Brandon Wu]

I think that they are for now. Thanks for the help!