{"action":"closed","issue":{"url":"https://api.github.com/repos/Microsoft/dafny/issues/16","repository_url":"https://api.github.com/repos/Microsoft/dafny","labels_url":"https://api.github.com/repos/Microsoft/dafny/issues/16/labels{/name}","comments_url":"https://api.github.com/repos/Microsoft/dafny/issues/16/comments","events_url":"https://api.github.com/repos/Microsoft/dafny/issues/16/events","html_url":"https://github.com/Microsoft/dafny/issues/16","id":167929216,"number":16,"title":"Report errors originating from included files when verifying including file","user":{"login":"kwf","id":597089,"avatar_url":"https://avatars.githubusercontent.com/u/597089?v=3","gravatar_id":"","url":"https://api.github.com/users/kwf","html_url":"https://github.com/kwf","followers_url":"https://api.github.com/users/kwf/followers","following_url":"https://api.github.com/users/kwf/following{/other_user}","gists_url":"https://api.github.com/users/kwf/gists{/gist_id}","starred_url":"https://api.github.com/users/kwf/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/kwf/subscriptions","organizations_url":"https://api.github.com/users/kwf/orgs","repos_url":"https://api.github.com/users/kwf/repos","events_url":"https://api.github.com/users/kwf/events{/privacy}","received_events_url":"https://api.github.com/users/kwf/received_events","type":"User","site_admin":false},"labels":[{"id":359270914,"url":"https://api.github.com/repos/Microsoft/dafny/labels/enhancement","name":"enhancement","color":"84b6eb","default":true}],"state":"closed","locked":false,"assignee":{"login":"kwf","id":597089,"avatar_url":"https://avatars.githubusercontent.com/u/597089?v=3","gravatar_id":"","url":"https://api.github.com/users/kwf","html_url":"https://github.com/kwf","followers_url":"https://api.github.com/users/kwf/followers","following_url":"https://api.github.com/users/kwf/following{/other_user}","gists_url":"https://api.github.com/users/kwf/gists{/gist_id}","starred_url":"https://api.github.com/users/kwf/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/kwf/subscriptions","organizations_url":"https://api.github.com/users/kwf/orgs","repos_url":"https://api.github.com/users/kwf/repos","events_url":"https://api.github.com/users/kwf/events{/privacy}","received_events_url":"https://api.github.com/users/kwf/received_events","type":"User","site_admin":false},"assignees":[{"login":"kwf","id":597089,"avatar_url":"https://avatars.githubusercontent.com/u/597089?v=3","gravatar_id":"","url":"https://api.github.com/users/kwf","html_url":"https://github.com/kwf","followers_url":"https://api.github.com/users/kwf/followers","following_url":"https://api.github.com/users/kwf/following{/other_user}","gists_url":"https://api.github.com/users/kwf/gists{/gist_id}","starred_url":"https://api.github.com/users/kwf/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/kwf/subscriptions","organizations_url":"https://api.github.com/users/kwf/orgs","repos_url":"https://api.github.com/users/kwf/repos","events_url":"https://api.github.com/users/kwf/events{/privacy}","received_events_url":"https://api.github.com/users/kwf/received_events","type":"User","site_admin":false}],"milestone":null,"comments":4,"created_at":"2016-07-27T18:56:30Z","updated_at":"2017-01-12T16:49:46Z","closed_at":"2017-01-12T16:49:46Z","body":"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.\n\nOne solution to this is to enable the Dafny compiler to report errors in includ**ed** files when typechecking/verifying/compiling the includ**ing** files. We could localize this reported error to the line of the pertinent `include` statement to indicate to the user what has gone wrong.\n\nThis 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.\n\nI 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.\n\nWhat do you think about this solution, @RustanLeino and @cpitclaudel?\n"}}
{"actor":{"display_login":"qunyanm"}}