When using include, helpful "this is the precondition that might not hold" information is missing from flycheck errors

[wilcoxjay]

Consider a that has two files A.dfy and B.dfy. A contains library declarations, which B uses via the include directive.

// A.dfy
method foo(x: int)
  requires x > 0
  requires x % 2 == 0
{
} 

// B.dfy
include "A.dfy"

method bar()
{
  foo(0);
}

Then flycheck will report that a precondition of foo is violated, but it won't tell you which one. This gets annoying when there are many preconditions, and I am reduced to copy-pasting the contents of A into B or to running dafny on the command line.

Would it be possible to get this information into flycheck, preferably including the ability to jump to the precondition, just like when the caller and callee are in the same file?

[cpitclaudel]

Thanks for that report! That's indeed annoying :/ C-c C-c is probably a half-decent workaround, as long as your files are quick to process.

The issue is within the Dafny server implementation (not within the Emacs mode), and I need to debug that. That could take a while; I may have time next week-end though.