Dafny-generated files are not mergeable due to hard-coded line number debugging info #5749
Description
If two PRs modify the bodies of two different methods of a Dafny project, we would expect these two PRs to not conflict.
However, because backends emit a spurious line number for debugging, this line number prevents one PR to be merged with the other one, causing conflicts.
This line printing would happen only when a var-such-that fails.
This line number printing for has some issues:
- It only displays the line, whereas for a multi-file project also the file would be needed (like expect statement actually do)
- Verified code shouldn't throw an exception by definition. In the rare case it would (e.g. verification is not complete), it would be very easy to look at the source and figure out the offending var-such-that statement. This is in contrast to expect statements, which are relatively frequently expected to fail when developing.
- It prevents the merging of generated C# files when changes in Dafny are unrelated, causing developer productivity loss due to the local regeneration of the C# files, like in Fix: Support for double constant initialization in Dafny-to-Rust #5667 after another unrelated PR was merged.