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?