MCP: --root for relative paths; say when claims were not checked

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

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.

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 () =

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. *)

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: <with errors>, claims_source: …})";
+      right = Call "writ_validate({model_source: <valid>, 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");

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 =