From d7b17ea6d661f1fe426bfa3d9db3bf4ad8d749ad Mon Sep 17 00:00:00 2001 From: Alex Kunich Date: Sat, 3 Oct 2026 22:27:20 +0300 Subject: [PATCH] mcp: --root for relative paths; say when claims were not checked From live testing (Claude Desktop via WSL): - The server's working directory was C:\Windows\System32, so every relative model or claims path failed. `writ-mcp --root DIR` (or WRIT_MCP_ROOT) moves there before reading anything; command-line paths stay relative to where it was started, and a bad root is refused at startup. A missing relative path now names the working directory and the flag. The server writes nothing in its working directory, only temporary files. - With errors in both model and claims, only the model's were reported, and the claims looked clean until the next round trip. Claims and rules are typed against the model, so they are still not read, but writ_validate now says so: `note E_NOT_CHECKED in claims`. Co-Authored-By: Claude Opus 5.5 --- CHANGELOG.md | 6 ++++ docs/mcp.md | 12 +++++-- tests/unit/test_mcp_authoring.ml | 28 +++++++++++++++++ tooling/mcp/bin/writ_mcp.ml | 54 ++++++++++++++++++++++++++------ tooling/mcp/lib/diagnose.ml | 17 +++++++++- tooling/mcp/lib/tools.ml | 41 +++++++++++++++++++++--- 6 files changed, 141 insertions(+), 17 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 8902ed7..b606452 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -12,6 +12,12 @@ half-way no longer look alike. **MCP, from live testing:** +- `writ-mcp --root DIR` (or `WRIT_MCP_ROOT`) sets the directory relative + paths resolve against; a client may start the server anywhere, Claude + Desktop through WSL in `C:\Windows\System32`. A missing relative path now + names the working directory and the flag. +- While the model has errors, `writ_validate` says the claims and rules were + not checked (`note E_NOT_CHECKED`), instead of leaving them looking clean. - `writ_validate` reports every error it can find, one per top-level form (up to 20), not only the first; a syntax error still stops the file. - A missing `model`, `claims` or `rules` path is `E_FILE_NOT_FOUND` in the diff --git a/docs/mcp.md b/docs/mcp.md index 402e394..b3e9ee8 100644 --- a/docs/mcp.md +++ b/docs/mcp.md @@ -63,9 +63,16 @@ use a writ installed on your machine instead of Docker, set `WRIT_MCP_NATIVE=1`. `make install-writ`): ```json -{ "mcpServers": { "writ": { "command": "writ-mcp" } } } +{ "mcpServers": { "writ": { "command": "writ-mcp", + "args": ["--root", "/path/to/project"] } } } ``` +`--root` (or `WRIT_MCP_ROOT`) is the directory relative `model`, `claims` and +`rules` paths resolve against. Without it they resolve against wherever the +client started the server; Claude Desktop through WSL starts it in +`C:\Windows\System32`. The server writes nothing there either way: it reads +models, and its only files are temporary ones. + **Any other MCP client, with only Docker:** ```json @@ -156,7 +163,8 @@ would answer `n/a`, is an error in `writ_validate`, and `writ_check` adds a `why n/a` line naming it. `writ_validate` reports every error it can find in a file, one per top-level -form, up to 20: after a name or type error it leaves that form out and reads +form, up to 20. While the model has errors, the claims and rules are not read +(they are typed against it), and a `note E_NOT_CHECKED` says so: after a name or type error it leaves that form out and reads the file again. A syntax error, or one in the schema or instance, stops there. A path argument that names no file is `E_FILE_NOT_FOUND`, with the path it resolved to; `E_LOAD` is kept for a `(load …)` form. diff --git a/tests/unit/test_mcp_authoring.ml b/tests/unit/test_mcp_authoring.ml index 8fc6bcb..4735ea0 100644 --- a/tests/unit/test_mcp_authoring.ml +++ b/tests/unit/test_mcp_authoring.ml @@ -907,6 +907,34 @@ let () = check "compare: no laws reads `equations: none`" (contains ~sub:"equations: none" out) +(* ── claims not checked while the model is broken, and said so ─────────── *) + +let () = + let broken = + Writ_mcp.Diagnose.replace base + [ ("(set a.stage running)", "(set a.stage runing)") ] + in + let err, out = + tool "writ_validate" + [ + ("model_source", s broken); + ("claims_source", s "(property p \"x\" (possible (is a.stage don)))"); + ("rules_source", s "(relation r 1)"); + ] + in + check "broken model: its error is reported" + (err && contains ~sub:"error E_UNKNOWN_VALUE in model" out); + check "broken model: claims are said to be not checked" + (contains ~sub:"note E_NOT_CHECKED in claims" out); + check "broken model: so are rules" + (contains ~sub:"note E_NOT_CHECKED in rules" out); + let _, out = tool "writ_validate" [ ("model_source", s broken) ] in + check "broken model alone: no note" (not (contains ~sub:"E_NOT_CHECKED" out)); + let _, out = tool "writ_check" [ ("model", s "rel/x.writ") ] in + check "relative missing path: names the working directory and --root" + (contains ~sub:"resolves against the server's working directory" out + && contains ~sub:"--root" out) + (* ── a bare (set …) outside (do …) is an error, not a silent no-op ───────── *) let () = diff --git a/tooling/mcp/bin/writ_mcp.ml b/tooling/mcp/bin/writ_mcp.ml index a6db276..4cf1088 100644 --- a/tooling/mcp/bin/writ_mcp.ml +++ b/tooling/mcp/bin/writ_mcp.ml @@ -61,16 +61,50 @@ let resolve_for (base : string) : Writ_syntax.Loader.resolve = in first (Load_path.candidates ~base name) -(* `writ-mcp [--claims-dir DIR]`. With DIR, every claims file is read from - there by basename, whatever path a tool call names, so the agent editing the - model cannot also edit its questions. *) -let pinned = - match Array.to_list Sys.argv with - | [ _ ] -> None - | [ _; "--claims-dir"; dir ] -> Some dir - | _ -> - prerr_endline "usage: writ-mcp [--claims-dir DIR]"; - exit 2 +(* `writ-mcp [--claims-dir DIR] [--root DIR]`. + + --claims-dir: every claims file is read from DIR by basename, whatever path + a tool call names, so the agent editing the model cannot also edit its + questions. + + --root (or $WRIT_MCP_ROOT): the directory relative paths resolve against. + A client may start the server anywhere — Claude Desktop through WSL starts + it in C:\Windows\System32 — so the server moves there before it reads a + line. Paths given on the command line are taken relative to where it was + started. *) +let usage () = + prerr_endline "usage: writ-mcp [--claims-dir DIR] [--root DIR]"; + exit 2 + +let absolute d = + if Filename.is_relative d then Filename.concat (Sys.getcwd ()) d else d + +let pinned, root = + let rec go pinned root = function + | [] -> (pinned, root) + | "--claims-dir" :: d :: rest -> go (Some (absolute d)) root rest + | "--root" :: d :: rest -> go pinned (Some (absolute d)) rest + | _ -> usage () + in + let pinned, root = go None None (List.tl (Array.to_list Sys.argv)) in + let root = + match root with + | Some _ -> root + | None -> ( + match Sys.getenv_opt "WRIT_MCP_ROOT" with + | Some d when d <> "" -> Some (absolute d) + | _ -> None) + in + (pinned, root) + +let () = + Option.iter + (fun d -> + try Sys.chdir d + with Sys_error e -> + prerr_endline ("writ-mcp: --root: " ^ e); + exit 2) + root (* One line in, at most one line out; a line that is not JSON gets a JSON-RPC parse error rather than silence. *) diff --git a/tooling/mcp/lib/diagnose.ml b/tooling/mcp/lib/diagnose.ml index 6c0b917..95cb0ed 100644 --- a/tooling/mcp/lib/diagnose.ml +++ b/tooling/mcp/lib/diagnose.ml @@ -369,6 +369,18 @@ let codes : entry list = wrong = Call "writ_check({model: \"probe-does-not-exist.writ\"})"; right = Call "writ_check({model_source: \"(schema …) …\"})"; }; + { + code = "E_NOT_CHECKED"; + cause = + "Claims and rules are typed against the model, so while the model has \ + errors they are not read at all. This is not a verdict on them."; + hint = + "Fix the model's errors, then validate again: the claims are checked \ + then."; + wrong = + Call "writ_validate({model_source: , claims_source: …})"; + right = Call "writ_validate({model_source: , claims_source: …})"; + }; { code = "E_NO_SITUATION"; cause = @@ -963,7 +975,10 @@ let to_text (d : t) = | _ -> "" in Buffer.add_string b - (Printf.sprintf "error %s in %s%s\n" d.code + (* Not checked is not an error in the file; it says why there is none. *) + (Printf.sprintf "%s %s in %s%s\n" + (if d.code = "E_NOT_CHECKED" then "note" else "error") + d.code (Fault.source_name d.source) (if where = "" then "" else " at " ^ where)); Buffer.add_string b (" " ^ d.message ^ "\n"); diff --git a/tooling/mcp/lib/tools.ml b/tooling/mcp/lib/tools.ml index c0076ce..ecde080 100644 --- a/tooling/mcp/lib/tools.ml +++ b/tooling/mcp/lib/tools.ml @@ -34,8 +34,14 @@ let exists ~arg resolve path = { Errors.pos = None; msg = - arg ^ ": " ^ path ^ " not found (resolved to " ^ absolute path - ^ ")"; + (arg ^ ": " ^ path ^ " not found (resolved to " ^ absolute path + ^ ")" + ^ + if Filename.is_relative path then + "; a relative path resolves against the server's working \ + directory, " ^ Sys.getcwd () + ^ ", which writ-mcp --root DIR (or WRIT_MCP_ROOT) sets" + else ""); }) let load ?(arg = "model") resolve path = @@ -747,10 +753,37 @@ let collect ~resolve ~path read = let validate ?(json = false) ?(pinned = None) ~resolve ~model ~claims ~rules () = - let* m = collect ~resolve ~path:model (fun r -> load r model) in + (* Claims and rules are typed against the model, so a broken model leaves + them unread: say so, or a client takes them for clean. *) + let skipped (f : Fault.failure) = + let not_checked source what path = + { + Fault.source; + code = Some "E_NOT_CHECKED"; + err = + { + Errors.pos = None; + msg = + what ^ " " ^ path + ^ ": not checked — it is typed against the model, which has \ + errors"; + }; + meant = None; + } + in + let extra = + Option.to_list (Option.map (not_checked Fault.Claims "claims") claims) + @ Option.to_list (Option.map (not_checked Fault.Rules "rules") rules) + in + match f with Fault.Bad fs -> Fault.Bad (fs @ extra) | l -> l + in + let* m = + collect ~resolve ~path:model (fun r -> load r model) + |> Result.map_error skipped + in let* ctx, _ = State.build_ctx m.Model.schema m.Model.initial - |> Result.map_error (model_fault model) + |> Result.map_error (fun e -> skipped (model_fault model e)) in let claims = Option.map (pin ~pinned) claims in let cl =