Orange bar hell even after after cache get

Stream: mathlib4

[Bolton Bailey]

I have run lake exe cache get! on #7278 after merging master, but I am still in orange bar hell. Info tells me it is building various things, like

[548/955] Building Mathlib.Tactic.NormNum.Core
and later
info: [585/955] Building Mathlib.Data.Int.Order.Basic
and later
info: [677/955] Building Mathlib.Order.GaloisConnection

Why are things building from Mathlib when I have supposedly downloaded the cache?

[Kevin Buzzard]

Because the system is constantly a bit broken. Try lake clean and then lake exe cache get again. And good luck.

[Kevin Buzzard]

If that doesn't work, try rm -rf build and rm -rf lake-packages and then lake clean and lake exe cache get. And if that doesn't work then it's broken more than usual.

[Kevin Buzzard]

And remember to never ever ever type lake update with no additional arguments, even if lake helpfully suggests doing this.

[Bolton Bailey]

Unfortunately the first one didn't work. I'll move on to the second one.

[Bolton Bailey]

Actually wait, maybe it did work.

[Bolton Bailey]

Wow that's weird, I pressed the pause button in the infoview and then the orange bar started going away.

[Bolton Bailey]

I wasn't aware literally anything could happen with the pause button pressed.

[Sky Wilshaw]

The pause button stops the infoview from changing, it doesn't stop lean from doing things.

[Yaël Dillies]

Kevin Buzzard said:

And remember to never ever ever type lake update with no additional arguments, even if lake helpfully suggests doing this.

Wait what are you supposed to do then?

[Kevin Buzzard]

Well I was developing NNG yesterday and lake said "ooh GameServer needs updating, please type lake update". If I had typed this then it would have broken everything, because it would also have e.g. updated mathlib. But I typed lake update GameServer and it did what lake was trying to tell me to do.

[Kevin Buzzard]

@Mac Malone lucky I'm wise to this, eh?