Help needed to open a PR

Stream: new members

[Emilie Uthaiwat]

Hello,

I am currently trying to open a PR. I have followed the instructions on the following web page: https://leanprover-community.github.io/contribute/index.html. My PR !4#7235 indicates that I would like to merge 14 commits but that is not the case (the 14 commits are all old commits which date back to the port and which therefore have no link with the current PR). Could someone please help me get rid of those commits?

[Yaël Dillies]

Do you care about what the list of commits is? When merging, bors will squash them all to a single PR anyway.

[Riccardo Brasca]

If the diff here is good you can ignore the various commits (they will be "squashed", meaning that at the end there will be only one commit in the official version of mathlib)

[Yaël Dillies]

The one reason I would care about the intermediate commits is if they were authored by people who have nothing to do with the PR, because bors looks at the intermediate commits to determine the commit authors. But here all the intermediate PRs are yours, so I just wouldn't bother

[Riccardo Brasca]

So this is fine, but there are merge conflict, meaning that git does not know how to handle some changements in mathlib happened after you cloned it (someone else modified something you also modified). The easiest way is to merge master, something like git fetch && git merge origin/master, and VS code will flag the conflicts.

[Riccardo Brasca]

(You will also need to get a new cache after that)

[Emilie Uthaiwat]

Well noted concerning the commits. Thank you!

[Emilie Uthaiwat]

I used git fetch, git merge, lake exe cache get, lake build. I don't know what is supposed to happen but it seems like nothing changed. I have also got one red squiggle in the file which I am trying to modify (Mathlib.Algebra.Associated). The squiggle is in the proof of prime_pow_succ_dvd_mul because the proof that I have on my local version of mathlib4 is apparently not the same as the one online. How do I update my local version of mathlib4?

[Yaël Dillies]

What does git merge origin/master do? I suspect you merged your local version of master, not the (updated) remote one.

[Yaël Dillies]

Ah actually that may be related to https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Updating.20mathlib.20broke.20my.20cache ?

[Emilie Uthaiwat]

Yaël Dillies said:

What does git merge origin/master do? I suspect you merged your local version of master, not the (updated) remote one.

VS Code says "Already up to date." (please see on the screenshot).

Screenshot-2023-09-18-113429.png

[Damiano Testa]

You seem to be on the master branch of your project, rather than on the branch of Mathlib where you PR is. At least, this is what I think looking at the screenshot.

[Damiano Testa]

So, you probably have on your computer both a copy of Mathlib embedded inside your project as a dependency with its master branch and also a separate copy of Mathlib (not inside any project) with its master branch. (It is completely normal to have multiple copies of Mathlib lying around in different places!)

[Emilie Uthaiwat]

Indeed, I am on the master branch on my project.

[Damiano Testa]

Ok, so you should find the master branch of Mathlib (in a different folder) and from there git switch Associated; git fetch; git merge origin/master and now you should have locally updated your branch of Mathlib to the current master.

[Damiano Testa]

If you do not have a cache, I would have recommended

git pull  # on `master`
lake exe cache get!  # wait for it to finish, possibly a few seconds
git switch Associated
git merge origin/master  # now the cache is ok, up to the import-ideal of what you modified

however, currently I am not able to get the remote cache working for me.

[Emilie Uthaiwat]

I need to go to class soon. I am going to try all of that later today and will get back to you. Thank you!

[Emilie Uthaiwat]

The problem is solved! Thank you again!