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

Stream: new members

[Laurent Bartholdi]

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]

Did you get update-mathlib working?

[Laurent Bartholdi]

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

[Patrick Massot]

That explains what you see.

[Patrick Massot]

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

[Laurent Bartholdi]

Yes, I did

[Patrick Massot]

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

[Patrick Massot]

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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Patrick Massot]

Did that lean command start before update-mathlib?

[Patrick Massot]

Is yes then kill it

[Patrick Massot]

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

[Laurent Bartholdi]

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]

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

[Laurent Bartholdi]

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

[Rob Lewis]

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

[Patrick Massot]

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

[Laurent Bartholdi]

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

[Patrick Massot]

What did you do?

[Patrick Massot]

Did you used Rob's incantation?

[Laurent Bartholdi]

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]

Just to make sure: was leanpkg build quick?

[Laurent Bartholdi]

No, it took 9 minutes

[Laurent Bartholdi]

... with 8 cores heating...

[Patrick Massot]

Then there is something really weird going on.

[Patrick Massot]

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

[Patrick Massot]

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

[Kevin Buzzard]

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]

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]

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]

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]

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

[Patrick Massot]

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]

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

[Mario Carneiro]

We need alternatives for when that call fails

[Kevin Buzzard]

leanpkg build ;-)

[Kevin Buzzard]

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

[Laurent Bartholdi]

I think 4 times.

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

[Rob Lewis]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Patrick Massot]

but we can still write those instructions

[Mario Carneiro]

What if I just want the latest?

[Mario Carneiro]

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

[Rob Lewis]

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]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Patrick Massot]

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

[Rob Lewis]

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

[Rob Lewis]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Patrick Massot]

This is trivial to do.

[Mario Carneiro]

great

[Mario Carneiro]

mediating this process is very useful for beginners too

[Patrick Massot]

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]

#2018