Process for PRs depending on Lean PRs

Stream: batteries

[François G. Dorais]

I'm working on following up with my RFC lean4#3198. This involves making a PR to core and a dependent PR to Std (perhaps even another PR for Mathlib). This is actually my first time doing this for a long time.

I tried to keep track of the various features to facilitate this process but I was only passively reading as they were happening. Is there some documentation how to properly use bump/v4.6.0 and nightly-testing branches. Right now I'm following my nose and things are working out but I'm worried I'm doing it wrong and I might have to backtrack and do it all over again.

[Marc Huisinga]

There is documentation here: https://leanprover-community.github.io/contribute/tags_and_branches.html

[François G. Dorais]

That's exactly what I was looking for! Thanks!

[François G. Dorais]

I keep running into small issues. Most are due to my ignorance but some appear to be due to the fact that I'm working from a fork on lean4 and std4 rather than a branch. Pro-tips from git experts would be most welcome!

[Marc Huisinga]

You need to branch off from nightly-with-mathlib, not master.

[Joachim Breitner]

This means that your git log should show your changes, and then as the first commit that isn't yours the one labeled nightly-with-mathlib.

[François G. Dorais]

The issue is that my fork is only set to track the master branch from upstream. It's a serious pain to get other upstream branches.

[Mauricio Collares]

git fetch origin plus referring to the branch as origin/nightly-with-mathlib should work fine. Does it go wrong somehow?

[François G. Dorais]

I'm on a fork, origin is my fork, upstream is where the branch is. I had to go and edit .git/config to track all branches from upstream instead of just master. It took forever to figure out that was the problem!

[Mauricio Collares]

git fetch upstream and referring to the branch as upstream/nightly-with-mathlib is supposed to work out of the box, but glad to hear your issue is solved!

[Mauricio Collares]

At least when I add a new remote it says fetch = +refs/heads/*:refs/remotes/REMOTE_NAME/* in .git/config by default

[Mauricio Collares]

(I'm a fan of additionally having fetch = +refs/pull/*/head:refs/pullreqs/* so I can refer to branches by PR number)

[François G. Dorais]

That was the problem, mine was set to fetch = +refs/heads/master:refs/remotes/upstream/master for unknown reasons.

[Mauricio Collares]

Oh, ouch. The manpage says git remote add -t master <name> <URL> does that, I wonder what porcelain does that by default

[François G. Dorais]

Indeed! I created that fork a long time ago so I don't recall.

[François G. Dorais]

Now that my setup woes are all resolved, everything is on-track. The nightly-testing on Std doesn't work right now but I have a PR ready that builds on the most recent nightly-testing-2024-01-24. I now need write access to the branch lean-pr-testing-3223 but that can wait after nighly-testing is fixed. @Scott Morrison

[Kim Morrison]

Holiday still, will probably fix it on the next 24 hours!