No typechecking when saving twice

[v-moreau]

Dear maintainers,

I am a bit confused regarding vscode-rzk as it seems that, in an ill-typed file, saving once does typecheck and shows the errors whereas saving another time will make the errors disappear. This behavior appears whether or not the file has been changed between the two saves.

For instance, I have a minimal file test.rzk whose content is

#lang rzk-1

#def weird (A : U)
  : A
  := \ x → x

together with a rzk.yaml file in the same directory containing

include:
  - 'test.rzk'

When I save the file once, vscode-rzk underlines the definition of weird with some red as follows:

When I put the mouse on it, I get the typechecking error:

However, when I save the file another time, then the error is gone:

I have tried with a new vscode profile whose sole installed extension is vscode-rzk, but I have the same behavior. Is there something wrong on my side, or is it supposed to be how the vscode-rzk extension works? For the moment, I thus prefer to use the rzk typecheck command in a terminal window to check my file, as I don't see the errors with the vscode extension.

[fizruk]

Thanks for the bug report! This is definitely not intended.

I think this has to do with the incorrect caching of the type errors in the Rzk Language Server, which should hopefully be fixed when we merge this PR: rzk-lang/rzk#167

We'll try to reproduce, fix, and release an update sometime this week.

[fizruk]

I believe what's happened is on the second save the diagnostics were cleaned, but since nothing changed, we should've preserved the diagnostics (or restored them). I have a very simple fix (rzk-lang/rzk#172) that seems to be working locally for me, the problem should go away with the next release of Rzk (hopefully very soon).

[fizruk]

@v-moreau I have just released rzk v0.7.4 that contains the fix to the language server, which should fix this issue for you (reload VS Code so that it prompts you to update Rzk). Please let me know if you experience any further issues!

[v-moreau]

Indeed, the bug is now gone on my side too. Thank you very much!