Critical bug - cannot step forward / backwards (version 2.2.3)

[nirshahar]

Hi, as of the latest (2.2.3) version, I encountered a bug where stepping forward / backwards doesn't do anything.
I have tried the keyboard shortcut, as well as using the UI buttons.

Its important to note that "interpret to point" (Alt+right) does work, but its insanely frustrating to not be able to do a single step-forward.

I opened the log output to verify, and indeed - pressing on "interpret to point" adds the following logs:

[GoalPanel] Received proofview notification
[GoalPanel] Created new goal panel

While pressing on step-forward or step-backwards does not print anything at all.

I suspect the issue is only in the new version because downgrading to 2.2.1 fixed the issue for me.

[TheoWinterhalter]

Did you update both the server and the extension because I don't have this problem.

[nirshahar]

The extension auto-updated by vscode, so probably the server didn't automatically update?
Seems like updating it does solve the problem.

In any case, doesn't it seem weird that an auto-update will only update the client and not the server, while having breaking changes?
Is there an option to add an automatic update to the language-server that the client will attempt to do?
For example, by showing a popup to the user with something like
"we have detected you are running an old vscoq-language-server of version x.y.z, while the extension's client runs at x'.y'.z' > x.y.z
do you want to proceed by updating vscoq-language-server? Note that not updating it might cause considerable bugs and issues"

[TheoWinterhalter]

The server never auto-updates indeed.

I guess it should warn if the server and extensions are incompatible, and probably it does, but this wasn't noticed to be incompatible before?

[nirshahar]

No, it didn't figure out it was incompatible before. I think my server was running 2.2.1 because I installed it only recently, so thats expected.

[rtetley]

You should have seen this warning

[nirshahar]

Wasn't shown :/
Not even after a restart, thats why I was really confused and opened this issue in the first place...

Maybe a bug when showing the popup?

[ybertot]

I experienced a similar problem, even though I had anticipated:

• I first updated my opam setting to make sure I had vscoq-language-server 2.2.3
• I then restarted my code process (finished the previous one by using the exit button from the file menu).
• When in the new instance of code, I clicked on the extensions, and relevant option (I don't remember the name, and it is not shown anymore).
• then everything was fine, apparently, no complaints of a mismatch between the Coq extension and the vscoq-language-server, but there was no reaction when I used the keyboard shortcuts or the arrows (even for execute-to-point).

Starting from here, it is relevant to say that I am working on a Linux machine (Fedora). I stopped the code process again (using the exit option from the File menu). I moved away the directory ~/.config/Code to a different location, and restarted the code process. It showed it knew about the coq extension (so the information must be stored somewhere else than in ~/.config/Code), but that it did not I already trusted the authors in the given directory. After saying I trusted the authors, I was able to have an acceptable behavior.

After that, I stopped my session of code moved the old version of ~/.config/Code back in place, and restarted code. Now the behavior seems to be back to normal. Weird!