Zulip Chat Archive

Stream: new members

Topic: Cannot start tutorials, nor import topology.basic, nor...


Laurent Bartholdi (Feb 19 2020 at 20:59):

I tried to follow the instructions on mathlib to play with the "tutorials" lean project (using emacs, but it's probably not relevant). When I open "src/first_proofs.lean", my laptop just runs for 1/2-hour before I kill it.

I then tried to run just the first 10 lines of the file; same issue.

I then created a tiny file src/yyy.lean in the tutorials directory, containing

import topology.basic

#check topological_space

but it also runs for an enormous amount of time, giving then the weird error message "invalid import: topology.basic" and "/Users/laurent/.../topology/basic.lean:118:18: error: unexpected token". There isn't even anything on line 118 of that file!

I know I must be doing something really stupid, but I can't see what.

For reference, a singe line #check id seems to work fine.

Attached is a screenshot of the emacs window, just in case.

TIA, Laurent Screen-Shot-2020-02-19-at-21.45.12.png

Patrick Massot (Feb 19 2020 at 21:00):

Did you get update-mathlib working?

Laurent Bartholdi (Feb 19 2020 at 21:01):

no :)
I don't have any command with that name

Patrick Massot (Feb 19 2020 at 21:02):

That explains what you see.

Patrick Massot (Feb 19 2020 at 21:02):

Did you follow https://github.com/leanprover-community/mathlib/blob/master/docs/install/macos.md?

Laurent Bartholdi (Feb 19 2020 at 21:03):

Yes, I did

Patrick Massot (Feb 19 2020 at 21:04):

Can you try, in a terminal, source ~/.profile and see if update-mathlib becomes available?

Patrick Massot (Feb 19 2020 at 21:04):

Oh, wait, with the new procedure it shouldn't be relevant to update-mahtlib anymore (depending whether you followed that web page today or a couple of days ago).

Patrick Massot (Feb 19 2020 at 21:05):

You can still try to source, that can't hurt.

Kevin Buzzard (Feb 19 2020 at 21:05):

Without the mathlib olean files you'll have a grim time using Lean. Emacs might well be compiling mathlib every time you open it. Best to get it compiled once and for all I guess.

Alex J. Best (Feb 19 2020 at 21:06):

I just tried https://github.com/leanprover-community/mathlib/blob/master/docs/install/macos.md#installing-mathlib-supporting-tools on my osx and it looks like it worked well. pip installs it all to /usr/local/bin/ and I didn't need to restart terminal or anything

Laurent Bartholdi (Feb 19 2020 at 21:07):

OK, something strange happened. I have update-mathlib installed now. Problem was I had done some cut-and-paste, and the "sudo" prevented the command from being executed (I don't allow sudo from my main login).

How do I get to compile the lean files? update-mathlib was almost instantaneous, and "lean src/yyy.lean" is still running as I type

Patrick Massot (Feb 19 2020 at 21:07):

Actually, I followed those instructions on a Mac today, and everything went fine.

Patrick Massot (Feb 19 2020 at 21:08):

Did that lean command start before update-mathlib?

Patrick Massot (Feb 19 2020 at 21:08):

Is yes then kill it

Patrick Massot (Feb 19 2020 at 21:08):

When you write "update-mathlib was almost instantaneous", did it still output something?

Laurent Bartholdi (Feb 19 2020 at 21:10):

I killed all lean instances, and then reran update-mathlib. Here is the output:

Info: No github 'user'/'password' or 'oauthtoken' keys found in git config, we will use GitHub with no authentication.
You can create an OAuth token at https://github.com/settings/tokens/new (no scopes are required).
Querying GitHub...
Reusing cached olean archive
... successfully extracted olean archive.

But then again running "lean src/yyy.lean" runs forever.

Patrick Massot (Feb 19 2020 at 21:11):

can you list the content of the folder you are in when running this command?

Laurent Bartholdi (Feb 19 2020 at 21:12):

~/src/lean/tutorials 2320[1]+> ls
LICENSE       README.md     _target/      leanpkg.path  leanpkg.toml  src/

Rob Lewis (Feb 19 2020 at 21:12):

Try running find _target | grep "[.]olean$" | xargs touch in that directory.

Patrick Massot (Feb 19 2020 at 21:12):

and what happens if you run leanpkg build in this folder?

Laurent Bartholdi (Feb 19 2020 at 21:21):

Ta-da! Works fine now. Thanks a lot!

Patrick Massot (Feb 19 2020 at 21:22):

What did you do?

Patrick Massot (Feb 19 2020 at 21:22):

Did you used Rob's incantation?

Laurent Bartholdi (Feb 19 2020 at 21:23):

Yes, and then yours.

So, just to make sure: every once in a while, to have the most fancy mathlib, I should run "update-mathlib" and then "leanpkg build"?

Patrick Massot (Feb 19 2020 at 21:23):

Just to make sure: was leanpkg build quick?

Laurent Bartholdi (Feb 19 2020 at 21:24):

No, it took 9 minutes

Laurent Bartholdi (Feb 19 2020 at 21:25):

... with 8 cores heating...

Patrick Massot (Feb 19 2020 at 21:25):

Then there is something really weird going on.

Patrick Massot (Feb 19 2020 at 21:25):

It means you recompiled a lot of things that update-mathlib was meant to bring all compiled to you.

Patrick Massot (Feb 19 2020 at 21:26):

This is so frustrating to remote debug (and there shouldn't be anything to debug).

Kevin Buzzard (Feb 19 2020 at 21:26):

It's probably worth remarking that once you have the olean files, your problems should be solved (i.e. if you try again tomorrow it will just work)

Patrick Massot (Feb 19 2020 at 21:27):

Could you try to start over from a different folder, very carefully following https://github.com/leanprover-community/mathlib/blob/master/docs/install/project.md#working-on-an-existing-package

Kevin Buzzard (Feb 19 2020 at 21:27):

You can check in e.g. _target/deps/mathlib/src/topology to see whether you have as many olean files as lean files

Laurent Bartholdi (Feb 19 2020 at 21:40):

Yes, starting over with a fresh clone is much faster.

I tried deleting all the .olean files in the original directory, and re-running "leanpkg build". It just compiled 151 .olean files, rather than the 613 in the new clone.

BTW, the "update-mathlib" command stopped working in the old directory, reporting "github.GithubException.RateLimitExceededException: 403 {"message": "API rate limit exceeded for 84.140.118.54. (But here's the good news: Authenticated requests get a higher rate limit. Check out the documentation for more details.)", "documentation_url": "https://developer.github.com/v3/#rate-limiting"}"

Perhaps it would be good to have a somewhat authenticated request? Does that only require a username to be specified in the git config?

Patrick Massot (Feb 19 2020 at 21:43):

That API rate limit is really bad. How many times did you ran update-mathlib to hit that?

Patrick Massot (Feb 19 2020 at 21:44):

Anyway, you shouldn't have to delete any of the olean files that update-mathlib brings you, that the whole point of update-mathlib, it download olean files.

Mario Carneiro (Feb 19 2020 at 21:46):

I can't run update-mathlib at all on my work machine, I got the API rate limit on the first try

Mario Carneiro (Feb 19 2020 at 21:47):

We need alternatives for when that call fails

Kevin Buzzard (Feb 19 2020 at 21:47):

leanpkg build ;-)

Kevin Buzzard (Feb 19 2020 at 21:48):

Is this failure a new feature because something changed, or has it always been there? I get it occasionally

Laurent Bartholdi (Feb 19 2020 at 21:48):

I think 4 times.

Not to worry, I started a VPN to the university and got a fresh new IP address :)

Rob Lewis (Feb 19 2020 at 21:48):

Self hosting the build artifacts is still on the to-do list.

Mario Carneiro (Feb 19 2020 at 21:48):

It would be nice if there were instructions for how to do the thing update-mathlib does manually

Patrick Massot (Feb 19 2020 at 21:49):

The painful part is to get the nightly matching the commit indicated in leanpkg.toml

Patrick Massot (Feb 19 2020 at 21:49):

but we can still write those instructions

Mario Carneiro (Feb 19 2020 at 21:50):

What if I just want the latest?

Mario Carneiro (Feb 19 2020 at 21:50):

Also there should still be a way to do the commit matching with a magic git call

Rob Lewis (Feb 19 2020 at 21:50):

What would be great: someone could write a script that takes in a URL, pointing to a zip of the build archive, and unpacks the oleans into the right place.

Patrick Massot (Feb 19 2020 at 21:51):

In case you want to work on an existing project (like the tutorial one) you don't want the latest.

Rob Lewis (Feb 19 2020 at 21:51):

Then you could manually point the script at the URL from Actions.

Rob Lewis (Feb 19 2020 at 21:51):

(Which we can't get automatically without authentication hassle.)

Rob Lewis (Feb 19 2020 at 21:52):

This would be reusable once we're hosting them ourselves.

Patrick Massot (Feb 19 2020 at 21:52):

Sorry Rob, I don't understand what you are suggesting (it's getting late...).

Rob Lewis (Feb 19 2020 at 21:53):

I'm guessing most of the logic is in update-mathlib and/or cache-olean already, just needs to be repackaged.

Rob Lewis (Feb 19 2020 at 21:54):

Actions publishes artifacts from every build: https://github.com/leanprover-community/mathlib/suites/467998748/artifacts/2016943

Mario Carneiro (Feb 19 2020 at 21:54):

If we ignore commit matching, there is still some work to be done taking a zip of oleans and putting them in the right place and touching them. That should be a script on its own

Rob Lewis (Feb 19 2020 at 21:54):

The script should get that archive given the URL, extract the oleans, and put them in the right place.

Mario Carneiro (Feb 19 2020 at 21:54):

The existing tools could be broken up into smaller pieces so that they can fail independently

Patrick Massot (Feb 19 2020 at 21:56):

This is trivial to do.

Mario Carneiro (Feb 19 2020 at 21:56):

great

Mario Carneiro (Feb 19 2020 at 21:57):

mediating this process is very useful for beginners too

Patrick Massot (Feb 19 2020 at 21:57):

Currently I'm fighting several other fights in parallel, but anyone can have a look at https://gist.github.com/PatrickMassot/567833153f106379b87a20e9d3a712ef to see how such things work.

Rob Lewis (Feb 19 2020 at 22:07):

#2018


Last updated: Dec 20 2023 at 11:08 UTC