On Sat, Apr 11, 2020 at 10:24:33AM +0100, haael wrote:
Imagine I wanted to take code from some public repo and add loop invariants to it. If the diff touches half of the lines of the code, it will never be merged.
You have a social problem: you want to annotate for-loops with some sort of unspecified loop invariant, but the maintainers won't accept it if you dump a huge diff in their laps.
Okay, but that's between you and the project maintainers, nothing to do with us.