Have github actions automatically push PR autofixes

[lihaoyi]

This will save the tedious process of noticing formatting/scalafix irregularities and having to run a manual command before pushing them.

[lefou]

Not sure how exactly this work or why there is this message "please use git push -f", but if you need --force please use --force-with-lease, making following a branch easier. Why do we encourage to force push at all? I always communicate the opposite, since it makes reviewing PRs much harded and GitHub UI looses all personal review state and I have to start over. Also, a lightly git push -f risks to loose commits made by other maintainers.

[lefou]

Suggested change

	git commit --allow-empty -am 'Github Actions Autofix; please use "git push -f" next time you push to this PR';
	git commit --allow-empty -am 'Github Actions Autofix; please use "git push --force-with-lease" next time you push to this PR';

[lihaoyi]

git push -f is just the way I've done this kind of CI-driven autofixes before, and it worked fine. The alternative is to ask people to git fetch the CI autofix before proceeding with local development, which works as well.

[lefou]

git push -f is just the way I've done this kind of CI-driven autofixes before, and it worked fine. The alternative is to ask people to git fetch the CI autofix before proceeding with local development, which works as well.

I have a alias git pullr for that which stands for pull --rebase --autostash. It will rebase all local commits on top of upstream changes. It will also work with local uncommitted changes, which will be temporarily stashed.

git push -f without fetching is dangerous, since you may loose some commits, without even noticing. We definitely should not recommend this.