mcp: structured JSON from eval/hol_load, output truncation, built-in timing

[sgmenda]

Reduces LLM context window bloat from the MCP server by making eval and hol_load return structured, truncated JSON instead of raw strings.

Motivation

During the AES-GCM formalization, I found that large outputs from eval and hol_load fill up the context window quickly---the S-box precomputation dumps ~15K chars, needs prints every intermediate val binding (~10K chars), and large let bindings print full values. All this noise leaves less room for actual reasoning.

Changes

eval returns structured JSON

{
  "success": true,
  "output": "val it : thm = |- 1 + 1 = 2",
  "output_truncated": false,
  "full_output_chars": 42,
  "time_seconds": 0.003
}

• max_output_chars parameter (default 4000, configurable per-call and in hol-mcp.toml)
• success field uses heuristic error detection (checks for Error:, Exception:, Failure, and Unbound)
• Built-in timing eliminates the need to wrap calls in time (...)

hol_load returns quiet structured JSON

  {"success": true, "file": "Library/words.ml", "time_seconds": 0.45}

hol_load is meant for loading known-good files, so intermediate val bindings are suppressed entirely.

If it fails, an error field is included, and you can debug by using eval with needs "file.ml" to get the full output.

Other

• hol_status now includes max_output_chars in its response
• hol-mcp.toml gains a max_output_chars config key
• Bump all deps to resolve Bump pygments from 2.19.2 to 2.20.0 in /mcp #158, Bump cryptography from 46.0.5 to 46.0.6 in /mcp #159, and Bump pyjwt from 2.11.0 to 2.12.0 in /mcp #160

Note on truncation safety

Truncation is purely cosmetic. It is implemented in Python after all output has been read from the HOL Light subprocess. Specifically, this does not break pipes or SIGPIPE.

[jrh13]

All looks great, thanks!