Separate UI code and business logic for the resolve and verify commands #4798

keyboardDrummer · 2023-11-17T20:22:17Z

Changes

At the heart of this PR is an architectural change: to lay the foundation for separating UI code from business logic. Part of this is to use Boogie purely as an API, instead of as a library that produces textual output for the CLI.

This change is not necessary, but I believe it is a good step towards giving us more control over the UI experience of our CLI, and to make it easier to work with our codebase. In the future section down below are some ideas of what this PR enables.

Because there is a lot of UI code intermingled with a lot of business code, making this architectural change produces a lot of code changes, so this PR only takes the first step: the pathway where UI and logic are separated is only used when using dafny resolve or dafny verify. I will update the remaining commands in follow-up PRs.

Refactoring

Move Compilation, a UI agnostic back-end for driving the Dafny compiler pipeline, from the project LanguageServer to DafnyCore, so it can be used by the CLI as well. Reusing this code means more IDE code is tested using the CLI test, and you can see the effect of this additional testing from the IDE fixes down below, yay!
Introduce CliCompilation which uses the CLI as a user interface to track the results of Compilation.
Let the commands dafny resolve and dafny verify use CliCompilation instead of CompilerDriver .
Due to the introduction of CliCompilation, rename CompilerDriver to SynchronousCliCompilation, even though there are many features CliCompilation does not support yet.
Remove DafnySymbolKind from DafnyCore, which was a duplicate of an LSP enum that is now directly accessible in DafnyCore

Behavior

IDE fix: enable comma's in the library flag to specify multiple libraries, as the CLI does
IDE fix: enable having the same file as input multiple times, as the CLI does
IDE fix: support verification for some code generating Dafny constructors, like iterators
IDE fix: the option solver-path is respected by the IDE
IDE fix: when verification can not start due to a technical issue, the IDE tells the user what happened
Make it easy to update .expect files by setting the flag DiffCommand.UpdateExpectFile to true. This was broken before this PR.
Configure littish tests so they time out after running for 120 minutes. They normally complete in less than 30m on all platforms, so 120m should be ample.
Fix a bug in the cloning code, that was discovered because the CLI tests are using the server back-end code, which clones the program after parsing. (Is this good or bad? In the future I hope we'll have an immutable AST so then the question becomes redundant)
Make the order in which verification error are shown on the CLI consistent. Now errors are always shown in the order in which they occur in the file

Example diff:

- git-issue-4074.dfy(24,11): Error: assertion might not hold
git-issue-4074.dfy(5,9): Error: assertion might not hold
git-issue-4074.dfy(14,11): Error: assertion might not hold
+ git-issue-4074.dfy(24,11): Error: assertion might not hold

Consistently let CLI diagnostics have a Warning/Error label. Example diff:

- github-issue-4804.dfy(19,8): Verification out of resource (Power.LemmaPowSubAddCancel (correctness))
+ github-issue-4804.dfy(19,8): Error: Verification out of resource (Power.LemmaPowSubAddCancel (correctness))

The way in which custom error messages is shown is slightly different. Example diff:

CustomErrorMesage.dfy(42,63): Error: this loop invariant could not be proved on entry
- CustomErrorMesage.dfy(42,63): Related message: position variable out of range
+  Related message: position variable out of range

Future

This PR paves the way for:

Adding a --filter option that operates on Dafny symbols/files, and possibly also filters parsing and resolution
Update the CLI output.
- Removed useless "related message" output. Example below this list.
- Improve summary output. Dafny currently reports Dafny program verifier finished with 21 verified, 0 errors but the number 21 does not refer to anything visible to the user. It would be better to report the number of Dafny symbols that were verified.
- Do not report Dafny program verifier did not attempt verification when running dafny resolve

Definedness.dfy(175,27): Error: this loop invariant could not be proved on entry
- Definedness.dfy(175,27): Related message: loop invariant violation

How has this been tested?

Updated existing tests to account for behavioral changes

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

…ion Manager

…into compilationEvents

robin-aws

Reviewed most of the rest, just need to have a final look at the core changes in a third batch.

docs/HowToFAQ/Errors-CommandLine.md

Source/DafnyCore/Pipeline/Compilation.cs

Source/DafnyCore/Generic/ReporterExtensions.cs

Source/IntegrationTests/TestFiles/LitTests/LitTest/doofiles/Test2.dfy.expect

Source/IntegrationTests/TestFiles/LitTests/LitTest/cli/projectFile/projectFile.dfy.expect

Source/DafnyDriver/DafnyBackwardsCompatibleCli.cs

robin-aws · 2024-01-18T21:36:09Z

Source/DafnyLanguageServer/Language/Symbols/ISymbolTableFactory.cs

-    /// <summary>
-    /// Initializes a new symbol table with the given compilation unit.
-    /// </summary>
-    /// <param name="program">The parsed dafny program.</param>
-    /// <param name="compilationUnit">The compilation to create the symbol table of.</param>
-    /// <param name="cancellationToken">A token to cancel the update operation before its completion.</param>
-    /// <returns>A symbol table representing the provided compilation unit.</returns>
-    /// <exception cref="System.OperationCanceledException">Thrown when the cancellation was requested before completion.</exception>
-    /// <exception cref="System.ObjectDisposedException">Thrown if the cancellation token was disposed before the completion.</exception>


Why delete this comment?

Was it useful? I would argue it's not. Even the interface ISymbolTableFactory is unused.

Given the amount of refactoring going on I just wanted to make sure it wasn't dropped by accident. If you removed it because it wasn't useful that's just fine (and looking closer I agree it seems like "I'm being forced to document every method" rather than "I have something useful to say beyond the signature here" :)

robin-aws · 2024-01-18T21:36:43Z

Source/DafnyLanguageServer/Workspace/INotificationPublisher.cs

-    /// <summary>
-    /// Publishes the diagnostics of the specified dafny document to the connected LSP client.
-    /// </summary>
-    /// <param name="state">The document whose diagnostics should be published.</param>


I'll add it back.

robin-aws

A few more for today. :)

Source/DafnyCore/AST/Grammar/Printer.cs

robin-aws · 2024-01-18T23:56:13Z

Source/DafnyCore/Pipeline/Compilation.cs

+    if (Options.UseStdin) {
+      var uri = new Uri("stdin:///");
+      result.Add(DafnyFile.CreateAndValidate(errorReporter, fileSystem, Options, uri, Token.Cli));
+    }


OoC what happens if you specify this in the IDE?

You can't. StdIn is not an IDE option.

Sure, I'm just pointing out that technically you could add --stdin to the Language Server Launch Args, and now it seems like it would actually do something rather than being ignored. I assume it's harmless but asking just in case.

If you use the CLI to specify an option to a command to which it doesn't apply, then the CLI will return an error. If you pass it through the project file, the CLI won't error but it'll be ignored.

robin-aws · 2024-01-19T00:08:41Z

Source/DafnyDriver/CliCompilation.cs

+    } catch (TaskCanceledException) {
+    }


When does this happen? Why not catch OperationCanceledException instead?

Added a comment and changed to OperationCanceledException. Happens when there's a parsing error so it can not resolve. I could change the interface of Compiler so it uses null instead of OperationCanceledException when it can't return a Task<ResolutionResult due to a user program error. This means inside Compilation there's a need for more if (resultIDependOn == null) { return null } since we don't coast on the monadic behavior of async/await, but it might be more readable.

I'd prefer doing that in a follow-up PR, this one is huge as is.

robin-aws · 2024-01-19T00:10:46Z

Source/DafnyCore/Pipeline/Compilation.cs

+      if (HasErrors) {
+        throw new OperationCanceledException();
+      }


The name of this exception always bothered/confused me a little, and it feels worse using it in the CLI context now: it sounds like the user cancelled the pipeline, when it's really that the pipeline stoped early because of errors.

Is this usage idiomatic for C# in general when hitting an "early return" as opposed to a parallel cancellation request?

See above answer

Co-authored-by: Robin Salkeld <[email protected]>

… into mergedCLiAndServer

robin-aws

Last batch!

robin-aws · 2024-01-22T21:51:01Z

Source/DafnyDriver/CliCompilation.cs

+
+  public Task<ResolutionResult> Resolution => Compilation.Resolution;
+
+  public void Start() {


Worth raising an explicit error if Start is called more than once?

robin-aws · 2024-01-22T21:51:42Z

Source/DafnyDriver/CliCompilation.cs

+        new DafnyProgramVerifier(factory.CreateLogger<DafnyProgramVerifier>()), engine, input);
+  }
+
+  public async Task VerifyAllAndPrintSummary() {


Similarly, can we raise an error if Start wasn't called yet? Otherwise I assume you just get deadlock.

In theory you can first call VerifyAllAndPrintSummary but not await the result, then call Start, and then await the task, although I don't see why you would do that.

robin-aws · 2024-01-22T21:59:40Z

Source/DafnyDriver/CliCompilation.cs

+        foreach (var canVerify in orderedCanVerifies) {
+          canVerifyResults[canVerify] = new CliCanVerifyResults();
+          await Compilation.VerifyCanVerify(canVerify, false);
+        }


Would it be more efficient/cleaner to do await Task.WhenAll(...) instead in general, rather than awaiting inside a loop like this?

I have to await before I do the next call, to ensure that the previous verification work has finished being queued. Otherwise, the order in which things get verified becomes non-deterministic.

robin-aws · 2024-01-22T22:23:05Z

Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs

      this.logger = logger;
      this.innerLogger = innerLogger;
      this.telemetryPublisher = telemetryPublisher;
    }

    private readonly ResolutionCache resolutionCache = new();
-    public CompilationUnit ResolveSymbols(DafnyProject project, Program program, CancellationToken cancellationToken) {
+    public void ResolveSymbols(Compilation compilation, Program program, CancellationToken cancellationToken) {


It feels redundant to be passing in a program separately from the compilation here (and probably other similar places). Does it have to be the same as compilation.programAfterParsing?

This is a mutating operation, and program is the program to mutate. It's a bit much for this code to assume which Program field that Compilation exposes it may mutate. For example, compilation.programAfterParsing would be the wrong one to mutate ! That's an instance of Program which is just the parsed program and which won't be changed afterwards.

robin-aws · 2024-01-22T22:24:05Z

Source/DafnyLanguageServer/Language/Symbols/SymbolTableFactory.cs

+      var compilationUnit = resolutionResult.HasErrors
+        ? new CompilationUnit(input.Project.Uri, resolutionResult.ResolvedProgram)
+        : new SymbolDeclarationResolver(logger, cancellationToken).ProcessProgram(input.Project.Uri, resolutionResult.ResolvedProgram);
+      // telemetryPublisher.PublishTime("LegacyServerResolution", project.Uri.ToString(), DateTime.Now - beforeLegacyServerResolution); TODO


robin-aws · 2024-01-22T22:26:13Z

Source/DafnyLanguageServer/Workspace/IdeState.cs

@@ -139,4 +161,379 @@ public record IdeState(
  public IEnumerable<Uri> GetDiagnosticUris() {
    return StaticDiagnostics.Keys.Concat(VerificationResults.Keys);
  }
+


I assume all the code from this point on is relocated rather than brand new? If not, how's the testing coverage?

It is relocated, yes

robin-aws · 2024-01-22T22:28:24Z

Source/IntegrationTests/TestFiles/LitTests/LitTest/logger/ProofDependencyLogging.dfy

@@ -111,7 +111,7 @@
 // CHECK:       ProofDependencies.dfy\(337,12\)-\(337,16\): requires clause
 // CHECK:       ProofDependencies.dfy\(338,11\)-\(338,15\): ensures clause
 // CHECK:       ProofDependencies.dfy\(341,3\)-\(341,39\): function call result
-// CHECK:       ProofDependencies.dfy\(341,3\)-\(341,3\): function precondition satisfied


Not seeing why this location changed, was it actually incorrect before?

I'm not sure we have enough consistency in our reporting to say what's correct or not, but previously it reported a "range" which was just twice the starting position of the call, and now the range is the entire call expression.

robin-aws · 2024-01-22T22:29:00Z

docs/dev/news/4798.feat

+- Fix: verification in the IDE no longer fails for iterators
+- Fix: the IDE now provides feedback when verification fails to run, for example due to a bad solver path
+- Fix: let the IDE correctly use the solver-path option when it's specified in a project file
+- Feat: improve the order of verification diagnostics emitted by the Dafny CLI, so that they now always follow the line order of the program.


robin-aws

A lot of work but well worth it, thanks!

keyboardDrummer added 30 commits October 30, 2023 15:55

Compilation events draft

fa63567

Gutter icons using IdeState draft

cb443d8

Remove unused field

ae2416f

Merge branch 'ideStateBasedGutterIcons' into compilationEvents

5168c3f

ObservableErrorReporter

83b6344

Builds. ActionInput relying on tokens is still an issue though

09bb2d0

Diagnostics work again

95099a3

Cleanup

6768460

Various fixes

ce3d06f

Fix

8a32cc6

Fixes

39b4aba

Remove comment

a2094b9

Update verification trees through events, instead of through Compilat…

c9e889e

…ion Manager

Many diagnostics tests pass

ffee6cf

Most tests pass, except the tree ones

2427f1e

More fixes

e77b252

Signature help handler tests pass

131aa13

Bunch of gutter icon tests now passing

61a5d68

Gutter status seems to work as well

37982ae

Ran formatter

9ac85b9

Merge branch 'master' into compilationEvents

dbd44fe

Compilation changes

6f6fbd6

Diagnostics cleanup

93e065c

Merge branch 'master' into compilationEvents

c2abf78

Little bit more compilation cleanup

88ec526

Merge branch 'compilationEvents' of github.com:keyboardDrummer/dafny …

26e70f8

…into compilationEvents

Last document changes

8acea63

It compiles

9d4c213

Cleanup

16b1db9

Renames

86993be

keyboardDrummer added 2 commits January 17, 2024 15:24

Merge remote-tracking branch 'origin/master' into mergedCLiAndServer

a6f8abe

Fixes related to exceptions

51d0d82

keyboardDrummer requested a review from robin-aws January 17, 2024 15:28

keyboardDrummer added 3 commits January 18, 2024 12:25

Add tests and fixes

7ed5fb7

Ran formatter

4bce2b2

Cleanup

cd53845

keyboardDrummer force-pushed the mergedCLiAndServer branch from 0fe3d68 to cd53845 Compare January 18, 2024 11:45

robin-aws reviewed Jan 18, 2024

View reviewed changes

robin-aws mentioned this pull request Jan 18, 2024

Use async main methods to avoid waiting for tasks at the top level #4585

Merged

robin-aws reviewed Jan 19, 2024

View reviewed changes

keyboardDrummer and others added 4 commits January 19, 2024 10:10

Update Source/DafnyCore/Pipeline/Compilation.cs

dac2895

Co-authored-by: Robin Salkeld <[email protected]>

Small updates

7da110c

Merge branch 'mergedCLiAndServer' of github.com:keyboardDrummer/dafny…

91b259e

… into mergedCLiAndServer

Merge remote-tracking branch 'origin/master' into mergedCLiAndServer

f68f103

keyboardDrummer requested a review from robin-aws January 20, 2024 18:39

keyboardDrummer added 2 commits January 22, 2024 14:15

Fix expect files

6ce9aeb

Merge remote-tracking branch 'origin/master' into mergedCLiAndServer

c5cdef6

robin-aws reviewed Jan 22, 2024

View reviewed changes

keyboardDrummer added 2 commits January 23, 2024 12:22

Code review

2961bb2

Merge remote-tracking branch 'origin/master' into mergedCLiAndServer

59d0b39

keyboardDrummer force-pushed the mergedCLiAndServer branch from 1ca98aa to 59d0b39 Compare January 23, 2024 11:28

keyboardDrummer requested a review from robin-aws January 23, 2024 11:28

keyboardDrummer added 2 commits January 23, 2024 14:25

Fix oops

1ef5366

Fix IDE bug

fad0e12

robin-aws approved these changes Jan 23, 2024

View reviewed changes

keyboardDrummer merged commit 9d85655 into dafny-lang:master Jan 23, 2024
20 checks passed

keyboardDrummer deleted the mergedCLiAndServer branch January 23, 2024 21:06

keyboardDrummer mentioned this pull request Jan 30, 2024

Guarantee same diagnostics between verify and server commands #3109

Open

robin-aws mentioned this pull request Feb 8, 2024

Regression: CLI no longer prints helpful message if Z3 not found #5067

Closed

keyboardDrummer mentioned this pull request Feb 15, 2024

Hang with dafny verify on Std #5088

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Separate UI code and business logic for the resolve and verify commands #4798

Separate UI code and business logic for the resolve and verify commands #4798

keyboardDrummer commented Nov 17, 2023 •

edited by robin-aws

Loading

robin-aws left a comment

robin-aws Jan 18, 2024

keyboardDrummer Jan 19, 2024

robin-aws Jan 22, 2024

robin-aws Jan 18, 2024

keyboardDrummer Jan 19, 2024

robin-aws left a comment

robin-aws Jan 18, 2024

keyboardDrummer Jan 19, 2024

robin-aws Jan 19, 2024

keyboardDrummer Jan 20, 2024

robin-aws Jan 19, 2024

keyboardDrummer Jan 19, 2024 •

edited

Loading

robin-aws Jan 19, 2024

keyboardDrummer Jan 20, 2024

robin-aws left a comment

robin-aws Jan 22, 2024

robin-aws Jan 22, 2024

keyboardDrummer Jan 23, 2024 •

edited

Loading

robin-aws Jan 22, 2024

keyboardDrummer Jan 23, 2024 •

edited

Loading

robin-aws Jan 22, 2024

keyboardDrummer Jan 23, 2024

robin-aws Jan 22, 2024

robin-aws Jan 22, 2024

keyboardDrummer Jan 23, 2024

robin-aws Jan 22, 2024

keyboardDrummer Jan 23, 2024

robin-aws Jan 22, 2024

robin-aws left a comment


		public Task<ResolutionResult> Resolution => Compilation.Resolution;

		public void Start() {

Separate UI code and business logic for the resolve and verify commands #4798

Separate UI code and business logic for the resolve and verify commands #4798

Conversation

keyboardDrummer commented Nov 17, 2023 • edited by robin-aws Loading

Changes

Refactoring

Behavior

Future

How has this been tested?

robin-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

robin-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Jan 19, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

robin-aws left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Jan 23, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

keyboardDrummer Jan 23, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

robin-aws left a comment

Choose a reason for hiding this comment

keyboardDrummer commented Nov 17, 2023 •

edited by robin-aws

Loading

keyboardDrummer Jan 19, 2024 •

edited

Loading

keyboardDrummer Jan 23, 2024 •

edited

Loading

keyboardDrummer Jan 23, 2024 •

edited

Loading