search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.88k stars 256 forks source link

Output issue in compile:3 for Java #1291

Open sorawee opened 3 years ago

sorawee commented 3 years ago

Two issues (that are closely related):

  1. Any program that output something that doesn't end with a newline will have an extra newline at the end. This is due to: https://github.com/dafny-lang/dafny/commit/02362fa07dd99c6b35978565dee33b9e8de1c87d#diff-954c2b2c16ed5149285314e30d39fc0fe9c9908920d040483c4ef886e558e303R1085

    To elaborate, ReadLine will read to either the end of line or the end of file, whichever comes first. The returned string does not include the newline character, however. Therefore, ReadLine + WriteLine loop will incorrectly produce an extra newline on the last line that doesn't have a newline at the end.

  2. Most compilers besides Java simply output to stderr / stdout right away (that is, RedirectStandardOutput and RedirectStandardError are false). Java is the only backend that sets these two to true and manually pump the content to the stdout, thus combining both stderr and stdout channels together. (This issue also affects other compilation levels) Two relevant commits are:

It's unclear to me how these should be handled. The Java behavior is odd, but seems intentional, so it could be that Java is right and the rest is wrong. Or it could be the opposite...

keyboardDrummer commented 3 years ago

Could you split this into two issues? I think they require separate fixes.

sorawee commented 3 years ago

I think it requires only one fix to deal with both issues at once, but I could be mistaken. I would be happy to help submitting a PR to fix the problem, too, but I don't know what is the expected behavior.

keyboardDrummer commented 3 years ago

I would be happy to help submitting a PR to fix the problem, too, but I don't know what is the expected behavior.

If you don't have a preference, why do you want to change it? Simply because the different back-ends are not consistent?

sorawee commented 3 years ago

Simply because the different back-ends are not consistent?

Yep.