Add format rebase bot command

[upsj]

Instead of filling the git history with format commits, this PR adds a format-rebase! command that formats each individual commit instead by rewriting the history.

[pratikvn]

I am not too sure of this. How would this work ? Would it rewrite each of the commits ? That might make things unnecessarily complicated with different commits on your local system and on github. I feel that this would be more error-prone.

[upsj]

Yes, like rebase! this rewrites the history for each individual commit, so you need to git fetch && git reset --hard origin/<branch> to get the new state locally. An alternative would be to run the command from the shell script manually.

To elaborate a bit on my thoughts for this: It is helpful for all kinds of operations (git blame, git bisect, ...) if most if not all intermediate states of develop are in a clean state. This is especially relevant for the few long-lived branches we have (batch, MPI, block-ILU, ...), since they can be hundreds of commits ahead of the code.

[tcojean]

In general LGTM, I like the idea.

Do you have an example of it working in your playground?

[upsj]

@tcojean I made a few updates in the playground (especially storing the individual diffs as artifacts of the job, to be able to roll back any potential breakages), but in general you can check it out for yourself, yes. You should have access: https://github.com/upsj/ginkgo-bot-playground

[yhmtsai]

dev_tools/scripts branch?

[upsj]

dev_tools/scripts folder ;) restore it to its previous state

[yhmtsai]

Could you remind me why it only needs to copy the first execution file not those source files?

[upsj]

the file may be overwritten when checking out a different state from the repo. Copying it avoids the resulting race conditions between bash reading the file and git updating it.

[yhmtsai]

Suggested change

	git push --force-with-lease fork $LOCAL_BRANCH:$HEAD_BRANCH 2>&1 || bot_error "Cannot push rebased branch, are edits for maintainers allowed?"
	git push --force-with-lease fork $LOCAL_BRANCH:$HEAD_BRANCH 2>&1 || bot_error "Cannot push rebased branch, are edits for maintainers allowed or are there changes introduced during rebase?"

[Slaedr]

I would prefer if we kept any merge commits. I guess if the merge commit is empty, it will still be discarded, but in general, I think this way would be better. This will not matter for most branches, but it will for long-lived branches like batch-develop.

Suggested change

	git rebase --empty=drop --no-keep-empty \
	git rebase --empty=drop --no-keep-empty --rebase-merges \

[upsj]

I don't think that's a good idea - rebasing the complete topology of a branch involving merges is pretty complex and loses all connection to the original branches. batch-develop is enough of a special case that we can do that by hand.