Zulip Chat Archive

Stream: general

Topic: lean orange bars wont go away


Chris Birkbeck (Sep 09 2021 at 09:34):

My lean seems to be stuck in orange bar hell, but I can't seem to fix it. I've tried using leanproject get-cache which downloaded something, but after restarting lean the orange bars still wont go away no matter how long I wait. I'm not sure if this has anything to do with it, but looked at the lean --version on these branches. It seems all the branches using version 3.32.1 are the ones that are broken. I have one branch using version 3.31.0 and that seems to be working fine. What can I do?

Huỳnh Trần Khanh (Sep 09 2021 at 09:42):

How about running leanproject get-mathlib-cache?

Oliver Nash (Sep 09 2021 at 09:42):

Are you working on Mathlib itself or a project dependent upon Mathlib?

Chris Birkbeck (Sep 09 2021 at 09:44):

Huỳnh Trần Khanh said:

How about running leanproject get-mathlib-cache?

I tried this and it just says Looking for local mathlib oleans followed by Found local mathlib oleans.

Kevin Buzzard (Sep 09 2021 at 09:44):

Are you working on a mathlib itself or a project dependent upon mathlib?

Kevin Buzzard (Sep 09 2021 at 09:44):

Better question: why don't you hop onto the discord and I'll see if I can sort you out?

Johan Commelin (Sep 09 2021 at 09:45):

@Chris Birkbeck how many files do you have open in VScode?

Oliver Nash (Sep 09 2021 at 09:45):

Multiple versions of Lean in play sounds like a good lead. If possible I recommend you merge the latest master into all your branches so that you're using 3.32.1 throughout.

Chris Birkbeck (Sep 09 2021 at 09:45):

Kevin Buzzard said:

Better question: why don't you hop onto the discord and I'll see if I can sort you out?

sure

Chris Birkbeck (Sep 09 2021 at 09:45):

Johan Commelin said:

Chris Birkbeck how many files do you have open in VScode?

only 1

Eric Wieser (Sep 09 2021 at 09:45):

Oliver Nash said:

Are you working on Mathlib itself or a project dependent upon Mathlib?

Kevin Buzzard said:

Are you working on a mathlib itself or a project dependent upon mathlib?

Are you working on a mathlib itself or a project dependent upon mathlib?

Yaël Dillies (Sep 09 2021 at 09:48):

Same happened to me yesterday. Had to write docstrings all day long because I was in hell :disappointed:

Kevin Buzzard (Sep 09 2021 at 10:09):

That's a good thing!

Chris Birkbeck (Sep 09 2021 at 10:09):

It's all sorted now thanks to Kevin. I may have accidentally modified a core lean file and broken things.

Kevin Buzzard (Sep 09 2021 at 10:09):

So the problem seems to be solved -- Chris deleted his copy of lean-3.32 in the .elan directory and redownloaded it and it's now working again

Johan Commelin (Sep 09 2021 at 10:12):

@Chris Birkbeck If you update elan this should no longer be possible. It makes the core files read-only.

Chris Birkbeck (Sep 09 2021 at 10:14):

Ah how do I update elan?

Johan Commelin (Sep 09 2021 at 10:14):

elan --help suggests elan update

Chris Birkbeck (Sep 09 2021 at 10:15):

Great, thank you!

Chris Birkbeck (Sep 09 2021 at 10:38):

Kevin Buzzard said:

So the problem seems to be solved -- Chris deleted his copy of lean-3.32 in the .elan directory and redownloaded it and it's now working again

In case anyone wants to try this in the future, the fix was specifically by deleting the ...lean--3.32.1 file in the toolchains folder AND similarly named one in the update-hashes folder (both of which are inside the .elan folder).

Kalle Kytölä (Oct 24 2021 at 11:35):

Hi helpful Zulipers!

I thought I had learned to deal with the "orange bar hell", but now I've done something that seems to have totally destroyed my mathlib.

The way I usually get out of this is checking out my master branch, and doing leanproject upgrade-mathlib and/or leanproject update-mathlib-cache. Both of these give a similar and at least slightly strange output, which does not tell me what the problem is. E.g. leanproject upgrade-mathlib gives:

Pulling...
Looking for local mathlib oleans
Found local mathlib oleans

Aborted!

(The last Aborted! is what I would not want to see, I guess.)

And when I open files with VS Code, I'm in the orange bar hell.

Any hints on how to troubleshoot?

Eric Rodriguez (Oct 24 2021 at 11:41):

Try delete ~/.mathlib?

Kalle Kytölä (Oct 24 2021 at 11:42):

Oh, that seems radical. And after that I should presumably reinstall somehow?

Rémy Degenne (Oct 24 2021 at 11:44):

It's the folder where all the oleans are stored. After deleting that, leanproject will not find local oleans anymore and will download the remote ones.

Kalle Kytölä (Oct 24 2021 at 11:47):

Brilliant, everything is back to normal after deleting the dir ~/.mathlib and running leanproject upgrade-mathlib!

Thank you very much @Eric Rodriguez and @Rémy Degenne for rescuing one local mathlib :relieved:.

Eric Rodriguez (Oct 24 2021 at 11:48):

If you wan a save some keystrokes in future, leanproject up does the same thing :) (as upgrade-mathlib, that is, not deleting the folder!)

Patrick Stevens (Oct 24 2021 at 13:44):

(Likely cause, by the way, is that the local mathlib oleans package was corrupted so couldn't be unpacked into your working directory. You could have also fixed the problem by deleting just the one tar file in ~/.mathlib that leanproject up was trying to unpack; it's just that an easier instruction is to delete all of them.)

Patrick Massot (Oct 24 2021 at 13:54):

leanproject also has a --force-download option that will download a fresh archive even if something is already there.

Moritz Doll (Aug 22 2022 at 17:36):

I seems that I can't rid of my orange bar of hell. It appears on two different branches of mathlib. updating lean and redownloading the caches had no effect. Does anyone have any ideas on what to do?

Eric Rodriguez (Aug 22 2022 at 17:41):

What happens when you lean --makethe file you want to open?

Moritz Doll (Aug 22 2022 at 17:53):

it just starts compiling everything. Pushing to github and then downloading the new oleans solves the problems though

Kevin Buzzard (Aug 23 2022 at 09:27):

When you say "everything" do you mean "order/field/defs" or whatever it is (the file with no olean) or "logic/basic"?

Moritz Doll (Aug 23 2022 at 16:22):

it starts with something like /src/data/bool/basic.lean


Last updated: Dec 20 2023 at 11:08 UTC