Remove VSCode LLM languageTools `SANYTool.ts` and `TLCTool.ts` in favor of MCP

[lemmy]

[...] we should consider removing https://github.com/tlaplus/vscode-tlaplus/blob/master/src/lm/SANYTool.ts and https://github.com/tlaplus/vscode-tlaplus/blob/master/src/lm/TLCTool.ts, given that MCP has won the race.

Originally posted by @lemmy in #467 (comment)

[lemmy]

Written by @younes-io at #467 (comment):

I am not convinced MCP "won" the race. It is still inconsistent in tool calling and instruction following; also, it's very token-hungry. People are already trying to figure out more reliable alternatives.

I think MCP (at least in this context) serves the people who want to use TLA+ through this protocol in whatever AI agent they use (or maybe even their own). However, SANYTool and TLCTool are useful for the Copilot/VS Code chat audience. If we remove those, we orphan that audience. Maybe, we keep both for now and revisit later, when new alternatives show up or status quo improves.

[lemmy]

I'm getting suspicious that there may not be any actual users, considering no one has spoken up even though SANYTool and TLCTool are clearly behind MCPServer in functionality.

[lemmy]

I'm getting suspicious that there may not be any actual users, considering no one has spoken up even though SANYTool and TLCTool are clearly behind MCPServer in functionality.

@zfhuang99's https://github.com/zfhuang99/lamport-agent/blob/a0e1e2f77099be929e5461ca01fff4ea45c2d12a/prompts/Lamport.chatmode.md?plain=1#L3 uses our VSCode language tools. @zfhuang99, is there a reason you’re not using the MCP server instead? According to the VSCode documentation, you should be able to reference an MCP via <server name>/.

[younes-io]

I think we're conflicting two things:

• the tools: which represent the capabilities
• MCP: which is the transport layer

I don't think the adoption rate of MCP vs. tools should define our decision on this, because:

• tools should be treated as first-class citizens, for so many reasons; if we remove them, then we force consumers to use tools from MCP only, and they cannot use them natively; this native usage of tools is supported by most agentic libraries:
  • Langchain: https://docs.langchain.com/oss/javascript/langchain/tools#tools
  • LlamaIndex: https://developers.llamaindex.ai/typescript/framework/modules/agents/tool
  • Vercel SDK also supports native tool calling: https://vercel.com/academy/ai-sdk/tool-use
• LM tools avoid server/port lifecycle and are lower-latency

These API/SDK "providers" treat MCP as an additional transport for reusable tools, not a replacement for native tooling.

Bottomline, imho: if we remove these tools, the TLA+ extension needlessly bind consumers to one I/O path

[lemmy]

Related: #472

[younes-io]

Example of another extension that exposes its tools as first class citizens and provide consumers with the possibility to keep in the context only a subset of the tools (for whatever reason, less tokens, granularity, etc):

[younes-io]

@lemmy : could you please elaborate more about the reasons why we should remove these tools?

[lemmy]

Our extension includes TLA+ commands such as “TLA+: Check Model with TLC.” These are designed for humans to invoke. I initially assumed that IDEs would allow LLMs to call those existing commands directly. However, the VSCode team noted that these commands need proper, machine-readable descriptions before they can be used by LLMs (though I’d argue we could have simply amended the descriptions of the existing tools).

This requirement led to a VSCode–specific solution: LLMLanguageTools. Our VSCode extension now exposes several of its TLA+ commands through this API as Language Model Tools.

Later, MCP emerged—another API through which we can expose the same TLA+ commands. MCP is more widely supported compared to the "proprietary" Language Model Tools. Specifically, it is supported by VSCode and Cursor.

I propose to discontinue and remove the VSCode LLMLangaugeTools tools.

Related:

• Tools API for your Copilot Extensions microsoft/vscode-discussions#2411 (comment)
• Tools API for your Copilot Extensions microsoft/vscode-discussions#2411 (comment)

[younes-io]

@lemmy : okay, thanks for sharing the context/history. Then, my question would be, when we drop the SANYTool/TLCTool, external function calls will remain in MCP only; so for non-HTTP pipelines, do you intend to expose a library API?

[lemmy]

At this time, I don’t intend to expose a library API, mainly because I don’t have a clear picture of the non-HTTP pipelines you’re aiming to support. If your intent is to expose our tools to LLMs independently of MCP, VSCode’s proprietary LLMLanguageTools API doesn’t appear to be an good fit given its limited support.