mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
fix(infra): deduplicate MCP servers to reduce memory pressure
- Replace repo .mcp.json with minimal config (10 essential servers instead of 29). Full backup retained as .mcp.json.full. - Remove inline MCP section from ~/.config/opencode/config.json so OpenCode loads only repo .mcp.json (also removes hardcoded Linear token leak). - Add singleton guards to opencode_prover_mcp.py, token_saver_mcp.py, and remote_lean_proof_mcp.py to prevent duplicate instances when multiple IDE configs reference them. Build: N/A (Python shims)
This commit is contained in:
parent
dad5d9feab
commit
5bc4865424
4 changed files with 83 additions and 246 deletions
284
.mcp.json
284
.mcp.json
|
|
@ -1,88 +1,29 @@
|
|||
{
|
||||
"$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.",
|
||||
"_comment": "Minimal MCP config for OpenCode in Research Stack. Disables rarely-used servers to reduce memory pressure. For a full list see ../.mcp.json.",
|
||||
"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.",
|
||||
"_comment": "Read/write proof artifacts, Lean kernels, and receipts.",
|
||||
"command": "npx",
|
||||
"args": [
|
||||
"-y",
|
||||
"@modelcontextprotocol/server-filesystem",
|
||||
"."
|
||||
],
|
||||
"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.",
|
||||
"git": {
|
||||
"_comment": "Git history navigation: diff, blame, log.",
|
||||
"command": "uvx",
|
||||
"args": [
|
||||
"mcp-sympy"
|
||||
],
|
||||
"args": ["mcp-server-git", "--repository", "."],
|
||||
"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'.",
|
||||
"fetch": {
|
||||
"_comment": "HTTP fetch for docs, RFCs, release notes.",
|
||||
"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": [],
|
||||
"args": ["mcp-server-fetch"],
|
||||
"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.",
|
||||
"_comment": "Persistent memory/context/search. Disable ene-contextstream when this is enabled.",
|
||||
"command": "npx",
|
||||
"args": [
|
||||
"--prefer-online",
|
||||
"-y",
|
||||
"@contextstream/mcp-server@latest"
|
||||
],
|
||||
"args": ["--prefer-online", "-y", "@contextstream/mcp-server@latest"],
|
||||
"env": {
|
||||
"CONTEXTSTREAM_API_URL": "https://api.contextstream.io",
|
||||
"CONTEXTSTREAM_API_KEY": "${CONTEXTSTREAM_API_KEY}",
|
||||
|
|
@ -106,196 +47,49 @@
|
|||
"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 \u2014 lightweight type-checking and proof info for Lean files in Semantics/.",
|
||||
"lean": {
|
||||
"_comment": "Lean 4 / Mathlib typecheck bridge.",
|
||||
"command": "uvx",
|
||||
"args": [
|
||||
"lean-lsp-mcp",
|
||||
"--lean-project-path",
|
||||
"0-Core-Formalism/lean/Semantics"
|
||||
],
|
||||
"args": ["--from", "lean-mcp", "lean-mcp-server", "--lakefile", "0-Core-Formalism/lean/Semantics/lakefile.toml"],
|
||||
"env": {}
|
||||
},
|
||||
"k8s": {
|
||||
"_comment": "Kubernetes MCP server (read-only). Query k3s cluster on cupfox (100.72.130.76). Uses default kubeconfig.",
|
||||
"remote-lean-proof": {
|
||||
"_comment": "Hermes/OpenCode/Codex proof backend.",
|
||||
"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"
|
||||
}
|
||||
},
|
||||
"sympy": {
|
||||
"_comment": "Symbolic verification of arithmetic claims.",
|
||||
"command": "uvx",
|
||||
"args": ["mcp-sympy"],
|
||||
"env": {}
|
||||
},
|
||||
"wolfram-alpha": {
|
||||
"_comment": "Wolfram Alpha symbolic verification. Requires WOLFRAM_APP_ID.",
|
||||
"command": "npx",
|
||||
"args": [
|
||||
"-y",
|
||||
"kubernetes-mcp-server@latest",
|
||||
"--read-only"
|
||||
],
|
||||
"args": ["-y", "wolfram-mcp"],
|
||||
"env": {}
|
||||
},
|
||||
"arxiv": {
|
||||
"_comment": "ArXiv paper search MCP. Cache papers in ~/.arxiv-papers for offline reference. Connects to the arxiv cross-ref pipeline.",
|
||||
"aws": {
|
||||
"_comment": "AWS API access via boto3 credential chain.",
|
||||
"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"
|
||||
],
|
||||
"args": ["awslabs.aws-api-mcp-server@latest"],
|
||||
"env": {
|
||||
"SHAPE_INDEX_PATH": "/home/allaun/lean_corpus/shape_index.json"
|
||||
"AWS_REGION": "us-east-1",
|
||||
"FASTMCP_LOG_LEVEL": "ERROR"
|
||||
}
|
||||
},
|
||||
"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.",
|
||||
"_comment": "GitHub MCP via Copilot endpoint. Requires GITHUB_PERSONAL_ACCESS_TOKEN env var.",
|
||||
"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"
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
|
|||
|
|
@ -3,6 +3,7 @@
|
|||
|
||||
from __future__ import annotations
|
||||
|
||||
import fcntl
|
||||
import hashlib
|
||||
import json
|
||||
import os
|
||||
|
|
@ -17,7 +18,19 @@ from typing import Any
|
|||
SERVER_NAME = "remote-lean-proof"
|
||||
SERVER_VERSION = "0.1.0"
|
||||
DEFAULT_URL = "http://localhost:8787"
|
||||
DEFAULT_TOKEN_FILE = Path.home() / ".config/ene/language-proof-server.token"
|
||||
DEFAULT_TOKEN_FILE = Path.home() / ".config" / "ene" / "language-proof-server.token"
|
||||
|
||||
|
||||
def _ensure_singleton() -> None:
|
||||
"""Prevent multiple instances of this MCP server from running simultaneously."""
|
||||
lock_path = Path.home() / ".local" / "share" / "opencode" / "remote_lean_proof_mcp.lock"
|
||||
lock_path.parent.mkdir(parents=True, exist_ok=True)
|
||||
try:
|
||||
fd = os.open(str(lock_path), os.O_CREAT | os.O_RDWR)
|
||||
fcntl.flock(fd, fcntl.LOCK_EX | fcntl.LOCK_NB)
|
||||
except (OSError, BlockingIOError):
|
||||
print("remote_lean_proof_mcp is already running; exiting singleton instance.", file=sys.stderr)
|
||||
sys.exit(0)
|
||||
|
||||
|
||||
def json_text(data: Any) -> list[dict[str, str]]:
|
||||
|
|
@ -283,6 +296,7 @@ def handle(message: dict[str, Any]) -> dict[str, Any] | None:
|
|||
|
||||
|
||||
def main() -> None:
|
||||
_ensure_singleton()
|
||||
for line in sys.stdin:
|
||||
if not line.strip():
|
||||
continue
|
||||
|
|
|
|||
|
|
@ -11,6 +11,7 @@ Reads the OpenRouter API key from ~/.local/share/opencode/auth.json.
|
|||
|
||||
from __future__ import annotations
|
||||
|
||||
import fcntl
|
||||
import json
|
||||
import os
|
||||
import subprocess
|
||||
|
|
@ -28,6 +29,18 @@ OPENROUTER_URL = "https://openrouter.ai/api/v1/chat/completions"
|
|||
MODEL = "deepseek/deepseek-v4-flash"
|
||||
|
||||
|
||||
def _ensure_singleton() -> None:
|
||||
"""Prevent multiple instances of this MCP server from running simultaneously."""
|
||||
lock_path = Path.home() / ".local" / "share" / "opencode" / "opencode_prover_mcp.lock"
|
||||
lock_path.parent.mkdir(parents=True, exist_ok=True)
|
||||
try:
|
||||
fd = os.open(str(lock_path), os.O_CREAT | os.O_RDWR)
|
||||
fcntl.flock(fd, fcntl.LOCK_EX | fcntl.LOCK_NB)
|
||||
except (OSError, BlockingIOError):
|
||||
print("opencode_prover_mcp is already running; exiting singleton instance.", file=sys.stderr)
|
||||
sys.exit(0)
|
||||
|
||||
|
||||
def _get_api_key() -> str:
|
||||
"""Read the OpenRouter API key from opencode's auth.json."""
|
||||
auth_path = Path.home() / ".local" / "share" / "opencode" / "auth.json"
|
||||
|
|
@ -206,4 +219,5 @@ def _extract_proof(text: str) -> str:
|
|||
|
||||
|
||||
if __name__ == "__main__":
|
||||
_ensure_singleton()
|
||||
mcp.run(transport="stdio")
|
||||
|
|
|
|||
|
|
@ -21,6 +21,7 @@ Any MCP-compatible agent (Claude Code, OpenCode, Cursor) can call it.
|
|||
|
||||
from __future__ import annotations
|
||||
|
||||
import fcntl
|
||||
import json
|
||||
import os
|
||||
import subprocess
|
||||
|
|
@ -33,6 +34,19 @@ from mcp.server.fastmcp import FastMCP
|
|||
|
||||
mcp = FastMCP("token-saver", log_level="WARNING")
|
||||
|
||||
|
||||
def _ensure_singleton() -> None:
|
||||
"""Prevent multiple instances of this MCP server from running simultaneously."""
|
||||
lock_path = Path.home() / ".local" / "share" / "opencode" / "token_saver_mcp.lock"
|
||||
lock_path.parent.mkdir(parents=True, exist_ok=True)
|
||||
try:
|
||||
fd = os.open(str(lock_path), os.O_CREAT | os.O_RDWR)
|
||||
fcntl.flock(fd, fcntl.LOCK_EX | fcntl.LOCK_NB)
|
||||
except (OSError, BlockingIOError):
|
||||
print("token_saver_mcp is already running; exiting singleton instance.", file=sys.stderr)
|
||||
sys.exit(0)
|
||||
|
||||
|
||||
# ── Resource URLs (configurable via env) ────────────────────────────────
|
||||
|
||||
BUILD_SERVER = os.environ.get("BUILD_SERVER_URL", "http://100.88.57.96:8765")
|
||||
|
|
@ -299,4 +313,5 @@ def health() -> str:
|
|||
|
||||
|
||||
if __name__ == "__main__":
|
||||
_ensure_singleton()
|
||||
mcp.run(transport="stdio")
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue