Add a batch runAt API for source-position probe batches

Summary

Please consider adding a batch runAt MCP API for agent workflows.

The current API is useful, but it has high interaction overhead when an agent needs to ask several small, source-position-attached questions against the same saved file snapshot. This comes up constantly in Lean porting/debugging work.

Concrete use case

In the Liris 4.31 port, the active blocker is a proofmode/package-key issue. The useful probes are small and related:

• test a candidate helper theorem
• test the corresponding instance head
• #check the exact generated target
• test whether the consumer theorem application elaborates
• inspect one or two alternative transparency modes

Each probe should run at the same file/position/root, against the same saved snapshot. Today this requires several independent MCP calls. Multi-command lean_run_at also currently rejects command sequences, so it does not cover this use case.

Suggested API shape

One possible shape:

{
  "tool": "lean_run_at_batch",
  "arguments": {
    "path": "Liris/Iris/HeapLang/Lib/SpinLock.lean",
    "line": 418,
    "character": 2,
    "mode": "independent",
    "stopOnFirstError": false,
    "items": [
      { "id": "check-target", "text": "#check someTarget" },
      { "id": "candidate-helper", "text": "example : ... := by ..." },
      { "id": "candidate-instance", "text": "#synth SomeClass ..." }
    ]
  }
}

Return per item:

{
  "id": "candidate-helper",
  "success": false,
  "messages": [],
  "diagnostics": [],
  "proof_state": null,
  "next_handle": null
}

Modes that would be useful

• independent: each item sees only the saved file snapshot
• sequence: item N+1 sees item N, explicitly requested
• stopOnFirstError: useful for sequence mode
• runAll: useful for independent exploration

Why this matters

Batching would reduce round trips without encouraging detached scratch files. It keeps the agent cost model aligned with Beam: many small source-context probes, all attached to the real module, rather than reconstructing partial contexts elsewhere.

I would prioritize batch runAt over batch sync; sync should first have rock-solid readiness/error semantics.

Start by reading the existing lean_run_at MCP API and its handling of command sequences. Trace the tool entry point and related tests, if present, before deciding where batch behavior belongs. Done means a batch runAt tool supports the requested independent and sequence modes and returns per-item results with the described controls.