Zulip Chat Archive

Stream: new members

Topic: update project

Alex Zhang (Jul 12 2021 at 20:28):

I am trying to update my local mathlib. But I saw this when updating:
image.png
Does this mean the update is failed?

Mario Carneiro (Jul 12 2021 at 20:32):

did you try again? Sometimes github has transient failures

Mario Carneiro (Jul 12 2021 at 20:33):

that error looks like an abort due to user input, so trying again might help if you accidentally hit ctrl-c or something

Alex Zhang (Jul 12 2021 at 20:35):

image.png

Alex Zhang (Jul 12 2021 at 20:36):

still "aborted" :cry:

Bryan Gin-ge Chen (Jul 12 2021 at 20:36):

Are you able to connect to github.com normally?

Bryan Gin-ge Chen (Jul 12 2021 at 20:37):

Oh, wait. That shouldn't have anything to do with what you're seeing, since it says "found local mathlib oleans".

Bryan Gin-ge Chen (Jul 12 2021 at 20:38):

Could you try leanproject --debug up ?

Alex Zhang (Jul 12 2021 at 20:42):

Hi, Bryan. I have tried now, but still the same error message.

Alex Zhang (Jul 12 2021 at 20:42):

image.png

Alex Zhang (Jul 12 2021 at 20:43):

@Bryan Gin-ge Chen

Alex Zhang (Jul 12 2021 at 20:44):

I can access github.com normally via chrome.

Kevin Buzzard (Jul 12 2021 at 20:44):

Whenever I get that message it's because I interrupted an earlier download and now have a corrupted abababab171716161.tar.xz olean archive file

Kevin Buzzard (Jul 12 2021 at 20:46):

So try leanproject get-c so you can see the name and location of the file to delete, and then delete it and try the same command again.

Bryan Gin-ge Chen (Jul 12 2021 at 20:46):

A more drastic approach is just deleting the contents of ~/.mathlib/.

Alex Zhang (Jul 12 2021 at 20:47):

image.png

Alex Zhang (Jul 12 2021 at 20:47):

leanproject get-c reports the same error message. :cry:

Alex Zhang (Jul 12 2021 at 20:49):

I don't have a mathlib folder as I am working in the downloaded mathlib, perhaps delete all the contents in /src?

Bryan Gin-ge Chen (Jul 12 2021 at 20:51):

Sorry, what I mean is that leanproject should create a folder called .mathlib in your home directory (referred to as ~). If you delete that directory, maybe leanproject will retry downloading the corrupted file.

Kevin Buzzard (Jul 12 2021 at 20:51):

(deleted)

Rémy Degenne (Jul 12 2021 at 20:52):

For me it's in Users/my_username/ (on windows).

Bryan Gin-ge Chen (Jul 12 2021 at 20:52):

Actually, maybe leanproject -f up will work? The -f option is supposed to force a download.

Kevin Buzzard (Jul 12 2021 at 20:52):

That's what ~ probably expands to?

Kevin Buzzard (Jul 12 2021 at 20:53):

Did you try my suggestion? It's what I always do to fix this -- oh, I see you did

Rémy Degenne (Jul 12 2021 at 20:53):

I just got myself into the same situation as you, with "aborted" errors. Deleting the folder worked to get another download starting... but it did not succeed

Alex Zhang (Jul 12 2021 at 20:53):

Yes, Kevin. I tried. The error message is in my screenshot.

Rémy Degenne (Jul 12 2021 at 20:54):

I got this

 18%|#8        | 8.39M/46.2M [00:20<00:14, 2.54MiB/s]("Connection broken: ConnectionResetError(10054, 'An existing connection was forcibly closed by the remote host', None, 10054, None)", ConnectionResetError(10054, 'An existing connection was forcibly closed by the remote host', None, 10054, None))

Alex Zhang (Jul 12 2021 at 20:54):

Yes!!! I got exactly the error message before.

Kevin Buzzard (Jul 12 2021 at 20:54):

Why don't you find your secret treasure trove of old mathlib oleans Alex?

Kevin Buzzard (Jul 12 2021 at 20:55):

It's in ~/.mathlib which will expand to something which depends on your OS. What OS are you using BTW?

Alex Zhang (Jul 12 2021 at 20:56):

I am using win10

Kevin Buzzard (Jul 12 2021 at 20:57):

And you can use git log in your mathlib repo to find the name of the commit you're on

Kevin Buzzard (Jul 12 2021 at 20:57):

Bryan's -f suggestion might be the easiest fix but this way you'll learn more about what's going on behind the scenes

Kevin Buzzard (Jul 12 2021 at 20:58):

So try looking in Users/your_username/.mathlib

Bryan Gin-ge Chen (Jul 12 2021 at 20:58):

There might be something wrong with the olean storage at the moment, as I just tried leanproject up and I got an error as well.

Bryan Gin-ge Chen (Jul 12 2021 at 20:58):

Trying to download https://oleanstorage.azureedge.net/mathlib/a9cb722ce675578c376c1a0e56c0353c02ae9c82.tar.xz to /Users/chb/.mathlib/a9cb722ce675578c376c1a0e56c0353c02ae9c82.tar.xz
Failed to fetch mathlib oleans

Bryan Gin-ge Chen (Jul 12 2021 at 20:58):

cc: @Rob Lewis

Alex Zhang (Jul 12 2021 at 20:59):

Lean and mathlib are forcing me to be a computer scientist.....

Bryan Gin-ge Chen (Jul 12 2021 at 20:59):

Hmm, there's a message at https://status.azure.com/en-us/status which indicates that there's something going on with Azure in general?

Kevin Buzzard (Jul 12 2021 at 21:00):

So Alex the problem right now is that something is broken and one fix is to just wait

Alex Zhang (Jul 12 2021 at 21:01):

It seems that going to sleep is currently the best solution.

Kevin Buzzard (Jul 12 2021 at 21:01):

You can compile your own mathlib while you sleep! Try lean --make src in the root of your mathlib repo

Kevin Buzzard (Jul 12 2021 at 21:02):

When you wake up it should be done

Kevin Buzzard (Jul 12 2021 at 21:02):

Unless your computer caught fire

Alex Zhang (Jul 12 2021 at 21:05):

image.png
I am in the UK however

Rémy Degenne (Jul 12 2021 at 21:05):

It crashes my laptop with 100% success :) (But it works and is very useful on my better home computer)

Kevin Buzzard (Jul 12 2021 at 21:10):

Try lean -M6000 --make src if compiling lean crashes your laptop

Alex Zhang (Jul 13 2021 at 06:52):

What is the function of this command lean -M6000 --make src? (I perhaps should be cautious about trying it on my laptop)

Kevin Buzzard (Jul 13 2021 at 06:58):

Just put lean --help or whatever to see what all the command line options do

Alex Zhang (Jul 13 2021 at 07:27):

What are mathlib oleans? :thinking:

Ruben Van de Velde (Jul 13 2021 at 07:34):

Compiled versions of the lean files, so you don't have to compile them all locally

Alex Zhang (Jul 13 2021 at 07:45):

Kevin Buzzard said:

Unless your computer caught fire

OK. Now I have understood why lean --make src will set my laptop on fire.

Anne Baanen (Jul 13 2021 at 09:15):

This error has been annoying me as well, so I created a PR mathlib-tools#104 so that leanproject does not keep around the broken files when a download gets interrupted.

Last updated: Dec 20 2023 at 11:08 UTC