Compilation events #4732

keyboardDrummer · 2023-11-01T17:45:18Z

Description

Updates

CompilationManager.CompilationUpdates is renamed to Updates, and its type has been changed from Observable<Compilation> to IObservable<ICompilationEvent>. This means that the updates are now deltas that describe how the state of compilation has changed, instead of describing the full state of compilation. The full state of the compilation can still be queried through CompilationManager.Program and CompilationManager.Resolution, so the interface is strictly more powerful now.

Having a stream of deltas available in the interface is important for being able to use it for the CLI, since the CLI wants to immediately print diagnostics as they're found, which CompilationManager couldn't handle well without this change.

Gutter icons

All processing of gutter related data is now done based on CompilationManager.CompilationUpdates, instead of inside CompilationManager, which makes it possible to use CompilationManager for the CLI without computing gutter icons. This happens to also fix #4656 for which a test was added.

Renames

Rename Compilation to CompilationInput, CompilationManager to Compilation,
Rename CompilationAfterResolution to Resolution, remove its inheritance, move the mutable fields to CompilationManager and change it into a record

How has this been tested?

Most of it is a refactoring, but also added the test GitIssue4656GutterIconsResolutionError

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

…ion Manager

…into compilationEvents

MikaelMayer

Well done! It seems that the codebase is more maintainable with these refactorings, immutable records, renamings. A few suggestions and questions

MikaelMayer · 2023-11-03T14:21:32Z

Source/DafnyLanguageServer/Language/IProgramVerifier.cs

 Task<IReadOnlyList<IImplementationTask>> GetVerificationTasksAsync(ExecutionEngine engine,
- CompilationAfterResolution compilation,
+ Resolution resolution,


I felt a bit weird about "Compilation" to describe an object, but now I feel a bit weirder about "Resolution", since Resolution is a process. I would have named it rather "Resolver", "ResolverOutput", "ResolutionOutput" depending on the meaning

Source/DafnyLanguageServer/Util/PathExtensions.cs

MikaelMayer · 2023-11-07T21:03:15Z

Source/DafnyLanguageServer.Test/Diagnostics/PublishedVerificationStatus.cs

+ NotificationPublisher.Combine(PublishedVerificationStatus.Stale, PublishedVerificationStatus.Queued));
+ Assert.Equal(PublishedVerificationStatus.Stale,
+ NotificationPublisher.Combine(PublishedVerificationStatus.Stale, PublishedVerificationStatus.Error));
+ Assert.Equal(PublishedVerificationStatus.Running,


How much did you weight this one against PublishedVerificationStatus.Error? I understand why it's running, but for example in the gutter icons, errors prevail above everything, including running.

I considered it. I think both have downsides:

If you show running, then someone who's only watching the status bar to see whether errors are found, will wait longer than they have too.

If you show error, then someone might be surprised when new errors appear after it already went from running to error.

I think it's a bit scary if the IDE is consuming resources through verification, and not indicating this. A user might think there's a bug or wonder why the IDE is lying to them, so I prefer to show running.

MikaelMayer · 2023-11-07T21:09:07Z

Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs


- var state = await projectManager.GetIdeStateAfterVerificationAsync();
+ var state = await projectManager.States.Select(s => s.Value).Where(s =>
+ s.Status == CompilationStatus.ResolutionSucceeded &&


I feel like this could be written

s.EverythingFinished() // needs to be refactored.

what do you think?

Not sure what you mean but I extracted some code into a method to make it more clear what it does.

MikaelMayer · 2023-11-07T21:11:09Z

Source/DafnyLanguageServer/Language/DafnyProgramVerifier.cs

@@ -28,21 +28,20 @@ public class DafnyProgramVerifier : IProgramVerifier {
 }

 public async Task<IReadOnlyList<IImplementationTask>> GetVerificationTasksAsync(ExecutionEngine boogieEngine,
- CompilationAfterResolution compilation,
+ Resolution resolution,


I'm a bit hesitant about the "Resolution" name. Resolution is a process, while class names are usually objects.
What about:

ResolutionOutput

ResolutionResult

ResolutionOutcome
?

MikaelMayer · 2023-11-07T21:18:13Z

Source/DafnyLanguageServer/Workspace/Compilation.cs

+ // When multiple calls to VerifyUnverifiedSymbol are made, the order in which they pass this await matches the call order.
+ await ticket;
+
+ if (!onlyPrepareVerificationForGutterTests) {


Switch condition to reduce nesting.

I don't see how it's possible to reduce nesting here by inverting, but I'll extract something to a separate method.

I was thinking of

if (onlyPrepareVerificationForGutterTests) { DecrementJobs(); return; } <previously indented cod> DecrementJobs();

but refactoring is a good idea as well.

MikaelMayer · 2023-11-07T21:19:45Z

Source/DafnyLanguageServer/Workspace/Compilation.cs

+ }
+ // TODO: https://github.com/dafny-lang/dafny/issues/3415
+ return new TextEditContainer(new TextEdit[] {
+ // TODO end position doesn't take into account trailing trivia


Move this comment up with the other TODO

MikaelMayer · 2023-11-07T21:21:40Z

Source/DafnyLanguageServer/Workspace/FinishedResolution.cs

+ Status = status,
+ ResolvedProgram = ResolvedProgram,
+ SymbolTable = SymbolTable
+ ?? previousState.SymbolTable, // TODO migration seems missing


TODO: Can you please create an issue and link the issue to that todo, or fix it?

Source/DafnyLanguageServer/Workspace/NotificationPublisher.cs

Source/DafnyLanguageServer/Workspace/Notifications/VerificationDiagnosticsParams.cs

…into compilationEvents

MikaelMayer

Thanks for taking my comments into account, it looks better. Two optional small improvements

MikaelMayer · 2023-11-13T20:37:14Z

Source/DafnyLanguageServer/Workspace/Compilation.cs

+
+ private void StatusUpdateHandlerFinally() {
+ try {
+ var remainingJobs = Interlocked.Decrement(ref runningVerificationJobs);


A statement not expected to create an exception should generally not be in the try portion of a try catch statement if possible.

I have removed this method in a branch I will publish after this PR is merged

MikaelMayer · 2023-11-13T20:38:42Z

Source/DafnyLanguageServer/Workspace/ProjectManager.cs

@@ -290,18 +290,18 @@ public class ProjectManager : IDisposable {
 compilation.IncrementJobs();
 var resolution = await compilation.Resolution;

- var verifiables = resolution.CanVerifies?.ToList();
- if (verifiables == null) {
+ var canVerifies = resolution.CanVerifies?.ToList();


Seem like a weird name after all. Did you mean "VerifiableDeclarations"?

That is what it means. CanVerifies is meant to the pural of CanVerify. Earlier I named these Verifiable and Verifiables. I'm OK with changing to VerifiableDeclarations although it is two words instead of one.

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

MikaelMayer reviewed Nov 7, 2023

View reviewed changes

keyboardDrummer added 3 commits November 8, 2023 19:28

Small refactoring

9c2915f

Renames

b8c881a

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

550f19f

keyboardDrummer requested a review from MikaelMayer November 9, 2023 11:55

keyboardDrummer added 3 commits November 9, 2023 17:28

Ran formatter

ee46d80

Improve CI logging

ebd672c

More logging

fff38b5

keyboardDrummer mentioned this pull request Nov 10, 2023

Symbol status fix #4765

Merged

keyboardDrummer added 13 commits November 10, 2023 14:10

Trace logging for counter examples

22099a7

More logging

2972108

Move logging so hopefully it triggers

678feeb

Add Uri check

195151e

Turn off logging

eb1025c

Merge branch 'master' into compilationEvents

ffa6943

Merge branch 'master' into compilationEvents

62516dc

Improve logging

96605b0

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

7e51582

…into compilationEvents

Fix counterexamples

5b33e43

Merge branch 'master' into compilationEvents

3346c33

Remove traces

3e3ad8b

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

c42adb2

…into compilationEvents

MikaelMayer approved these changes Nov 13, 2023

View reviewed changes

keyboardDrummer added 3 commits November 13, 2023 22:47

Merge branch 'master' into compilationEvents

d71e2b2

Merge branch 'master' into compilationEvents

770ddcd

Merge branch 'master' into compilationEvents

174b498

keyboardDrummer merged commit 843a4e8 into dafny-lang:master Nov 14, 2023
20 checks passed

keyboardDrummer deleted the compilationEvents branch November 14, 2023 11:08

keyboardDrummer restored the compilationEvents branch November 14, 2023 13:18

keyboardDrummer deleted the compilationEvents branch November 14, 2023 13:18

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Compilation events #4732

Compilation events #4732

keyboardDrummer commented Nov 1, 2023 •

edited

Loading

MikaelMayer left a comment

MikaelMayer Nov 3, 2023

MikaelMayer Nov 7, 2023

keyboardDrummer Nov 9, 2023 •

edited

Loading

MikaelMayer Nov 7, 2023

keyboardDrummer Nov 9, 2023

MikaelMayer Nov 7, 2023

MikaelMayer Nov 7, 2023

keyboardDrummer Nov 8, 2023

MikaelMayer Nov 8, 2023

MikaelMayer Nov 7, 2023

MikaelMayer Nov 7, 2023

MikaelMayer left a comment

MikaelMayer Nov 13, 2023

keyboardDrummer Nov 13, 2023

MikaelMayer Nov 13, 2023

keyboardDrummer Nov 13, 2023

Compilation events #4732

Compilation events #4732

Conversation

keyboardDrummer commented Nov 1, 2023 • edited Loading

Description

Updates

Gutter icons

Renames

How has this been tested?

MikaelMayer 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 Nov 9, 2023 • 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

MikaelMayer 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

keyboardDrummer commented Nov 1, 2023 •

edited

Loading

keyboardDrummer Nov 9, 2023 •

edited

Loading