Problems updating, again

Stream: mathlib4

[Sophie Morel]

So, to preface this, the reason for my problems this time is probably that I'm a git noob.

Anyway, I was trying to add some lemmas to mathlib, so I created a local branch, worked on it and PR'ed it (#9130). So far so good. But then somebody added a lemma somewhere else to simplify one of my proofs, which was great ! This lemma was PR #9137 and quickly got merged. I didn't want to keep that lemma in the wrong place in my PR, so I thought that it would be a good idea to update the copy of mathlib in my branch, and I tried to use the new ∀ menu in vscode and clicked "project actions -> update dependency", and, well my files don't build anymore and I get this wonderful error message:

`/home/sophie/.elan/toolchains/leanprover--lean4---v4.4.0-rc1/bin/lake setup-file /home/sophie/Lean4/mathlib4/Mathlib/LinearAlgebra/Multilinear/Basic.lean Init Mathlib.Algebra.Algebra.Basic Mathlib.Algebra.BigOperators.Order Mathlib.Data.Fintype.BigOperators Mathlib.Data.Fintype.Sort Mathlib.Data.List.FinRange Mathlib.LinearAlgebra.Pi` failed:

stderr:
info: [304/410] Building Mathlib.Data.Bool.Basic
error: > LEAN_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Qq/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/proofwidgets/.lake/build/lib:./.lake/packages/Cli/.lake/build/lib:./.lake/build/lib LD_LIBRARY_PATH=./.lake/packages/std/.lake/build/lib:./.lake/packages/Qq/.lake/build/lib:./.lake/packages/aesop/.lake/build/lib:./.lake/packages/proofwidgets/.lake/build/lib:./.lake/packages/Cli/.lake/build/lib:./.lake/build/lib:/home/sophie/.elan/toolchains/leanprover--lean4---v4.4.0-rc1/lib/lean:/home/sophie/.elan/toolchains/leanprover--lean4---v4.4.0-rc1/lib:./.lake/build/lib /home/sophie/.elan/toolchains/leanprover--lean4---v4.4.0-rc1/bin/lean -Dpp.unicode.fun=true -Dpp.proofs.withType=false -DautoImplicit=false -DrelaxedAutoImplicit=false ./././Mathlib/Data/Bool/Basic.lean -R ././. -o ./.lake/build/lib/Mathlib/Data/Bool/Basic.olean -i ./.lake/build/lib/Mathlib/Data/Bool/Basic.ilean -c ./.lake/build/ir/Mathlib/Data/Bool/Basic.c
error: stdout:
./././Mathlib/Data/Bool/Basic.lean:50:30: error: Declaration Bool.true_eq_decide_iff not found.
(add `set_option align.precheck false` to suppress this message)
./././Mathlib/Data/Bool/Basic.lean:51:30: error: Declaration Bool.false_eq_decide_iff not found.
(add `set_option align.precheck false` to suppress this message)
error: external command `/home/sophie/.elan/toolchains/leanprover--lean4---v4.4.0-rc1/bin/lean` exited with code 1

Okay, so I guess you're not supposed to update a mathlib branch the same way as a project using mathlib as a dependency (in retrospect, I guess strictly speaking mathlib is not a dependency here, so I should have expected it); I did test the ∀ menu method on one of my regular projects just after and it worked fine. But then my questions are:
(1) Was there any way for me to get the new lemmas ? (Maybe that's actually a git question. I am not super comfortable with git as soon as I leave the basic git pull/commit/push world.)
(2) Is there a way to recover from this, or should I just scratch the PR and create a new one ?

[Sophie Morel]

Hm, so maybe the correct method was a git fetch followed by a git rebase master. I still don't know how to save my current branch though, unless I try going back 394 commits.

[Eric Wieser]

git rebase master is signing yourself up for a world of hurt

[Eric Wieser]

Especially because what happens next is you get an error saying "upstream branch has diverged", and get tricked into running git merge master which is what you should have run in the first place anyway

[Eric Wieser]

(the correct thing to do after a rebase is a git push --force-with-lease, but rebase is often a bad choice even without any mistakes)

[Sophie Morel]

Well now I'm trying to revert to yesterday's last commit, but there were merges in between so it's complicating my life.

[Eric Wieser]

Presumably the reason that "update dependency" failed you is that you clicked one of the items from this list without checking that it said "mathlib"!

image.png

[Eric Wieser]

I think there's no need to; your git fu made a mess of the history and confused github, but ultimately it seems the files are probably ok

[Eric Wieser]

I played a trick on github to make it come to its senses

[Sophie Morel]

I don't remember seeing a list like that tbh, but that's quite possible...

[Sophie Morel]

Wait, does this mean that I should top flailing to fix the branch ? Because I was still trying.

[Eric Wieser]

Sophie Morel said:

Well now I'm trying to revert to yesterday's last commit, but there were merges in between so it's complicating my life.

The word revert is misleading here; if you make a git mess, git revert will usually only make it worse. reset is the command for "throw away all this git history". You need to be careful about pushing when you do this though, and will need the --force-with-lease flag

[Eric Wieser]

If you do decide to go this route, it looks like things start to go wrong after 5bf624186169319f9139df41e4b7803a20dee04a; so I suggest you run

git reset --hard 5bf624186169319f9139df41e4b7803a20dee04a
git merge origin/master
git push --force-with-lease

THIS WILL THROW AWAY ANY LOCAL CHANGES, MAKE SURE YOU ARE OK WITH THIS

[Eric Wieser]

(But leaving things as is and cleaning up the small issues is a reasonable option too)

[Sophie Morel]

I don't know how to clean up. Like, I don't know what to do, at all, at this point.

[Sophie Morel]

And I'm okay scratching local changes, because I saved the relevant file somewhere else.

[Sophie Morel]

Yes, the first "bad" commit is 5bf624186169319f9139df41e4b7803a20dee04a

[Sophie Morel]

(Also, yes, I messed up some merges. I stupidly attempted to do them with vscode, and it turns out that it would have been easier to use the command line, because at least I had some experience with that...)

[Sophie Morel]

Beware "intuitive" tools, I guess.

[Eric Wieser]

I think my zulip was showing your messages with a long delay, sorry for the confusing message interleaving

[Sophie Morel]

Okay, I seem to have problems writing in my own branch. :face_palm:

[Sophie Morel]

bolzano ~/Lean4/mathlib4 $ git push --force-with-lease
To github.com:leanprover-community/mathlib.git
 ! [rejected]            MultilinearMapContDiff -> MultilinearMapContDiff (stale info)
error: failed to push some refs to 'github.com:leanprover-community/mathlib.git'

[Eric Wieser]

This is the safety feature of force-with-lease

[Eric Wieser]

It is telling you "something had been pushed to your remote that you don't know about, so I'm going to refuse to throw it away"

[Eric Wieser]

This could be for instance another contributor making changes

[Sophie Morel]

I don't see any activity on github though ?

[Eric Wieser]

Do you have multiple copies of the repo?

[Sophie Morel]

I don't think so.

[Sophie Morel]

Sorry if I'm slow, it's half past midnight here and I've had a very long day.

[Eric Wieser]

You can run git fetch to ask git to "see" the changes

[Eric Wieser]

It will print out something short about the new commits it found

[Eric Wieser]

Once you've done that git trusts that you know what you're doing and will let you overwrite whatever they were

[Sophie Morel]

I'm trying to run it, but it's not printing anything right now.

[Eric Wieser]

Maybe git fetch origin

[Sophie Morel]

Same.

[Eric Wieser]

You can disable the safety feature by using --force without the with-lease bit

[Sophie Morel]

bolzano ~/Lean4/mathlib4 $ git push --force
Enumerating objects: 101259, done.
Counting objects: 100% (101259/101259), done.
Delta compression using up to 8 threads
Compressing objects: 100% (21435/21435), done.
Writing objects:   4% (4051/101259)

[Sophie Morel]

I'm copying this because it seems to have stayed stuck on this 4%.

[Eric Wieser]

What exactly is it pushing?

[Eric Wieser]

I would cancel that

[Sophie Morel]

Ah no, it's 7% now.

[Sophie Morel]

Ok, cancelled.

[Eric Wieser]

It sounds like it might be trying to force push every single branch

[Eric Wieser]

You should specify just your branch

[Sophie Morel]

Strange. Also, I should not have the right to push to other branches.

[Eric Wieser]

Otherwise you would revert everyone else's work by a day or so!

[Eric Wieser]

Sophie Morel said:

Strange. Also, I should not have the right to push to other branches.

That's usually true on GitHub, but it's not true for mathlib :grimacing:

[Sophie Morel]

Yes, it's a very good thing that I can't do that, as we are establishing.

[Sophie Morel]

Eric Wieser said:

Sophie Morel said:

Strange. Also, I should not have the right to push to other branches.

That's usually true on GitHub, but it's not true for mathlib :grimacing:

Wait wait wait, I can destroy other people's work ? Oh no, I will never dare push anything to mathlib again.

[Eric Wieser]

Yes, unfortunately you can. The only thing you can't destroy is stuff that's already merged

[Sophie Morel]

Aaaaaaaargh...

[Sophie Morel]

Okay, so just to be safe, it's git push --force origin BranchName ?

[Eric Wieser]

Yes, that should destroy only BranchName

[Sophie Morel]

Hm.

bolzano ~/Lean4/mathlib4 $ git push --force origin MultilinearMapContDiff
Enumerating objects: 101259, done.
Counting objects: 100% (101259/101259), done.
Delta compression using up to 8 threads
Compressing objects: 100% (21435/21435), done.
Writing objects:   4% (4051/101259)

[Sophie Morel]

Doesn't look very different from the last time.

[Eric Wieser]

Maybe last time was safe after all

[Eric Wieser]

This one certainly is

[Sophie Morel]

Eric Wieser said:

This one certainly is

Oh thank god.

[Eric Wieser]

Sophie Morel said:

Eric Wieser said:

Sophie Morel said:

Strange. Also, I should not have the right to push to other branches.

That's usually true on GitHub, but it's not true for mathlib :grimacing:

Wait wait wait, I can destroy other people's work ? Oh no, I will never dare push anything to mathlib again.

Only --force has this power, when you're not using it there is no need to worry :)

[Sophie Morel]

I think I'm only to do git push origin from now on...

[Sophie Morel]

Well this is slow.

[Eric Wieser]

I dread to think what you're pushing... I guess we'll find out eventually!

[Sophie Morel]

(At least it's giving me time to check that I did save my local changes, and yes, I did. Whew.)

[Eric Wieser]

(maybe a .lake or build folder got committed somehow?)

[Sophie Morel]

I have no idea. Maybe I'm pushing my entire collection of math article/book pdfs that got into that repository somehow ? At this point I'll believe anything.

[Thomas Murrills]

Well, we do need more documentation…

[Sophie Morel]

At least this is a work computer, so no embarrassing files.

[Eric Wieser]

You can run git diff $(git merge-base origin/master HEAD) --shortstat to find out

[Eric Wieser]

(it should be safe to run in parallel in another terminal)

[Sophie Morel]

1 file changed, 252 insertions(+)
Well that's a big file.

[Thomas Murrills]

Eric Wieser said:

Maybe last time was safe after all

I was going to say, I’ve never experienced git push --force pushing to anything but the current checked-out branch, and I’ve rebased with abandon as a git noob :sweat_smile: That would be really scary if it wasn’t safe in that way. Could it ever do that without additional flags?

[Sophie Morel]

(deleted)

[Kyle Miller]

Sophie Morel said:

Wait wait wait, I can destroy other people's work ? Oh no, I will never dare push anything to mathlib again.

If they already have a PR for their branch, then at least GitHub keeps track of the old commit hash on the PR page whenever you force push, so it's not really destroyed.

image.png

Plus, people can always do git reflog locally to see the history of their own copy of their repository and figure this out.

[Eric Wieser]

Thomas Murrills said:

That would be really scary if it wasn’t safe in that way. Could it ever do that without additional flags?

I think it might do that if your git is configured with push.default matching

[Sophie Morel]

28%, and it's been 12 minutes.

[Sophie Morel]

I'm going to go brush my teeth then, I think I have time. :grinning_face_with_smiling_eyes:

[Sophie Morel]

Eric Wieser said:

Thomas Murrills said:

That would be really scary if it wasn’t safe in that way. Could it ever do that without additional flags?

I think it might do that if your git is configured with push.default matching

Okay, so I ran git config --global push.default simple just in case.

[Sophie Morel]

(I thought about git config --global push.default nothing, but okay, let's not be too negative...)

[Thomas Murrills]

Just curious, what’s your git version? (irrelevant in this case)

[Thomas Murrills]

Seems matching used to be the default pre 2.0 and now simple is the default. (I have no idea how long ago 2.0 was.)

[Thomas Murrills]

But if you specify a branch in this way, it would still only push to that branch even with matching, right?

[Sophie Morel]

Also, my version is 2.34.1 anyway.

[Sophie Morel]

Well, my push is only at 53% and it's 1:19 am, I'm off to bed and we'll see what happens tomorrow. Thanks for all the help, @Eric Wieser !

[Yaël Dillies]

I hope your computer hasn't melted overnight!

[Sophie Morel]

My computer appears to think that I have created a new branch with the same name. I'm confused. But it's not melted at least.

[Sophie Morel]

I don't get it. I pulled again and the local files don't appear to have changed (i.e. yesterday evening's changes are still here).

[Sophie Morel]

Now will it build, that's the question.

[Sophie Morel]

It does. I am extremely confused. (But relieved too !)

[Marc Huisinga]

Okay, so I guess you're not supposed to update a mathlib branch the same way as a project using mathlib as a dependency (in retrospect, I guess strictly speaking mathlib is not a dependency here, so I should have expected it); I did test the ∀ menu method on one of my regular projects just after and it worked fine.

This is good feedback and suggests that there should be an additional warning message describing the consequences before even getting to see a list of options.

[Sophie Morel]

New twist: apparently it did create a new branch (with the same name ?), because I am not pushing into the PRed branch anymore. But on the bright side, all my files are compiling locally.

[Eric Wieser]

Where did it push to?

[Sophie Morel]

Okay no, I checked the mathlib branches, and there is still only one with that name.

[Sophie Morel]

Eric Wieser said:

Where did it push to?

That is what I am trying to determine.

[Eric Wieser]

(or maybe what I mean is; what was the output of last night's git push?)

[Sophie Morel]

bolzano ~/Lean4/mathlib4 $ git push --force origin MultilinearMapContDiff
Enumerating objects: 101259, done.
Counting objects: 100% (101259/101259), done.
Delta compression using up to 8 threads
Compressing objects: 100% (21435/21435), done.
Writing objects: 100% (101259/101259), 47.38 MiB | 15.00 KiB/s, done.
Total 101259 (delta 78882), reused 100298 (delta 78255), pack-reused 0
remote: Resolving deltas: 100% (78882/78882), done.
remote:
remote: Create a pull request for 'MultilinearMapContDiff' on GitHub by visiting:
remote:      https://github.com/leanprover-community/mathlib/pull/new/MultilinearMapContDiff
remote:
To github.com:leanprover-community/mathlib.git
 * [new branch]          MultilinearMapContDiff -> MultilinearMapContDiff

[Sebastian Ullrich]

You are likely pushing to your own fork (git remote -v)

[Sophie Morel]

bolzano ~/Lean4/mathlib4 $ git remote -v
origin  git@github.com:leanprover-community/mathlib.git (fetch)
origin  git@github.com:leanprover-community/mathlib.git (push)

[Sebastian Ullrich]

Oh my bad, it's the original repo. But it's mathlib 3!

[Eric Wieser]

That would explain why pushing took so long!

[Sophie Morel]

Oh no, I must have made a mistake when I was configuring git to work with ssh last night at 1 am...

[Eric Wieser]

You pushed the entire mathlib4 master to a mathlib3 branch

[Sophie Morel]

Okay, this I should be able to fix this...

[Yaël Dillies]

That explains why it took so long!

[Sophie Morel]

Okay, I will try to fix this when I stop laughing.

[Eric Wieser]

We should probably delete the branch on mathlib3 to save anyone having to wait for it to download mathlib4 when they git fetch, but that's very non urgent

[Sophie Morel]

I've now pushed to my mathlib4 branch, and I can see on github that it's been updated.

[Sophie Morel]

And the CI linter is complaining. I never thought I would be so happy to see that.

[Eric Wieser]

It looks like you might have clobbered some of your previous work

[Eric Wieser]

You should check there's nothing on that page you meant to keep (you can always just copy paste it from there rather than trying to use git to recover if)

[Eric Wieser]

Maybe it's just a reordering

[Sophie Morel]

Thanks ! It's fine, I was obsessively making local saves of the files last night, so nothing would be lost anyway. But I think it's just moving code so it comes after other code that it depends on.

[Sophie Morel]

Sophie Morel said:

And the CI linter is complaining. I never thought I would be so happy to see that.

Yes, I had a line that was 101 characters, the horror. :scream:

[Sophie Morel]

So if I go to the mathlib repo on github and click the little trash can icon next to my new branch's name, does this do what I think it should and delete the thing ?

[Eric Wieser]

Yes, but make sure it's mathlib 3

[Sophie Morel]

It is ! The branch doesn't have a PR on it, which is good.