Make status bar forward compatible with upcoming Dafny release

[keyboardDrummer]

Changes

• Let the status bar remember the message it has when resolution was previously finished, so it can show that message again when resolution finishes again. This is required to keep an up-to-date status bar together with the server changes in No duplicate symbol status dafny#4523. This change is only triggered by the new event "ResolutionSucceeded", and so is backwards compatible with older Dafny versions.
• Do not let VerificationSymbolStatusView update the status bar, but let the status bar work independently, so the status bar remains up to date even if 'verification as tests' is turned off.

Testing

• Test that the status bar behaves well with No duplicate symbol status dafny#4523
• Test that the status bar behaves well on Dafny 4.2
• Did not manage to test against 3.7 because of my M1 laptop and failing to build it locally. Any chance you could do that @MikaelMayer ?

[MikaelMayer]

I just tested this branch on Dafny 3.7, on this simple example:

method Test() {
  assert false;
}

it's stuck on "Verifying" both on the status bar and the gutter icons. The arguments are

Standalone language server installation completed.
Language server: {"command":"C:\\Program Files\\dotnet\\dotnet.EXE","args":["c:\\Users\\mimayere\\Documents\\ide vscode\\out\\resources\\3.9.0\\github\\dafny\\DafnyLanguageServer.dll","--documents:verify=onchange","--verifier:timelimit=30","--verifier:verifySnapshots=0","--verifier:vcscores=4","--ghost:markStatements=true","--verifier:gutterStatus=true"]}
Dafny is ready

On 3.8.0, it's stuck on "Verified 0/1, verifying Test"

On 3.9.0 it correctly displays "assertion might not hold" on the "false" and gutter icons respond correctly

[keyboardDrummer]

I just tested this branch on Dafny 3.7

I see that the same problem occurs on the VSCode extension master for Dafny 3.7 and 3.8. Looking at what the server sends last for 3.7:

Params: {
    "uri": "file:///Users/rwillems/Documents/Sync/DafnyExamples/test.dfy",
    "version": 8,
    "status": "VerificationStarted",
    "message": "0/1 Bat"
}

This is not telling the IDE to display anything more than "Verifying", so no IDE fix will make it backwards compatible with this older server version.

For the gutter icons, the server seems to be using an older API version, since the numbers don't match with what I'm used to from the latest gutter icon API.

Params: {
    "uri": "file:///Users/rwillems/Documents/Sync/DafnyExamples/test.dfy",
    "version": 8,
    "perLineStatus": [
        0,
        2,
        2,
        2,
        2,
        2,
        2,
        2,
        2,
        2,
        2,
        2
    ]
}

On 3.8 I also see this in the logs:

 ---> Microsoft.Boogie.ProverDiedException: Prover died with no further output, perhaps it ran out of memory or was killed.
   at Microsoft.Boogie.Checker.ReadOutcome()
   at VC.Split.ReadOutcome(Int32 iteration, Checker checker, VerifierCallback callback)

Maybe we're testing 3.7 and 3.8 against the wrong version of Z3.

However, it seems that the status bar is correctly responding to the information it's getting from the server, so I suggest we consider this test 'passed', even though something is wrong with the server we're testing against and that doesn't give us the right end-to-end behavior.