Error highlighting state not updating correctly after fixes to code

[kevinsullivan]

I haven't ascertained all the details, but it's clear that in some cases, error indications (in the form of red squiggly underlines) in the IDE are not being updated properly when problems are fixed in code in other files. Even when the compiler runs successfully, error indicators sometimes remain. The one way I've found to clear them is to exit and restart the IDE.

[hardliner66]

I just had a similar problem. I think the plugin (or maybe dafny itself) doesn't correctly determine if the file has changed or not if you make a change inside a lambda.

Given the following code:

method DoStuff(f: (int) -> int) returns (result: int) ensures result == f(1) { return f(1); }
method NeedsGtZeroValue(i: int) requires i > 0 {}

method Main() {
  /* 1 */ var a := DoStuff(x => x);
  /* 2 */ var someVariable := 1;
  /* 3 */ NeedsGtZeroValue(a);
}

If you change x => x to x => x - 1 at line 1 in main, vscode should show a red underline at line 3, but doesn't. If you comment out line 2, vscode correctly updates and shows the red underline, even if you uncomment line 2 again.

If you fix the "bug" and change x => x - 1 back to x => x, the same thing happens, until you comment/uncomment (or change/add/delete) some other statement in your code.

Because it has a problem with lambdas, this problem also effects array creation with an initilizer lambda.

@kevinsullivan: So until it gets fixed, maybe you can try to create an unused dummy value to comment/uncomment to trigger the refresh in vscode. It's not a good workaround, but at least it's better than restarting vscode all the time.