Avoid mutating user files when running PlusCal/SANY and keep diagnostics mapped

[younes-io]

PlusCal transpilation and SANY parsing (LM tool and MCP server paths) now execute on temporary copies, remapping diagnostics to the original files so user workspace files remain unchanged.

---

• PlusCal transpilation now accepts an override path so diagnostics point to the original file
• Both LM ParseModule tool and MCP SANY flow work on temporary copies, copying local .tla modules, remapping diagnostics back, and cleaning up after themselves
• Added a regression test to confirm the temp-copy behavior and that original files stay untouched

[lemmy]

Why don't we want the AI to be able to mutate the files?

[younes-io]

Why don't we want the AI to be able to mutate the files?

Before this PR, the LM/MCP path called transpilePlusCal directly on the user’s .tla, and the PlusCal translator writes in-place. That means an AI-invoked tool (no explicit user action) could modify workspace files just to parse, which is an unexpected side effect. This PR keeps AI calls read-only by working on a temp copy (see ParseModuleTool and MCPServer changes) and remaps diagnostics so the user still sees paths to their original files. The new regression test in tests/suite/lm/sanyTool.test.ts asserts the original file stays untouched while diagnostics reference it

[lemmy]

Isn’t this bypassing the agent-chat mode that’s designed to track all LLM-driven changes? If the user wants to accept the synthesized changes, how is she supposed to apply them?

[younes-io]

This is not bypassing anything. This PR only makes the LM/MCP parse tool read-only. If users want AI-suggested edits, those should go through agent-chat so changes stay explicit and tracked.

[younes-io]

as tools will be removed, let's close this, and re-assess in the future