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

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


#### 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!

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.

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: Jun 20 2021 at 00:35 UTC