Skip to content

Conversation

@Maverick618
Copy link

When the VS Code extension and opam-installed vsrocq-language-server are on different versions, the language server may fail during initialization. This can cause commands like "Interpret to point" to silently do nothing(I just ran into this problem).

This PR clarifies the README by:

  • Adding a "Version check" note recommending to keep extension and vsrocq-language-server versions aligned
  • Showing how to install a specific language server version (e.g. vsrocq-language-server.2.3.4)
  • Clarifying Rocq 9.x vs Coq 8.x package names (rocq-core vs coq-core)
  • Noting that pre-release pins should also have matching extension versions

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant