Goals are not displayed

[arnaudgolfouse]

Since updating to 2.1.3, I cannot get the goals panel to appear anymore. Using the Coq: Display Goals command results in an error popup saying "command 'extension.coq.displayGoals' not found".

I am using VsCodium on linux.

Versions:

• vscoq-language-server: 2.1.3
• coq: 8.18.0
• vscodium: 1.90.2

[arnaudgolfouse]

Switching the extension and vscoq-language-server to 2.1.2 fixes the issue

[rtetley]

Hi, from your message it is unclear to me if the goals ever display or if it is just the Coq: Display Goals command that does not exist ? If it is the former, I cannot reproduce (at least on vscode) I will try on vscodium when I get a chance. If it is the latter, we removed that command a while back. I should remove it from the package.json. Do you believe it has a use case ?

[arnaudgolfouse]

It's the former, I cannot see the goals at all. I tried Coq: Display Goals in an effort to make them reappear. I tested it on (a fresh install of) vscode, and got the exact same behavior: cannot display goals on 2.1.3, but it works fine on 2.1.2.

[arnaudgolfouse]

I just tested it on a fresh VM (Fedora 40, Gnome), everything is the same for me.

[arxgy]

I'm having the same problem.

[rtetley]

Does the goal window never open ? Or does it open but its empty ? Do you have an example file I could try ?

[arxgy]

The former case. And it doesn't work for any coq project.

[rtetley]

I just tested it on MacOS with vscodium 1.90.2. It works fine with v2.1.3 and v2.1.4. I'll try and get access to an Ubuntu machine and test it there. In the meantime can one of you check if the problem still occurs on v2.1.4 ?

[gares]

I don't have the exact setup, but it works fine with vscoq 2.1.3 on Coq 8.19 and codium 1.89 on Ubuntu 22.04 (codium 1.90 does not even start on my machine).

[rtetley]

Just re-tested on mac with Coq 8.18 and it also works fine (the previous test was with Coq 8.19)

[arnaudgolfouse]

So I tested it on virtual machines, freshly installed, and the behaviour happens each time: I install vscoq, it does not work. But if I downgrade both the extension and the package vscoq-language-server to 2.1.2, it works.

It does not work whether the extension's version is 2.1.3 or 2.1.4. vscoq-language-server (the opam package) only exists in the 2.1.3 version.

I confirm that in the 'bad' version, the goals panel does not appear at all.

I tested it on:

• Ubuntu 22.04, vscode 1.91.0 installed via snap
• Debian 12.6, vscode 1.91.0 installed via deb

Each time with the system's opam (aka installed via apt install opam), and coq pinned to 8.18.0.

The proofs also seems to not be checked (as in a typo in an hypothesis' name does not display the usual red squiggly line)

[rtetley]

Could you send me the logs from the language server when testing ? In the user settings, go to Vscoq: Args and in the json add the following option:

"vscoq.args": [
        "-vscoq-d", 
        "all",
    ],

Then in the outputs panel you'll find the logs in Coq Language Server. Thanks !

[arnaudgolfouse]

Here are logs for what I tried, with a recording of what I did in the editor:

• with 2.1.4: (same for 2.1.3) With 2.1.4.webm

  log for "Coq Language Server" : Coq Language Server log 2.1.4.txt

• with 2.1.2: With 2.1.2.webm

  log for "Coq Language Server" : Coq Language Server log 2.1.2.txt

[rtetley]

I think I just figured it out. This is due to a change that was requested internally. See here: https://github.com/coq-community/vscoq/pull/788

Basically you are now in manual mode by default so you need to navigate your proof by using stepForward, stepBackward, or interpretToPoint. If you want to go back to the previous mode, you just need to revert the setting to Continuous. See here.

I should have advertised the change more clearly in the release announcement ! Can you check and confirm that this was the problem ?

[arnaudgolfouse]

Yes, this is it! Thank you 🥳