Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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

view this post on Zulip Patrick Massot (Feb 19 2020 at 21:00):

Did you get update-mathlib working?

view this post on Zulip Laurent Bartholdi (Feb 19 2020 at 21:01):

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

view this post on Zulip Patrick Massot (Feb 19 2020 at 21:02):

That explains what you see.

view this post on Zulip Patrick Massot (Feb 19 2020 at 21:02):

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

view this post on Zulip Laurent Bartholdi (Feb 19 2020 at 21:03):

Yes, I did

view this post on Zulip Patrick Massot (Feb 19 2020 at 21:04):

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

view this post on Zulip 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).

view this post on Zulip Patrick Massot (Feb 19 2020 at 21:05):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Feb 19 2020 at 21:07):

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

view this post on Zulip Patrick Massot (Feb 19 2020 at 21:08):

Did that lean command start before update-mathlib?

view this post on Zulip Patrick Massot (Feb 19 2020 at 21:08):

Is yes then kill it

view this post on Zulip Patrick Massot (Feb 19 2020 at 21:08):

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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Feb 19 2020 at 21:11):

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

view this post on Zulip Laurent Bartholdi (Feb 19 2020 at 21:12):

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

view this post on Zulip Rob Lewis (Feb 19 2020 at 21:12):

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

view this post on Zulip Patrick Massot (Feb 19 2020 at 21:12):

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

view this post on Zulip Laurent Bartholdi (Feb 19 2020 at 21:21):

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

view this post on Zulip Patrick Massot (Feb 19 2020 at 21:22):

What did you do?

view this post on Zulip Patrick Massot (Feb 19 2020 at 21:22):

Did you used Rob's incantation?

view this post on Zulip 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"?

view this post on Zulip Patrick Massot (Feb 19 2020 at 21:23):

Just to make sure: was leanpkg build quick?

view this post on Zulip Laurent Bartholdi (Feb 19 2020 at 21:24):

No, it took 9 minutes

view this post on Zulip Laurent Bartholdi (Feb 19 2020 at 21:25):

... with 8 cores heating...

view this post on Zulip Patrick Massot (Feb 19 2020 at 21:25):

Then there is something really weird going on.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Feb 19 2020 at 21:26):

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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 19 2020 at 21:47):

We need alternatives for when that call fails

view this post on Zulip Kevin Buzzard (Feb 19 2020 at 21:47):

leanpkg build ;-)

view this post on Zulip 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

view this post on Zulip 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 :)

view this post on Zulip Rob Lewis (Feb 19 2020 at 21:48):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Feb 19 2020 at 21:49):

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

view this post on Zulip Patrick Massot (Feb 19 2020 at 21:49):

but we can still write those instructions

view this post on Zulip Mario Carneiro (Feb 19 2020 at 21:50):

What if I just want the latest?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Feb 19 2020 at 21:51):

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

view this post on Zulip Rob Lewis (Feb 19 2020 at 21:51):

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

view this post on Zulip Rob Lewis (Feb 19 2020 at 21:52):

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

view this post on Zulip Patrick Massot (Feb 19 2020 at 21:52):

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

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Feb 19 2020 at 21:54):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Feb 19 2020 at 21:54):

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

view this post on Zulip Patrick Massot (Feb 19 2020 at 21:56):

This is trivial to do.

view this post on Zulip Mario Carneiro (Feb 19 2020 at 21:56):

great

view this post on Zulip Mario Carneiro (Feb 19 2020 at 21:57):

mediating this process is very useful for beginners too

view this post on Zulip 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.

view this post on Zulip Rob Lewis (Feb 19 2020 at 22:07):

#2018


Last updated: Jun 20 2021 at 00:35 UTC