Let the IDE translate to and resolve Boogie only when attempting to verify #4378

keyboardDrummer · 2023-08-03T13:31:58Z

Changes

Let the IDE translate to and resolve Boogie only when attempting to verify, instead of doing those steps for all code in the project right after resolution, and before allowing any verification to be done.
- Using the experimental verification caching feature to detect which tasks were already verified before the user triggers any verification, no longer works. This is because that caching relies on pre-verification which we now only do when the user triggers verification. However, when trying to verify these cached tasks, they'll be completed immediately after pre-verification finishes. In the future, we will have to implement caching of verification based on the Dafny AST if we want it to show up before pre-verification.
- The Dafny AST nodes must now specify whether they can be verified, even before being translated to Boogie. This creates a slight duplication of effort, since this information was implicitly also provided by the Boogie translation
Properly close files after they are read, both .dfy and .dfyconfig.toml files
XUnit tests now all run sequentially. This does not seem to have a significant affect on total test runtime and makes debugging test timeouts easier because it excludes lack of available threads as a cause.
The class ConstantField is moved to a separate file
Add AutoGeneratedToken where they were missing.
Configure the dotnet test call on the CLI so individual server tests won't run for more than 6 minutes.
Split the existing OnChange mode into OnChangeFile and OnChangeProject, which let verification automatically run if either their containing file or containing project has changed, respectively.
Stringify, a method to help with debugging, has been improved
Small cleanup of CounterExampleTest, changing a List<Action> into an Action
Many improvements to logging

Testing

Existing tests have been adapted for the new behavior
The performance part improvement of this PR is not tested, since we don't have a good framework for testing performance.
Add tests for the behavior of OnChangeFile and OnChangeProject mode.
Add tests for Stringify
Add tests for FindNode

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

…able

…ectSupport

MikaelMayer

Just finished my review. I did not test this PR myself yet, so I'm relying on the CI tests, although I did not find any obvious or potential issues in the code itself.

Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs

Source/DafnyLanguageServer.Test/Util/ClientBasedLanguageServerTest.cs

Source/DafnyLanguageServer.Test/Util/StringifyTest.cs

Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs

Source/DafnyLanguageServer/Workspace/ChangeProcessors/Relocator.cs

MikaelMayer · 2023-08-10T14:22:03Z

Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs

    }

    private IdeState CreateDocumentWithEmptySymbolTable(Compilation compilation,
      IReadOnlyDictionary<Uri, IReadOnlyList<Diagnostic>> resolutionDiagnostics) {
      var dafnyOptions = DafnyOptions.Default;
      var program = new EmptyNode();
      return new IdeState(
+        compilation.Version,


Isn't that what was sufficient to ensure that gutter icons are handled in order?

Can you elaborate?

It looks like before the Ide state did not have this field and I remember you mentioning to me that because versioning had been lost, gutter icons were sometimes published in the wrong order. I was wondering if this fixes that.

Source/DafnyLanguageServer/Workspace/IdeStateObserver.cs

Source/DafnyLanguageServer/Workspace/CompilationManager.cs

Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs

…dafny into onDemandPreverification

MikaelMayer

One minor typo and I think it's good to go!

Source/DafnyLanguageServer.Test/Synchronization/VerificationStatusTest.cs

MikaelMayer · 2023-08-10T18:23:02Z

Source/DafnyLanguageServer/Workspace/TextDocumentLoader.cs

    }

    private IdeState CreateDocumentWithEmptySymbolTable(Compilation compilation,
      IReadOnlyDictionary<Uri, IReadOnlyList<Diagnostic>> resolutionDiagnostics) {
      var dafnyOptions = DafnyOptions.Default;
      var program = new EmptyNode();
      return new IdeState(
+        compilation.Version,


It looks like before the Ide state did not have this field and I remember you mentioning to me that because versioning had been lost, gutter icons were sometimes published in the wrong order. I was wondering if this fixes that.

…atusTest.cs Co-authored-by: Mikaël Mayer <[email protected]>

keyboardDrummer · 2023-08-10T19:02:42Z

It looks like before the Ide state did not have this field and I remember you mentioning to me that because versioning had been lost, gutter icons were sometimes published in the wrong order. I was wondering if this fixes that.

It previously sort of had this field, through its other field Compilation which has a version. This field is only needed because IdeState can now be migrated while keeping the same compilation, which is used in IdeObserverState.Migrate

MikaelMayer

Thanks for this excellent work.

This was breaking a CI for the last 3 runs

…erify (dafny-lang#4378) Depends on dafny-lang#4395 ### Changes Let the IDE translate to and resolve Boogie only when attempting to verify, instead of doing those steps for all code in the project right after resolution, and before allowing any verification to be done. - Using the experimental verification caching feature to detect which tasks were already verified before the user triggers any verification, no longer works. This is because that caching relies on pre-verification which we now only do when the user triggers verification. However, when trying to verify these cached tasks, they'll be completed immediately after pre-verification finishes. In the future, we will have to implement caching of verification based on the Dafny AST if we want it to show up before pre-verification. - The Dafny AST nodes must now specify whether they can be verified, even before being translated to Boogie. This creates a slight duplication of effort, since this information was implicitly also provided by the Boogie translation ### Testing - Existing tests have been adapted for the new behavior - The performance part improvement of this PR is not tested, since we don't have a good framework for testing performance. - Add tests for the behavior of `OnChangeFile` and `OnChangeProject` mode. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Aaron Tomb <[email protected]>

…erify (#4378) Depends on #4395 ### Changes Let the IDE translate to and resolve Boogie only when attempting to verify, instead of doing those steps for all code in the project right after resolution, and before allowing any verification to be done. - Using the experimental verification caching feature to detect which tasks were already verified before the user triggers any verification, no longer works. This is because that caching relies on pre-verification which we now only do when the user triggers verification. However, when trying to verify these cached tasks, they'll be completed immediately after pre-verification finishes. In the future, we will have to implement caching of verification based on the Dafny AST if we want it to show up before pre-verification. - The Dafny AST nodes must now specify whether they can be verified, even before being translated to Boogie. This creates a slight duplication of effort, since this information was implicitly also provided by the Boogie translation ### Testing - Existing tests have been adapted for the new behavior - The performance part improvement of this PR is not tested, since we don't have a good framework for testing performance. - Add tests for the behavior of `OnChangeFile` and `OnChangeProject` mode. <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small> --------- Co-authored-by: Aaron Tomb <[email protected]>

keyboardDrummer added 30 commits July 28, 2023 10:56

Move IVariableConstracts and NonglobalVariable to separate files

d30addf

Moves remaining classes in DafnyAst.cs to separate files

3b64410

All the changes

ee3c60c

Compute static hover information using AST instead of legacy symbol t…

afd11a6

…able

Refactoring

a68499e

Use project files in hover of HoverTest tests

7324c61

Fix bug in Formal.Children

ef30c41

Use more INode instead of Node

f15f284

Cleanup

59de765

Refactoring

ef9bf1d

Rename

ae34c37

Merge commit 'afd11a6dc53' into hoverAndGutterIconProjectSupport

79a4bf4

Merge branch 'computeStaticHoverUsingAst' into hoverAndGutterIconProj…

ab1e1ce

…ectSupport

Merge commit '6506c83868~1' into computeStaticHoverUsingAst

4d81e72

Merge commit '6506c83868' into computeStaticHoverUsingAst

5f565c8

Fix tests and formatting

524a5a3

Fix bugs and refactor

506af99

Merge branch 'master' into computeStaticHoverUsingAst

b6ba8ac

Draft

c2dd161

Split parsing and resolution

e8eece8

Small refactoring

bf9db2e

Running tests

380ceea

Ran formatter

7b03876

Update expect file

953f0f8

Increase unlock wait time

26b642f

Throw exception instead of returning null

cafd9e9

Merge branch 'master' into computeStaticHoverUsingAst

96d2fc3

More passing tests

bfa8966

Let more tests pass

ebc491a

Merge branch 'master' into computeStaticHoverUsingAst

5167023

keyboardDrummer added 5 commits August 10, 2023 15:03

Properly close project file stream

c354064

Concurrency fixes

564eaf1

Better hygiene

4fa74fc

Resolve TODO

0c3b5cb

Code review

a6e3b68

MikaelMayer reviewed Aug 10, 2023

View reviewed changes

keyboardDrummer added 10 commits August 10, 2023 16:43

Add fix

b792e95

Merge branch 'master' into onDemandPreverification

31a865f

Remove TODOs

7e6c8ba

Two fixes

10993fd

Add AutoGeneratedTokens where needed

43e069e

Change wait mechanics

e76064c

Merge branch 'onDemandPreverification' of github.com:keyboardDrummer/…

96ef23a

…dafny into onDemandPreverification

Resolve TODO

e10c8f7

Add exception handler to counter example handler

aff3490

Ran formatter

1f462f0

MikaelMayer reviewed Aug 10, 2023

View reviewed changes

Update Source/DafnyLanguageServer.Test/Synchronization/VerificationSt…

6a2a90b

…atusTest.cs Co-authored-by: Mikaël Mayer <[email protected]>

MikaelMayer previously approved these changes Aug 10, 2023

View reviewed changes

MikaelMayer added 2 commits August 10, 2023 15:39

Merge branch 'master' into onDemandPreverification

df567bf

Update Twostate-Functions.dfy.expect

95c5e5a

This was breaking a CI for the last 3 runs

MikaelMayer dismissed their stale review via 95c5e5a August 10, 2023 20:55

MikaelMayer approved these changes Aug 10, 2023

View reviewed changes

keyboardDrummer merged commit 99635a1 into dafny-lang:master Aug 11, 2023
18 checks passed

keyboardDrummer deleted the onDemandPreverification branch August 11, 2023 08:39

BrewTestBot mentioned this pull request Sep 29, 2023

dafny 4.3.0 Homebrew/homebrew-core#146965

Merged

MikaelMayer mentioned this pull request Oct 12, 2023

Resolution errors no longer appearing in the gutter #4656

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Let the IDE translate to and resolve Boogie only when attempting to verify #4378

Let the IDE translate to and resolve Boogie only when attempting to verify #4378

keyboardDrummer commented Aug 3, 2023 •

edited

Loading

MikaelMayer left a comment

MikaelMayer Aug 10, 2023

keyboardDrummer Aug 10, 2023

MikaelMayer Aug 10, 2023

MikaelMayer left a comment

MikaelMayer Aug 10, 2023

keyboardDrummer commented Aug 10, 2023

MikaelMayer left a comment

Let the IDE translate to and resolve Boogie only when attempting to verify #4378

Let the IDE translate to and resolve Boogie only when attempting to verify #4378

Conversation

keyboardDrummer commented Aug 3, 2023 • edited Loading

Changes

Testing

MikaelMayer left a comment

Choose a reason for hiding this comment

MikaelMayer Aug 10, 2023

Choose a reason for hiding this comment

keyboardDrummer Aug 10, 2023

Choose a reason for hiding this comment

MikaelMayer Aug 10, 2023

Choose a reason for hiding this comment

MikaelMayer left a comment

Choose a reason for hiding this comment

MikaelMayer Aug 10, 2023

Choose a reason for hiding this comment

keyboardDrummer commented Aug 10, 2023

MikaelMayer left a comment

Choose a reason for hiding this comment

keyboardDrummer commented Aug 3, 2023 •

edited

Loading