Zombie changes

Stream: general

[Yaël Dillies]

I am cleaning up files concerning encodable and denumerable and took the opportunity to change decode2 to decode₂. That makes me change quite a lot of files and one of them (namely src/topology/algebra/infinite_sum) decided to revert previous changes! How did that happen? Here's the PR: #7704. The changes I didn't make are all reversions of [pseudo_metric_space α] to [metric_space α].

[Eric Wieser]

leanproject get-cache wipes local changes - could that be it?

[Yaël Dillies]

Urf, that might be. I always use get-cache after a commit finished compiling to get the oleans file and avoid Lean burning my processor.

[Eric Wieser]

As long as you commit the files first you're safe

[Eric Wieser]

But I don't think that's what you're describing anyway

[Eric Wieser]

You're referring to this commit, right?

https://github.com/leanprover-community/mathlib/pull/7704/commits/124d9a033d29ac9ac2434e73ab48b2c9a93cd55f

[Yaël Dillies]

Aaah, I think I know what happened.

[Eric Wieser]

What's your workflow for getting the cache? Is it git checkout foo; leanproject get-cache; git checkout bar; or leanproject get-cache --rev foo?

[Eric Wieser]

Because the first approach easily leads to this type of trap

[Yaël Dillies]

When I commited the commit you just referred to, I switched to another, not up to date, branch before the little rotating icon stopped rotating. I suspect VScode picked the old version of the end of the file as it was changing branches.

[Yaël Dillies]

I use leanproject get-cache --rev origin/foo.