PRs to shorten a previous PR

Stream: general

[Damiano Testa]

Dear All,

this message is about Git-iquette. Throughout the morning, I have been producing several (very short) PRs:

#7866 -- approved, thanks Johan!
#7868
#7870 -- approved, thanks Johan!
#7871 -- introduces a new lemma
#7872
#7873

The main reason for these PRs is to shorten PR #7645, by reducing the number of touched files.

My question now is if this is good or bad behaviour! My instinct is to bundle together tiny changes into a bigger one, but I am slowly getting accustomed to the practice of producing several small, incremental changes.

Please, feel free to tell me whether these PRs are ok/silly, and whether I should continue/stop with them!

[Sebastien Gouezel]

I think short PRs like that are a very good idea. You should just make sure that they are compatible, i.e., that they don't create conflicts between one another.

[Damiano Testa]

Sébastien, thanks for your support! The PRs are certainly independent among them (unless I am mistaken, they only change proofs of existing lemmas/instances, with possibly one exception that introduces a new lemma). I have been consistently merging them back into their bigger brother and fixing conflicts, when they arose. So, hopefully, I should be ok from that point of view!

[Johan Commelin]

@Damiano Testa Yes, I think splitting into small PRs like you did is a good move

[Damiano Testa]

Great, thank you all for your support!

If/when these PRs will be merged, the number of touched files by PR #7645 should decrease by ~8, I think!

[Scott Morrison]

While many small PRs sometimes feels frustrating, because there is some extra time overhead in CI, fixing merge conflicts, and so on, I think this is more than made up for by the fact that it's so much easier to give useful reviews on focused PRs.