Flycheck seems to report success when error is in included file

[boogie-org]

Flycheck seems to report success when error is in included file

[cpitclaudel]

Thanks. Just to clarify, this is distinct from #5, right?

I think the bug is probably in the Dafny server.

[cpitclaudel]

I think the bug is probably in the Dafny server.

Actually, scratch that, at least in part. The error is properly reported, but it's discarded by Flycheck, because Flycheck discards errors in included files. flycheck/flycheck#972 was going to fix this, but the contributor didn't complete the implementation :/

There's an easy fix that can be implemented on the Dafny side. In addition to reporting the original error in A.dfy, Dafny could report an error in B.dfy on the include line, saying something like "Error: B.dfy has syntax errors".

Then that error would appear when verifying B.dfy.

[plaidfinch]

flycheck/flycheck#972 was going to fix this, but the contributor didn't complete the implementation :/

That's frustrating.

There's an easy fix that can be implemented on the Dafny side. In addition to reporting the original error in A.dfy, Dafny could report an error in B.dfy on the include line, saying something like "Error: B.dfy has syntax errors".

Sounds good to me! I've filed dafny-lang/dafny#16 documenting this proposed solution.

[cpitclaudel]

flycheck/flycheck#972 was going to fix this, but the contributor didn't complete the implementation :/

That's frustrating.

Indeed :) If you're curious about ELisp, this could be a nice starting project!

[cpitclaudel]

This is fixed now