# Bug report: stale/duplicate document nodes; edits stop propagating; loads never
  finish

  **Versions:** isabelle-pide-mcp commit `90e56bb` (2026-07-06); Isabelle dev snapshot
  `c13a4bd3c018`; Linux x86_64, 8 cores / 15 GB.
  **Launch:** `pide_mcp -v -l HOL-Library -d <project dir>` (project session of ~16
  theories based on HOL-Library). Long-lived session with frequent incremental edits.

  ## Session shape before onset (possibly relevant triggers)

  - Several full dependency-chain invalidations in quick succession (edits to theories
    near the root of a ~16-theory import chain), including one theory that
  source-loads
    `HOL-Combinatorics.Permutations` (cross-session import, base heap is HOL-Library).
  - Scratch files (via `create_scratch`) importing session-qualified project theories.
  - One earlier scratch was given a nonexistent import (`HOL-Library.Permutations`).
    After that, EVERY MCP operation on that scratch (`read`, corrective `edit`)
    failed with the import error, so it could not be repaired through the MCP; I had
    to fix the file on disk externally, after which it recovered.
  - Two long-running/diverging tactics were cancelled by edits mid-execution.

  ## Symptom 1: file-path node vs session-qualified node diverge; path node frozen

  Theory `A.thy` belongs to the loaded session and is imported by `B.thy`.
  After a sequence of `edit` calls using the **absolute file path** as `origin`:

  - `get_state(origin = /abs/path/A.thy)`: the tail from the last edit point
    (~510 of 898 commands) permanently `unprocessed` (all 0 ms),
    `commands_finished` frozen at 388, `total_timing_ms` frozen at the same value
    across 4 polls spanning ~10 minutes. No errors, nothing still-running.
    Indistinguishable from a wedged scheduler.
  - `get_state(origin = Session.A)` at the same time: all **898 commands
    finished, 0 errors**.
  - Corroboration: `get_state` on the importer `B.thy` showed it fully processed —
    so `A` really had been checked; only the path node's status was stale.
  - The stale path node listed the **post-edit source text** in its commands, i.e.
    it is not an old snapshot — it is a duplicate node whose execution status
    never updates. Presumably path-origin access creates a second document node
    alongside the session-resolved one, and only one is attached to execution.

  ## Symptom 2 (later, same session): edits ack but never reach the document model;
  new loads hang

  Theory `C.thy` (member of the session, not loaded at that moment). Three `edit`
  calls (path origin) each returned `{"status":"written"}` and verifiably changed
  the file on disk.

  - `get_state` on **both** the path origin and `Session.C` kept returning the
    pre-edit version; a range request even failed with "start_line 115 out of
    bounds (file has 103 lines)" — the OLD length — while the disk file had ~140
    lines. A further forcing `edit` also returned "written" with no observable
    effect on the reported state (not even the line count).
  - Inconsistently, `read` on the same path origin DID return the new disk
    content. So `read`, `edit` acknowledgement, and `get_state` were reflecting
    different views of the file.
  - A fresh scratch importing `Session.C` then hung in
    "queued for loading … not ready yet" indefinitely (many minutes, many polls).

  Batch `isabelle build` of the session from disk succeeded at that point, so the
  theories themselves were fine; the failure is in the server's document/version
  management. `ps` showed a single healthy poly process (busy during real
  rechecking, otherwise idle) — no runaway or orphaned processes.

  ## Expected behavior

  - One canonical document node per theory regardless of whether it is addressed
    by file path or session-qualified name (or at least status coherence between
    the two).
  - `edit` acknowledgements should imply the change is visible to subsequent
    `get_state`/loads.
  - A theory queued for loading should eventually load or report an error, not
    hang silently.

  ## Workaround used / severity

  Only reliable recovery was restarting the server. Severity: high for long
  interactive sessions — Symptom 1 mimics a wedge (inviting unnecessary
  restarts), Symptom 2 silently desynchronizes state and invalidates all
  subsequent interactive feedback.

  One judgment call on my part worth knowing about: the claim in Symptom 1 that
  path-origin access creates the duplicate node is my inference, not something I
  verified — the maintainer may want it phrased as observed behavior only (the
  paragraph already hedges with "presumably").