Add support for concurrent document updates

[camrein]

This PR resolves #1448 and dafny-lang/ide-vscode#31. I've reworked the document database and added the following features to the language server:

• Pending beefy changes will be canceled for new changes. For example, if the document is not yet parsed or resolved, this procedure will be skipped/canceled in favor of the newer change.
• Incomplete verifications will be canceled for new changes. This works as much as Boogie supports it. I've observed that it leads to ObjectDisposedException inside boogie when using the cancellation API. Otherwise, it appears to be functioning.
• Incoming document requests (such as hover, completion) will wait for the current update to complete. If the awaited update is superseded by a newer one, these requests will be canceled as they might wait for an outdated document state. these requests receive the migrated information of the version requested.

This PR is work in progress and some parts need refactorings. Furthermore, this PR depends on the changes introduced in #1452.

[camrein]

Can we prevent that? @mschlaipfer any preferences?

This mechanic can be easily changed or made configurable. Just pass CancellationToken.None to LoadAsync:

dafny/Source/DafnyLanguageServer/Workspace/DocumentDatabase.cs

Lines 115 to 123 in 2c136bb

	private DocumentEntry VerifyDocument(DafnyDocument document) {
	var cancellationSource = new CancellationTokenSource();
	var updatedEntry = new DocumentEntry(
	document.Version,
	Task.Run(() => documentLoader.LoadAsync(document.Text, VerifyOnSave, cancellationSource.Token)),
	cancellationSource
	);
	return updatedEntry;
	}

I would prefer that we either merge it with enough confidence to let customers use it, or not merge it at all.

Sounds like a fair statement for me.

Just for the record, I think this PR has a huge impact on the usability of the IDE. Thanks!

Thanks, I'm glad that the effort was worth it.

[keyboardDrummer]

Is this migration so that in case of parse errors, we keep outdated resolution results since we're unable to compute new ones? Apparently the errors aren't migrated, so the new parse errors remain.

In any case, could you add a comment explaining this call?

[camrein]

done

[mschlaipfer]

But be aware that even verifications launched through onsave may now be canceled when applying a change.

Can we prevent that? @mschlaipfer any preferences?

What does "applying a change" mean here? Another onsave event? Then I think it's no problem to cancel an ongoing verification. I'd expect it to just verify the latest changed version.

[keyboardDrummer]

What does "applying a change" mean here? Another onsave event? Then I think it's no problem to cancel an ongoing verification. I'd expect it to just verify the latest changed version.

It means making any edit to (any file in?) your program.

[camrein]

What does "applying a change" mean here? Another onsave event? Then I think it's no problem to cancel an ongoing verification. I'd expect it to just verify the latest changed version.

It means making any edit to (any file in?) your program.

Only a change (text edit) in the same file cancels its ongoing verification. Changes to any other file won't affect the verification, even if the changed file was included by the currently verified file.
Maybe it makes sense to leave it as is and wait for user feedback on how practical it is.

[mschlaipfer]

What does "applying a change" mean here? Another onsave event? Then I think it's no problem to cancel an ongoing verification. I'd expect it to just verify the latest changed version.

It means making any edit to (any file in?) your program.

Only a change (text edit) in the same file cancels its ongoing verification. Changes to any other file won't affect the verification, even if the changed file was included by the currently verified file. Maybe it makes sense to leave it as is and wait for user feedback on how practical it is.

Hm, should we cancel it also for included files? I could see us lose trust in the verification results if there's a possibility that there might be a discrepancy.

[camrein]

Hm, should we cancel it also for included files? I could see us lose trust in the verification results if there's a possibility that there might be a discrepancy.

Just for clarification, to ensure we're talking about the same thing.

A includes B
B includes C

If a verification of A is currently running, it will be canceled if one changes A. The running verification won't be canceled if one edits B or C. This is a similar behavior that could be observed prior this PR: If A had reported that there are errors in B, the error won't go away by only updating B. A has to be edited/saved/reopened to trigger a reload of the includes.
So if it is necessary that the changes of B or C are respected by the verification of A, the verification of A has to be re-triggered. I should note that if A is verified, B and C aren't verified (only the saved document itself). I think this can be compared to omitting the /verifyAllModules flag when running the Dafny compiler. As mentioned, that is exactly the same behavior as before. The only difference between this PR and before is that verifications may now be canceled. If this behavior should be improved, I believe this is subject to a new issue and PR.