Zulip Chat Archive

Stream: new members

Topic: Cannot Import topology.basic


view this post on Zulip Carlo Cabrera (May 09 2020 at 14:42):

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

view this post on Zulip Johan Commelin (May 09 2020 at 14:43):

Where did you try that command?

view this post on Zulip Kevin Buzzard (May 09 2020 at 14:43):

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

view this post on Zulip Kevin Buzzard (May 09 2020 at 14:44):

Can you send a screenshot?

view this post on Zulip Patrick Massot (May 09 2020 at 14:44):

The most frequent source is opening the wrong folder

view this post on Zulip Mario Carneiro (May 09 2020 at 14:44):

The docs should mention this error text

view this post on Zulip Carlo Cabrera (May 09 2020 at 14:44):

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

view this post on Zulip Patrick Massot (May 09 2020 at 14:44):

Especially a screenshot of the file explorer of VScode

view this post on Zulip Mario Carneiro (May 09 2020 at 14:44):

and also that changing the LEAN_PATH is not the answer

view this post on Zulip Kevin Buzzard (May 09 2020 at 14:44):

and if you already changed it, tell us now!

view this post on Zulip Reid Barton (May 09 2020 at 14:45):

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

view this post on Zulip Carlo Cabrera (May 09 2020 at 14:45):

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

view this post on Zulip Kevin Buzzard (May 09 2020 at 14:46):

your package is corrupt

view this post on Zulip Kevin Buzzard (May 09 2020 at 14:46):

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

view this post on Zulip Patrick Massot (May 09 2020 at 14:46):

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

view this post on Zulip Patrick Massot (May 09 2020 at 14:46):

I don't think there are in src

view this post on Zulip Reid Barton (May 09 2020 at 14:47):

the triangle is :play: not :red_triangle_down:

view this post on Zulip Patrick Massot (May 09 2020 at 14:47):

The src folder seems folded

view this post on Zulip Kevin Buzzard (May 09 2020 at 14:47):

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

view this post on Zulip Carlo Cabrera (May 09 2020 at 14:48):

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

view this post on Zulip Mario Carneiro (May 09 2020 at 14:48):

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

view this post on Zulip Reid Barton (May 09 2020 at 14:48):

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

view this post on Zulip Patrick Massot (May 09 2020 at 14:49):

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

view this post on Zulip Reid Barton (May 09 2020 at 14:49):

Or does this look different in vscode somehow?

view this post on Zulip Reid Barton (May 09 2020 at 14:49):

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

view this post on Zulip Patrick Massot (May 09 2020 at 14:49):

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

view this post on Zulip Kevin Buzzard (May 09 2020 at 14:49):

oh wait where is _target?

view this post on Zulip Mario Carneiro (May 09 2020 at 14:49):

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

view this post on Zulip Carlo Cabrera (May 09 2020 at 14:49):

TPWL was created via leanproject new TPWL.

view this post on Zulip Kevin Buzzard (May 09 2020 at 14:50):

did you get any errors when you typed that command?

view this post on Zulip Reid Barton (May 09 2020 at 14:50):

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?

view this post on Zulip Reid Barton (May 09 2020 at 14:50):

Does leanproject just automatically assume you want mathlib?

view this post on Zulip Carlo Cabrera (May 09 2020 at 14:50):

Kevin Buzzard said:

did you get any errors when you typed that command?

I did not.

view this post on Zulip Kevin Buzzard (May 09 2020 at 14:51):

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

view this post on Zulip Carlo Cabrera (May 09 2020 at 14:51):

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

view this post on Zulip Kevin Buzzard (May 09 2020 at 14:51):

Your problem is that you are missing a maths library

view this post on Zulip Kevin Buzzard (May 09 2020 at 14:52):

which is kind of important

view this post on Zulip Carlo Cabrera (May 09 2020 at 14:52):

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.

view this post on Zulip Kevin Buzzard (May 09 2020 at 14:52):

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

view this post on Zulip Patrick Massot (May 09 2020 at 14:52):

leanpoject new TPWL should have done everything

view this post on Zulip Carlo Cabrera (May 09 2020 at 14:53):

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

view this post on Zulip Reid Barton (May 09 2020 at 14:53):

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

view this post on Zulip Kevin Buzzard (May 09 2020 at 14:53):

leanproject new TPWL is not downloading mathlib for me

view this post on Zulip Patrick Massot (May 09 2020 at 14:54):

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

view this post on Zulip Patrick Massot (May 09 2020 at 14:54):

Sorry about that, you are simply very unlucky

view this post on Zulip Patrick Massot (May 09 2020 at 14:54):

You should upgrade mathlibtools now

view this post on Zulip Kevin Buzzard (May 09 2020 at 14:55):

Is there an easy way to do that?

view this post on Zulip Kevin Buzzard (May 09 2020 at 14:55):

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

view this post on Zulip Patrick Massot (May 09 2020 at 14:55):

pip install --upgrade mathlibtools

view this post on Zulip Kevin Buzzard (May 09 2020 at 14:55):

Should I type workon (something) first?

view this post on Zulip Carlo Cabrera (May 09 2020 at 14:55):

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

view this post on Zulip Kevin Buzzard (May 09 2020 at 14:55):

And should I run pip3 not pip?

view this post on Zulip Patrick Massot (May 09 2020 at 14:56):

Reid Barton said:

Does leanproject just automatically assume you want mathlib?

Yes.

view this post on Zulip Reid Barton (May 09 2020 at 14:57):

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:

view this post on Zulip Kevin Buzzard (May 09 2020 at 14:57):

OK I upgraded and it's working again

view this post on Zulip Kevin Buzzard (May 09 2020 at 14:58):

(with workon and pip3)

view this post on Zulip Patrick Massot (May 09 2020 at 14:58):

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

view this post on Zulip Patrick Massot (May 09 2020 at 14:58):

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

view this post on Zulip Patrick Massot (May 09 2020 at 15:02):

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

view this post on Zulip Carlo Cabrera (May 09 2020 at 15:02):

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

view this post on Zulip Patrick Massot (May 09 2020 at 15:03):

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

view this post on Zulip Carlo Cabrera (May 09 2020 at 15:03):

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.

view this post on Zulip Patrick Massot (May 09 2020 at 15:07):

Sorry about that. Have fun with Lean now!

view this post on Zulip Mario Carneiro (May 09 2020 at 15:14):

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.

view this post on Zulip Mario Carneiro (May 09 2020 at 15:15):

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

view this post on Zulip Johan Commelin (May 09 2020 at 15:19):

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

view this post on Zulip Mario Carneiro (May 09 2020 at 15:20):

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

view this post on Zulip Johan Commelin (May 09 2020 at 15:20):

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

view this post on Zulip Johan Commelin (May 09 2020 at 15:22):

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!

view this post on Zulip Mario Carneiro (May 09 2020 at 15:22):

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

view this post on Zulip Reid Barton (May 09 2020 at 15:23):

it would produce an appropriate error message though

view this post on Zulip Carlo Cabrera (May 09 2020 at 15:23):

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!

view this post on Zulip Mario Carneiro (May 09 2020 at 15:24):

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

view this post on Zulip Gabriel Ebner (May 19 2020 at 16:55):

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

view this post on Zulip Bryan Gin-ge Chen (May 19 2020 at 23:20):

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

view this post on Zulip Brandon Wu (Jul 04 2020 at 00:26):

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!

view this post on Zulip Brandon Wu (Jul 04 2020 at 00:42):

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

view this post on Zulip Brandon Wu (Jul 04 2020 at 22:54):

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.

view this post on Zulip Brandon Wu (Jul 04 2020 at 23:20):

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

view this post on Zulip Brandon Wu (Jul 04 2020 at 23:22):

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.

view this post on Zulip Bryan Gin-ge Chen (Jul 04 2020 at 23:29):

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.

view this post on Zulip Brandon Wu (Jul 04 2020 at 23:33):

I opened the directory tutorials in VS Code.

view this post on Zulip Brandon Wu (Jul 04 2020 at 23:33):

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

view this post on Zulip Kevin Buzzard (Jul 04 2020 at 23:44):

Restart lean?

view this post on Zulip Brandon Wu (Jul 04 2020 at 23:46):

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

view this post on Zulip Bryan Gin-ge Chen (Jul 05 2020 at 00:11):

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

view this post on Zulip Bryan Gin-ge Chen (Jul 05 2020 at 00:14):

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

view this post on Zulip Bryan Gin-ge Chen (Jul 05 2020 at 00:15):

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.

view this post on Zulip Brandon Wu (Jul 05 2020 at 01:02):

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

view this post on Zulip Brandon Wu (Jul 05 2020 at 01:03):

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)

view this post on Zulip Brandon Wu (Jul 05 2020 at 01:13):

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.

view this post on Zulip Brandon Wu (Jul 05 2020 at 01:13):

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.

view this post on Zulip Bryan Gin-ge Chen (Jul 05 2020 at 03:31):

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.

view this post on Zulip Brandon Wu (Jul 05 2020 at 19:19):

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.

view this post on Zulip Bryan Gin-ge Chen (Jul 05 2020 at 19:35):

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

view this post on Zulip Brandon Wu (Jul 07 2020 at 00:32):

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


Last updated: May 10 2021 at 00:31 UTC