Report errors originating from included files when verifying including file

[plaidfinch]

As reported in boogie-org/boogie-friends#8, the Emacs mode for Dafny does not report errors when they appear in an included file, which leads to the appearance of correct verification for all type-correct files which import type-incorrect files.

One solution to this is to enable the Dafny compiler to report errors in included files when typechecking/verifying/compiling the including files. We could localize this reported error to the line of the pertinent include statement to indicate to the user what has gone wrong.

This issue does not exist in Visual Studio; however, it does not seem like such a bad thing to produce an error annotation on the include statement saying "errors exist in this included file," even if those errors are reported from within their own file. Indeed, this would clarify for the user why it is that this file is refusing to verify, should they forget that they had included the file whose errors are being reported.

I suggest the following format for the error message: If there are errors in an included file A.dfy, and we have B.dfy with a line include "A.dfy", let Dafny say: B.dfy(<line>,<col>): Error: the included file "A.dfy" contains error(s)." I don't think we wish to report all of A.dfy's potentially many errors here; it is best, I would guess, to merely point the user toward A.dfy so that they can investigate these errors within the context of that file.

What do you think about this solution, @RustanLeino and @cpitclaudel?

[cpitclaudel]

I'm fine with the solution, as you might expect :) And I like your phrasing.

[RustanLeino]

This sounds good. As a clarification, am I correct in my understanding that if boogie-org/boogie-friends#5 were fixed, then that would also fix this issue?

[plaidfinch]

am I correct in my understanding that if boogie-org/boogie-friends#5 were fixed, then that would also fix this issue?

It seems so. But probably not vice-versa, because as per my current implementation plan, we don't report the actual errors, just their presence, to avoid duplication and spamming the user with error messages. Ideally, flycheck/flycheck#972 would fix all these issues in one fell swoop, but from the dialog on that issue page, it does not seem likely that this will easy to get merged.

[cpitclaudel]

This sounds good. As a clarification, am I correct in my understanding that if boogie-org/boogie-friends#5 were fixed, then that would also fix this issue?

I don't think so, but I could be wrong.

Ideally, flycheck/flycheck#972 would fix all these issues in one fell swoop, but from the dialog on that issue page, it does not seem likely that this will easy to get merged.

Well, it needs to be implemented first :)

[RustanLeino]

I'm detecting a couple of problems with the fix checked in on 12 Jan 2017.

One problem is that there was a manual change to Parser.cs. Note that Parser.cs is automatically generated. The proper way to make the change to the parser is to change Dafny.atg and then to run nmake in the Source/Dafny directory. In order for this to succeed, first do this:

• Create a folder parallel to your local Dafny repository. I suggest naming the new folder boogie-partners (with the hyphen, because that's how the makefile happens to write it). For example, if your Dafny root is c:\dafny, create a folder c:\boogie-partners.

• Clone the Mercurial repository at boogiepartners.codeplex.com (note the absence of a hyphen here). If you're not going to make any changes in the boogiepartners repository, or if you don't have Mercurial, you can simply download the boogiepartners.codeplex.com repository as a .zip file and extract the contents into your local c:\boogie-partners folder. Also, note that Dafny still depends on this old repository on CodePlex. It used to be that Boogie and Dafny both shared this folder, but that's no longer the case. The version of boogiepartners that Boogie uses (and which you don't need to build Dafny) has migrated to GitHub under the boogie-org organization. There's a message on boogiepartners.codeplex.com that says the repository has moved, but that message applies only to the Boogie use. (One day, we should improve this situation, but this is what it is now.)

• When you run nmake (from the VS Developers prompt) in the c:\dafny\Source\Dafny directory, I think Coco will generate two warnings (these are described in the .atg file, I think), but it should generate no more than that.

The other problem with the 12 Jan 2017 change is that DafnyExtension.sln no longer builds. It also calls one of the Parse routine, so it needs to be updated as well.

Thanks,
Rustan