Simple MCP server implementation based on vsrocq#1194
Conversation
|
Hello, many thanks for your contribution! I have a bunch of questions, but maybe it is easier to have a visio chat. If you agree it is a good idea, we can organize that via the Rocq zulip. |
KacperFKorban
force-pushed
the
vsrocqmcp
branch
4 times, most recently
from
3d10a81 to
c6c99d4
Compare
| "command": "vsrocqtop", | ||
| "args": [ | ||
| "-mcp", | ||
| "-coqlib", |
There was a problem hiding this comment.
I wonder why you need this option. Can't it read the _CoqProject file as vsrocq does?
There was a problem hiding this comment.
Yes, this should definitely be possible in some way. I had plans to separately simplify the initialization phase, but for now I just used the simplest option (not to bundle too many unrelated changes together).
The vscode extension code basically calls vsrocqtop twice, starting with -where.
vsrocq/client/src/utilities/toolchain.ts
Line 103 in 0ad9d19
|
thanks for rebasing |
|
Just FYI, I just realized that the new changes are still broken after the rebase, I'm looking into it. |
|
I'll merge #1046 and then rebase this one ontop, if it is OK for you |
|
Sounds great! Thanks! |
edit_line replaces entire lines (startLine to endLine, inclusive, 0-indexed), avoiding character offset errors that LLMs are prone to. apply_edit is kept for programmatic clients needing sub-line precision, with a warning in its description.
|
I'm so sorry I left this on the side for so long. But I did not forget about it. |
|
No problem at all! I just figured that it might be easiest for me to do the rebase. (I might've broken some CI jobs though. I'm looking into that now.) |
|
I did reorganize the sources so that we have two binaries sharing the document manager, i.e. the apis to check documents, cache states, etc. The two binaries speak via json rpc the LSP and MCP respectively. I'll look into the tools soon, but I wonder what are your thoughts about the approach of https://github.com/scidonia/rocq-piler by @GavinMendelGleason with whom I recently exchanged at the Iris WS. In particular I recall a discussion about LLM being confused by the column-line addressing approach. Rocq-piler seems to have a nicer approach to this. |
|
Thanks for doing the refactor! I don't have strong opinions about the tools. I definitely thought about implementing more "controlled" tools (in the style rocq-piler has now). But if the line addressing is a problem, one can always disable this one tool (interpretToPoint) and only use interpretToEnd/step*. One thing that I experimentally prefer in the current implementation is no edit tools– different models have very different ways to edit files (patches, sed, scripts. etc.). Also adding more tools adds a cost to the initial context window size. I think that my general approach is: once we have something that more people can use, we can iterate based on the feedback. And since it is an interface for an LLM we don't have to care about compatibility issues that much. |
|
The discussion about line-column addressing was either with you @KacperFKorban or with Guillaume about rocq-mcp, not with Gavin. (I feel like my message was not clear) |
3 participants
This PR adds a base implementation for an MCP server using vsrocq.
The MCP server is implemented as an alternative to the lsp server – passing
-mcpthvsrocqtopstarts an mcp server, instead of and lsp server. This way, the user and the LLM don't share the same vsrocqtop session, which should make it easier to delegate tasks.