Warning messages linger after file is closed

[RustanLeino]

Problem

I have a file open in VS Code and the Problems pane is showing a warning about the file. When I close the file, the warning is still listed in the Problems pane.

Repro

• Use View->Problems to make the Problems pane visible if it isn't already.

• Open a folder in VS Code. (I've tried it both with and without a dfyconfig.toml file. The issue occurs with both.)

• Open or create a file LingeringWarnings.dfy with the following contents:

  method M() returns (r: int)
    ensures r < 10

  This should show a warning in the Problems pane.

• Close the file. The warning is still showing in the Problems pane.

Version

I'm using Dafny IDE version 3.4.4. In it, I use Dafny version 4.10 or "latest stable release" (which I think are the same at this time).

Mitigation

The only way I know how to get rid of the warning is to restart VS Code. Or to reopen the file, change the file to make the warning go away, save the file, and close it.

[keyboardDrummer]

LSP server behaves as expected. After closing it sends empty diagnostics. However, VSCode+the extension then opens the document again, even though it is visually closed in VSCode, and then the LSP server sends non-empty diagnostics again.

Next steps is investigating why VSCode would trigger an open event for a document that was just closed.

[Trace - 3:46:41 PM] Sending notification 'textDocument/didOpen'.
Params: {
    "textDocument": {
        "uri": "file:///Users/rwillems/Documents/Sync/Scratchpad/LingeringWarnings.dfy",
        "languageId": "dafny",
        "version": 1,
        "text": "method M() returns (r: int)\n  ensures r < 10"
    }
}

[Trace - 3:46:42 PM] Received notification 'textDocument/publishDiagnostics'.
Params: {
    "uri": "file:///Users/rwillems/Documents/Sync/Scratchpad/LingeringWarnings.dfy",
    "version": 1,
    "diagnostics": [
        {
            "range": {
                "start": {
                    "line": 1,
                    "character": 10
                },
                "end": {
                    "line": 1,
                    "character": 16
                }
            },
            "severity": 2,
            "code": "none",
            "codeDescription": {
                "href": "https://dafny.org/dafny/HowToFAQ/Errors#none"
            },
            "source": "Verifier",
            "message": "This ensures clause is part of a bodyless method. Add the {:axiom} attribute to it or the enclosing method to suppress this warning",
            "relatedInformation": []
        }
    ]
}

[Trace - 3:46:47 PM] Sending notification 'textDocument/didClose'.
Params: {
    "textDocument": {
        "uri": "file:///Users/rwillems/Documents/Sync/Scratchpad/LingeringWarnings.dfy"
    }
}


[Trace - 3:46:47 PM] Received notification 'textDocument/publishDiagnostics'.
Params: {
    "uri": "file:///Users/rwillems/Documents/Sync/Scratchpad/LingeringWarnings.dfy",
    "diagnostics": []
}


[Trace - 3:46:47 PM] Sending notification 'textDocument/didOpen'.
Params: {
    "textDocument": {
        "uri": "file:///Users/rwillems/Documents/Sync/Scratchpad/LingeringWarnings.dfy",
        "languageId": "dafny",
        "version": 1,
        "text": "method M() returns (r: int)\n  ensures r < 10"
    }
}


[Trace - 3:46:47 PM] Received notification 'textDocument/publishDiagnostics'.
Params: {
    "uri": "file:///Users/rwillems/Documents/Sync/Scratchpad/LingeringWarnings.dfy",
    "version": 1,
    "diagnostics": [
        {
            "range": {
                "start": {
                    "line": 1,
                    "character": 10
                },
                "end": {
                    "line": 1,
                    "character": 16
                }
            },
            "severity": 2,
            "code": "none",
            "codeDescription": {
                "href": "https://dafny.org/dafny/HowToFAQ/Errors#none"
            },
            "source": "Verifier",
            "message": "This ensures clause is part of a bodyless method. Add the {:axiom} attribute to it or the enclosing method to suppress this warning",
            "relatedInformation": []
        }
    ]
}