lean orange bars wont go away

Stream: general

[Chris Birkbeck]

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]

How about running leanproject get-mathlib-cache?

[Oliver Nash]

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

[Chris Birkbeck]

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]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Oliver Nash]

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]

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]

Johan Commelin said:

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

only 1

[Eric Wieser]

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]

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

[Kevin Buzzard]

That's a good thing!

[Chris Birkbeck]

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

[Kevin Buzzard]

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]

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

[Chris Birkbeck]

Ah how do I update elan?

[Johan Commelin]

elan --help suggests elan update

[Chris Birkbeck]

Great, thank you!

[Chris Birkbeck]

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ä]

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]

Try delete ~/.mathlib?

[Kalle Kytölä]

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

[Rémy Degenne]

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ä]

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]

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]

(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]

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

[Moritz Doll]

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]

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

[Moritz Doll]

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

[Kevin Buzzard]

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

[Moritz Doll]

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