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 =