how to restart port process?

Stream: mathlib4

[Kevin Buzzard]

In the process of porting CategoryTheory.Sites.DenseSubsite in !4#3939 (which is still marked WIP even though it compiles, for reasons which are about to become clear) I found myself wanting to do a very minor refactor of the file, so I made this refactor in mathlib3 in #19002, now merged. As a result (a) the mathlib4 diff between the "automated fixes" commit and the final commit is confusing in a couple of places and (b) commit hashes will be different and merging !4#3939 will cause some confusion with the backporting algorithm etc.

All this could be avoided if I simply make a local copy of the final ported file and then simply start the port process again (once mathlib3port has picked up on #19002 -- when does this happen?) and copy my fixes to the Lean code back but leave the first few lines of the file alone. But I am a bit unclear about how this will work because the branch port/CategoryTheory.Sites.DenseSubsite already exists on github. Any advice?

[Joël Riou]

./scripts/start_port.sh will work: it will tell you that the branch already exists, and give you the exact syntax to create a branch with an alternate name!

[Kevin Buzzard]

oh nice, this looks like it might work. Thanks!

[Eric Wieser]

You can probably rebase your fixes on top of the new branch

[Kevin Buzzard]

My main question now is when I'll be able to make the changes. The changes have been in mathlib3 for about 10 hours. When will they appear in mathlib3port?

[Jeremy Tan]

From my experience, right about now

[Kevin Buzzard]

They're there now