From 5bea52a09afe26b40a850c6de963438c666bb966 Mon Sep 17 00:00:00 2001 From: allaun Date: Sun, 21 Jun 2026 05:31:11 -0500 Subject: [PATCH] fix(infra): wrap lean-lsp-mcp to correct severity schema for Moonshot API Added a python-based wrapper script for lean-lsp-mcp that intercepts and cleans the 'severity' schema field from the tools/list output, resolving the 400 error from Moonshot API which strictly forbids defining 'type' in parent schemas alongside 'anyOf'. Build: 3314 jobs, 0 errors (lake build) --- .mcp.json.full | 301 ++++++++++++++++++ .vscode/mcp.json | 4 +- 4-Infrastructure/AGENTS.md | 1 + .../infra/lean_lsp_mcp_wrapper.py | 88 +++++ 4 files changed, 392 insertions(+), 2 deletions(-) create mode 100644 .mcp.json.full create mode 100755 4-Infrastructure/infra/lean_lsp_mcp_wrapper.py diff --git a/.mcp.json.full b/.mcp.json.full new file mode 100644 index 00000000..60eb49e3 --- /dev/null +++ b/.mcp.json.full @@ -0,0 +1,301 @@ +{ + "$schema": "https://modelcontextprotocol.io/schemas/2025-03-26/client-config.json", + "_comment": "Math-first MCP server declarations for Research Stack. Each server below is gated on a runtime environment variable so the config never embeds secrets and so contributors who have not provisioned a given backend simply skip it. See docs/math-first-tooling.md for setup instructions.", + "mcpServers": { + "filesystem": { + "_comment": "Read/write proof artifacts, Lean kernels, and DeepSeek receipts. Scope is the repository root so review tooling cannot escape the project tree.", + "command": "npx", + "args": [ + "-y", + "@modelcontextprotocol/server-filesystem", + "." + ], + "env": {} + }, + "sympy": { + "_comment": "Local SymPy bridge for symbolic verification of arithmetic claims. Package is 'mcp-sympy' on PyPI (provides 'mcp-sympy' executable); the sdiehl/sympy-mcp GitHub name differs from the PyPI name.", + "command": "uvx", + "args": [ + "mcp-sympy" + ], + "env": {} + }, + "wolfram-alpha": { + "_comment": "Wolfram Alpha symbolic verification. Requires WOLFRAM_APP_ID in the shell environment (NOT WOLFRAM_ALPHA_APPID \u2014 that's an alias in fish config). Package is 'wolfram-mcp' on npm (was '@wolfram-alpha/mcp-server' which no longer exists).", + "command": "npx", + "args": [ + "-y", + "wolfram-mcp" + ], + "env": {} + }, + "notion": { + "_comment": "Notion integration via official Notion MCP (Streamable HTTP + OAuth). Run `devin mcp login notion` once to complete the OAuth flow; tokens are stored locally and auto-refreshed.", + "url": "https://mcp.notion.com/mcp", + "transport": "http" + }, + "lean": { + "_comment": "Lean 4 / Mathlib typecheck bridge. Targets 0-Core-Formalism/lean/Semantics/ via the existing lakefile. Requires `elan` on PATH; see GETTING_STARTED.md for the lean-toolchain pin (leanprover/lean4:v4.30.0-rc2). The executable in the lean-mcp package is 'lean-mcp-server', not 'lean-mcp'.", + "command": "uvx", + "args": [ + "--from", + "lean-mcp", + "lean-mcp-server", + "--lakefile", + "0-Core-Formalism/lean/Semantics/lakefile.toml" + ], + "env": {} + }, + "remote-lean-proof": { + "_comment": "Hermes/OpenCode/Codex proof backend. Calls the dedicated AWS language-proof-server and returns receipt-bearing Lean/Lake results. Token is read from PROOF_SERVER_TOKEN or ~/.config/ene/language-proof-server.token.", + "command": "python3", + "args": [ + "4-Infrastructure/infra/remote_lean_proof_mcp.py" + ], + "env": { + "PROOF_SERVER_URL": "${PROOF_SERVER_URL}", + "PROOF_SERVER_TOKEN_FILE": "/home/allaun/.config/ene/language-proof-server.token" + } + }, + "service-orchestrator": { + "_comment": "Unified control plane: register/unregister services across Authentik + Caddy + credential server. Requires AUTHENTIK_TOKEN and CADDY_ADMIN env vars. HTTP mode on port 8338.", + "command": "python3", + "args": [ + "4-Infrastructure/infra/service-orchestrator/service_orchestrator.py" + ], + "env": { + "AUTHENTIK_BASE": "http://100.102.173.61:9000", + "CADDY_ADMIN": "http://100.101.247.127:2019", + "CREDENTIAL_SERVER": "http://100.101.247.127:8444" + } + }, + "authentik-mcp": { + "_comment": "Authentik SSO MCP server \u2014 user/group/application management via Authentik API v3. Requires AUTHENTIK_TOKEN env var. Built from 4-Infrastructure/shim/authentik_agent_manager/.", + "command": "/home/allaun/Research Stack/4-Infrastructure/shim/authentik_agent_manager/target/release/mcp_server", + "args": [], + "env": {} + }, + "contextstream": { + "_comment": "Persistent memory, context, and search across all coding sessions. Provides session management, knowledge graph, code search, and decision/lesson capture. Plan: Elite.", + "command": "npx", + "args": [ + "--prefer-online", + "-y", + "@contextstream/mcp-server@latest" + ], + "env": { + "CONTEXTSTREAM_API_URL": "https://api.contextstream.io", + "CONTEXTSTREAM_API_KEY": "${CONTEXTSTREAM_API_KEY}", + "CONTEXTSTREAM_ALLOW_HEADER_AUTH": "false", + "CONTEXTSTREAM_WORKSPACE_ID": "21c133f6-6854-4e81-b801-4037c11b7e34", + "CONTEXTSTREAM_PROJECT_ID": "ef91cc79-aae3-4765-ae0d-63b48f5ea6e6", + "CONTEXTSTREAM_USER_AGENT": "contextstream-mcp/0.4.74", + "CONTEXTSTREAM_TOOLSET": "complete", + "CONTEXTSTREAM_LOG_LEVEL": "quiet", + "CONTEXTSTREAM_OUTPUT_FORMAT": "compact", + "CONTEXTSTREAM_CONTEXT_PACK": "true", + "CONTEXTSTREAM_TRANSCRIPTS_ENABLED": "true", + "CONTEXTSTREAM_HOOK_TRANSCRIPTS_ENABLED": "true", + "CONTEXTSTREAM_SHOW_TIMING": "false", + "CONTEXTSTREAM_PROGRESSIVE_MODE": "false", + "CONTEXTSTREAM_ROUTER_MODE": "false", + "CONTEXTSTREAM_CONSOLIDATED": "true", + "CONTEXTSTREAM_AUTO_HIDE_INTEGRATIONS": "true", + "CONTEXTSTREAM_SEARCH_LIMIT": "15", + "CONTEXTSTREAM_SEARCH_MAX_CHARS": "2400", + "CONTEXTSTREAM_INCLUDE_STRUCTURED_CONTENT": "true" + } + }, + "ene-contextstream": { + "_comment": "Local ENE replacement for ContextStream-like memory/search/session recall. Writes local receipt-bearing SQLite memory and reads ene-api/session-sync when running.", + "command": "python3", + "args": [ + "/home/allaun/Research Stack/4-Infrastructure/infra/ene_contextstream_mcp.py" + ], + "env": { + "ENE_API_URL": "http://127.0.0.1:3000", + "ENE_CONTEXT_STORE": "/home/allaun/.local/share/ene/contextstream.sqlite", + "ENE_CONTEXT_CANDIDATE_ROOT": "/home/allaun/Research Stack/shared-data/data/germane/research/github-ene-contextstream" + } + }, + "deepseek-prover": { + "_comment": "DeepSeek-Prover-V2-7B proof search. Backend: ollama (default), huggingface, or deepseek_api. Generates Lean proof candidates, compiles with lake build, iterates with error feedback.", + "command": "python3", + "args": [ + "4-Infrastructure/infra/deepseek_prover_mcp.py" + ], + "env": { + "DEEPSEEK_PROVER_BACKEND": "ollama", + "OLLAMA_URL": "http://localhost:11434", + "LAKE_WORKDIR": "/home/allaun/Research Stack/0-Core-Formalism/lean/Semantics" + } + }, + "vikunja": { + "_comment": "Kanban board server on neon (100.92.88.64). Agents and humans set goals, track status, assign tasks. Wraps Vikunja v2.3.0 REST API.", + "command": "python3", + "args": [ + "4-Infrastructure/infra/vikunja_mcp.py" + ], + "env": { + "VIKUNJA_URL": "http://100.92.88.64:3456", + "VIKUNJA_TOKEN_FILE": "/home/allaun/.config/ene/vikunja.token" + } + }, + "lean-lsp": { + "_comment": "Lean Language Server MCP — lightweight type-checking and proof info for Lean files in Semantics/. Wrapped to fix Moonshot/Kimi schema validation.", + "command": "python3", + "args": [ + "4-Infrastructure/infra/lean_lsp_mcp_wrapper.py", + "--lean-project-path", + "0-Core-Formalism/lean/Semantics" + ], + "env": {} + }, + "k8s": { + "_comment": "Kubernetes MCP server (read-only). Query k3s cluster on cupfox (100.72.130.76). Uses default kubeconfig.", + "command": "npx", + "args": [ + "-y", + "kubernetes-mcp-server@latest", + "--read-only" + ], + "env": {} + }, + "arxiv": { + "_comment": "ArXiv paper search MCP. Cache papers in ~/.arxiv-papers for offline reference. Connects to the arxiv cross-ref pipeline.", + "command": "uvx", + "args": [ + "arxiv-mcp-server", + "--storage-path", + "/home/allaun/.arxiv-papers" + ], + "env": {} + }, + "nixos": { + "_comment": "NixOS MCP server. Read/write NixOS configs (steamdeck, nixos-laptop, neon). Requires ssh access.", + "command": "uvx", + "args": [ + "mcp-nixos" + ], + "env": {} + }, + "shape-index": { + "_comment": "FAMM shape-index of the Lean corpus. 112K indexed theorems classified by Sidon sumset signature. Query nearest neighbors by shape to find proof templates.", + "command": "python3", + "args": [ + "4-Infrastructure/infra/shape_index_mcp.py" + ], + "env": { + "SHAPE_INDEX_PATH": "/home/allaun/lean_corpus/shape_index.json" + } + }, + "github": { + "_comment": "GitHub MCP (official Copilot endpoint). Provides PR creation/review, issue tracking, CI status, repo search, and branch management. Set GITHUB_PERSONAL_ACCESS_TOKEN in the shell environment (token lives in Goose config \u2014 do NOT hardcode here). The token in ~/.config/goose/config.yaml should be migrated to a secrets store or shell profile.", + "type": "http", + "url": "https://api.githubcopilot.com/mcp/", + "headers": { + "Authorization": "Bearer ${GITHUB_PERSONAL_ACCESS_TOKEN}" + } + }, + "git": { + "_comment": "Git MCP server for history navigation: diff, blame, log traversal, commit search. Complements the filesystem MCP with git-native operations. Useful for proof archaeology and tracing when/why a lemma changed.", + "command": "uvx", + "args": [ + "mcp-server-git", + "--repository", + "." + ], + "env": {} + }, + "fetch": { + "_comment": "HTTP fetch MCP \u2014 retrieve any public URL as text or markdown. Fills the gap between ArXiv (papers) and Wolfram (symbolic): reading Mathlib4 docs, Lean release notes, RFC pages, blog posts, etc.", + "command": "uvx", + "args": [ + "mcp-server-fetch" + ], + "env": {} + }, + "serena": { + "_comment": "Serena code intelligence MCP (Oraios). LSP-powered cross-file symbol search, call-graph navigation, and definition lookup across all languages in the Research Stack (Lean, Rust, Python). Complements lean-lsp (Lean-only) with multi-language awareness.", + "command": "uvx", + "args": [ + "--from", + "git+https://github.com/oraios/serena", + "serena", + "start-mcp-server" + ], + "env": {} + }, + "context7": { + "_comment": "Context7 live library documentation (Upstash). Fetches real-time docs for Mathlib4, Lean stdlib, Python packages, and Rust crates \u2014 not stale training data. Use when lean-lsp hover info isn't enough and you need full API context.", + "command": "npx", + "args": [ + "-y", + "@upstash/context7-mcp" + ], + "env": {} + }, + "chrome-devtools": { + "_comment": "Chrome DevTools MCP \u2014 control and inspect a live Chrome browser session. Useful for testing web UIs (Authentik admin, Vikunja, Grafana dashboards) and scraping dynamically rendered pages that fetch MCP cannot reach.", + "command": "npx", + "args": [ + "-y", + "chrome-devtools-mcp@latest" + ], + "env": {} + }, + "council-of-mine": { + "_comment": "LLM council with 9 distinct personas (Block/Square). Routes a question to multiple opinionated advisors and synthesizes a debate. Useful for architectural decisions, proof strategy reviews, and doctrine alignment checks where a single agent perspective is insufficient.", + "command": "uvx", + "args": [ + "--from", + "git+https://github.com/block/mcp-council-of-mine", + "mcp_council_of_mine" + ], + "env": {} + }, + "gdrive": { + "_comment": "Google Drive MCP \u2014 read/write access to Google Drive files. Imported from Windsurf config. Requires GOOGLE_CLIENT_ID and GOOGLE_CLIENT_SECRET env vars.", + "command": "npx", + "args": [ + "-y", + "@piotr-agier/google-drive-mcp" + ], + "env": { + "GOOGLE_CLIENT_ID": "${GOOGLE_CLIENT_ID}", + "GOOGLE_CLIENT_SECRET": "${GOOGLE_CLIENT_SECRET}" + } + }, + "opencode-prover": { + "_comment": "OpenCode Prover MCP \u2014 from OpenCode config. Lean proof verification bridge for OpenCode/Codex CLI.", + "command": "python3", + "args": [ + "5-Applications/tools-scripts/mcp/opencode_prover_mcp.py" + ], + "env": {} + }, + "token-saver": { + "_comment": "Token saver MCP \u2014 from OpenCode config. Saves tokens by consolidating file reads and reducing redundant context.", + "command": "python3", + "args": [ + "5-Applications/tools-scripts/mcp/token_saver_mcp.py" + ], + "env": {} + }, + "container-use": { + "_comment": "Container Use MCP (container-use.com). Spawns isolated container environments for running untrusted code, reproducible build experiments, and testing NixOS derivations without touching the host. Connects via mcp-remote relay.", + "command": "npx", + "args": [ + "-y", + "mcp-remote", + "https://container-use.com/mcp" + ], + "env": {} + }, + "consensus": { + "_comment": "Consensus MCP server for evidence-based search over 200M academic papers.", + "url": "https://mcp.consensus.app/mcp", + "transport": "http" + } + } +} \ No newline at end of file diff --git a/.vscode/mcp.json b/.vscode/mcp.json index 6211b184..863592ff 100644 --- a/.vscode/mcp.json +++ b/.vscode/mcp.json @@ -48,9 +48,9 @@ }, "lean-lsp": { "type": "stdio", - "command": "uvx", + "command": "python3", "args": [ - "lean-lsp-mcp", + "4-Infrastructure/infra/lean_lsp_mcp_wrapper.py", "--lean-project-path", "0-Core-Formalism/lean/Semantics" ], diff --git a/4-Infrastructure/AGENTS.md b/4-Infrastructure/AGENTS.md index d107513c..ab17a61d 100644 --- a/4-Infrastructure/AGENTS.md +++ b/4-Infrastructure/AGENTS.md @@ -315,6 +315,7 @@ python3 4-Infrastructure/storage/storage_agent.py --loop --interval 900 - `4-Infrastructure/shim/arxiv_oaipmh_harvest.py` — arXiv OAI-PMH harvester: fetches paper metadata (title, abstract, categories, authors) into arxiv DB on neon-64gb - `4-Infrastructure/shim/rrc_arxiv_kernel_refine.py` — RRC arXiv kernel refinement: title+abstract keyword search against arxiv_papers for unmatched equations +- `4-Infrastructure/infra/lean_lsp_mcp_wrapper.py` — Python wrapper for `lean-lsp-mcp` to fix the schema of `lean_diagnostic_messages` for compatibility with strict validators like Moonshot/Kimi API. - `4-Infrastructure/shim/stack_solidification_audit.py` - `4-Infrastructure/shim/stack_fail_closure_register.py` - `4-Infrastructure/shim/beaver_mask_freshness_negative_controls.py` diff --git a/4-Infrastructure/infra/lean_lsp_mcp_wrapper.py b/4-Infrastructure/infra/lean_lsp_mcp_wrapper.py new file mode 100755 index 00000000..502ad809 --- /dev/null +++ b/4-Infrastructure/infra/lean_lsp_mcp_wrapper.py @@ -0,0 +1,88 @@ +#!/usr/bin/env python3 +import sys +import subprocess +import json +import threading + +def forward_stdin(proc): + try: + for line in sys.stdin: + proc.stdin.write(line) + proc.stdin.flush() + except Exception: + pass + finally: + try: + proc.stdin.close() + except Exception: + pass + +def forward_stderr(proc): + try: + for line in proc.stderr: + sys.stderr.write(line) + sys.stderr.flush() + except Exception: + pass + +def main(): + # Construct the command to run the real lean-lsp-mcp + cmd = ["uvx", "lean-lsp-mcp"] + sys.argv[1:] + + # Start the child process + proc = subprocess.Popen( + cmd, + stdin=subprocess.PIPE, + stdout=subprocess.PIPE, + stderr=subprocess.PIPE, + text=True, + bufsize=1 + ) + + # Start threads to forward stdin and stderr + t_in = threading.Thread(target=forward_stdin, args=(proc,), daemon=True) + t_err = threading.Thread(target=forward_stderr, args=(proc,), daemon=True) + t_in.start() + t_err.start() + + try: + # Read from child stdout line by line + for line in proc.stdout: + line_str = line.strip() + if not line_str: + sys.stdout.write(line) + sys.stdout.flush() + continue + + try: + msg = json.loads(line_str) + # Check if it's a response with result and tools + if isinstance(msg, dict) and "result" in msg and "tools" in msg["result"]: + tools = msg["result"]["tools"] + for tool in tools: + if tool.get("name") == "lean_diagnostic_messages": + properties = tool.get("inputSchema", {}).get("properties", {}) + if "severity" in properties: + severity_schema = properties["severity"] + # Fix the schema: if anyOf is present, remove the parent 'type' + if "anyOf" in severity_schema and "type" in severity_schema: + del severity_schema["type"] + # Serialize the modified message + line = json.dumps(msg) + "\n" + except Exception: + # If parsing fails, just forward the original line + pass + + sys.stdout.write(line) + sys.stdout.flush() + except Exception: + pass + finally: + proc.terminate() + try: + proc.wait(timeout=2) + except subprocess.TimeoutExpired: + proc.kill() + +if __name__ == "__main__": + main()