Flycheck seems to report success when error is in included file

[plaidfinch]

Suppose I create two files, A.dfy and B.dfy, as follows:

A.dfy:

predicate Problem() {
   1 == false
}

B.dfy:

include "A.dfy"

lemma UhOh()
  ensures false
{
}

When viewing A.dfy, the type error in the body of Problem is correctly identified. However, when viewing B.dfy, no error is reported (the Flycheck status in the modeline indicates no errors, and there are no errors to be jumped to via Flycheck keybindings). Commenting the include statement causes the unprovable lemma to be correctly identified.

In general, this problem is: when there is a syntax or type error in an included file (i.e. A.dfy), verification of the including module (i.e. B.dfy) appears to succeed. A verification error in the included file will not cause this effect, and this effect will not mask the reporting of syntax or type errors in the including file—only verification errors are masked by this problem.

It's unclear to me whether the fix to this bug lies with Dafny or with the Emacs mode; paging @RustanLeino for further discussion of this.

[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