From ee2a49342d08f057eb9dc45e0ae315818fe034b6 Mon Sep 17 00:00:00 2001 From: Brandon Schneider Date: Mon, 25 May 2026 22:27:18 -0500 Subject: [PATCH] Add proof worker pool routing --- .../infra/deploy_language_proof_server.sh | 2 +- .../infra/language_proof_server.py | 11 +++- .../infra/remote_lean_proof_mcp.py | 54 ++++++++++++++++--- AGENTS.md | 9 ++++ opencode.json | 1 + 5 files changed, 67 insertions(+), 10 deletions(-) diff --git a/4-Infrastructure/infra/deploy_language_proof_server.sh b/4-Infrastructure/infra/deploy_language_proof_server.sh index 1cda938f..17e6513e 100755 --- a/4-Infrastructure/infra/deploy_language_proof_server.sh +++ b/4-Infrastructure/infra/deploy_language_proof_server.sh @@ -116,7 +116,7 @@ fi export HOME=/var/lib/language-proof-server export PATH="$HOME/.elan/bin:$PATH" cd /srv/research-stack/0-Core-Formalism/lean/Semantics -runuser -u proofsrv -- sh -lc "cd /srv/research-stack/0-Core-Formalism/lean/Semantics && export PATH=/var/lib/language-proof-server/.elan/bin:\$PATH && elan toolchain install \"\$(cat lean-toolchain)\" && lake update" +runuser -u proofsrv -- sh -lc "cd /srv/research-stack/0-Core-Formalism/lean/Semantics && export PATH=/var/lib/language-proof-server/.elan/bin:\$PATH && elan toolchain install \"\$(cat lean-toolchain)\" || true; lake update" systemctl daemon-reload systemctl enable --now language-proof-server.service systemctl --no-pager --full status language-proof-server.service | sed -n "1,18p" diff --git a/4-Infrastructure/infra/language_proof_server.py b/4-Infrastructure/infra/language_proof_server.py index 6454d2eb..8b67ba9f 100644 --- a/4-Infrastructure/infra/language_proof_server.py +++ b/4-Infrastructure/infra/language_proof_server.py @@ -105,6 +105,11 @@ def command_env() -> dict[str, str]: return env +def command_prefix() -> list[str]: + raw = os.environ.get("PROOF_COMMAND_PREFIX", "").strip() + return shlex.split(raw) if raw else [] + + def run_command( command: list[str], cwd: Path, @@ -112,10 +117,11 @@ def run_command( timeout_s: int, ) -> dict[str, Any]: started = time.time() - command_display = " ".join(shlex.quote(part) for part in command) + full_command = command_prefix() + command + command_display = " ".join(shlex.quote(part) for part in full_command) try: proc = subprocess.run( - command, + full_command, cwd=str(cwd), env=command_env(), text=True, @@ -178,6 +184,7 @@ def health() -> dict[str, Any]: checks: dict[str, Any] = { "repo_dir": str(repo_dir()), "lean_root": str(root), + "proof_command_prefix": command_prefix(), "lean_root_exists": root.exists(), "lakefile_exists": (root / "lakefile.toml").exists(), "lean_toolchain_exists": (root / "lean-toolchain").exists(), diff --git a/4-Infrastructure/infra/remote_lean_proof_mcp.py b/4-Infrastructure/infra/remote_lean_proof_mcp.py index ad61ebc4..bdfbd19f 100644 --- a/4-Infrastructure/infra/remote_lean_proof_mcp.py +++ b/4-Infrastructure/infra/remote_lean_proof_mcp.py @@ -3,6 +3,7 @@ from __future__ import annotations +import hashlib import json import os import sys @@ -38,7 +39,29 @@ def base_url() -> str: return os.environ.get("PROOF_SERVER_URL", DEFAULT_URL).rstrip("/") -def request_json(path: str, payload: dict[str, Any] | None = None, timeout: int = 120) -> dict[str, Any]: +def proof_urls() -> list[str]: + raw = os.environ.get("PROOF_SERVER_URLS", "").strip() + urls = [item.strip().rstrip("/") for item in raw.split(",") if item.strip()] + if not urls: + urls = [base_url()] + return list(dict.fromkeys(urls)) + + +def ordered_urls(payload: dict[str, Any] | None = None) -> list[str]: + urls = proof_urls() + if len(urls) <= 1 or payload is None: + return urls + key = str(payload.get("name") or payload.get("target") or payload.get("agent") or "") + offset = int(hashlib.sha256(key.encode("utf-8")).hexdigest(), 16) % len(urls) + return urls[offset:] + urls[:offset] + + +def request_json_from( + url: str, + path: str, + payload: dict[str, Any] | None = None, + timeout: int = 120, +) -> dict[str, Any]: headers = {"Accept": "application/json", "User-Agent": f"{SERVER_NAME}/{SERVER_VERSION}"} body = None method = "GET" @@ -49,10 +72,13 @@ def request_json(path: str, payload: dict[str, Any] | None = None, timeout: int auth = token() if auth: headers["Authorization"] = f"Bearer {auth}" - req = urllib.request.Request(f"{base_url()}{path}", data=body, headers=headers, method=method) + req = urllib.request.Request(f"{url}{path}", data=body, headers=headers, method=method) try: with urllib.request.urlopen(req, timeout=timeout) as response: - return json.loads(response.read().decode("utf-8")) + data = json.loads(response.read().decode("utf-8")) + if isinstance(data, dict): + data.setdefault("proof_server_url", url) + return data except urllib.error.HTTPError as exc: text = exc.read().decode("utf-8", errors="replace") try: @@ -61,20 +87,34 @@ def request_json(path: str, payload: dict[str, Any] | None = None, timeout: int data = {"error": text} data["http_status"] = exc.code data["ok"] = False + data["proof_server_url"] = url return data except Exception as exc: - return {"ok": False, "error": f"{type(exc).__name__}: {exc}"} + return {"ok": False, "error": f"{type(exc).__name__}: {exc}", "proof_server_url": url} + + +def request_json(path: str, payload: dict[str, Any] | None = None, timeout: int = 120) -> dict[str, Any]: + failures = [] + for url in ordered_urls(payload): + data = request_json_from(url, path, payload, timeout) + if data.get("ok"): + return data + failures.append(data) + return {"ok": False, "error": "all proof servers failed", "failures": failures} def tool_status(_: dict[str, Any]) -> dict[str, Any]: - health = request_json("/health", timeout=10) + nodes = [request_json_from(url, "/health", timeout=10) for url in proof_urls()] + healthy = [node for node in nodes if node.get("ok")] return { - "ok": bool(health.get("ok")), + "ok": bool(healthy), "server": SERVER_NAME, "version": SERVER_VERSION, "proof_server_url": base_url(), + "proof_server_urls": proof_urls(), "token_configured": bool(token()), - "health": health, + "health": healthy[0] if healthy else (nodes[0] if nodes else {"ok": False}), + "nodes": nodes, } diff --git a/AGENTS.md b/AGENTS.md index f12c0666..8bd1776d 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -229,6 +229,15 @@ slow or unavailable. The MCP server fronts the dedicated proof service at `~/.config/ene/language-proof-server.token`, and returns receipt-bearing responses. +Active proof-worker pool: + +```text +http://54.236.176.28:8787 AWS EC2 dedicated proof server +http://100.110.163.82:8787 361395-1 Netcup proof worker +http://100.102.173.61:8787 nixos-laptop proof worker +http://100.85.244.73:8787 nixos-steamdeck-1 proof worker +``` + Primary tools: - `proof_status` for health and token wiring. diff --git a/opencode.json b/opencode.json index 4e5d74ce..c67eefbc 100644 --- a/opencode.json +++ b/opencode.json @@ -31,6 +31,7 @@ ], "environment": { "PROOF_SERVER_URL": "http://54.236.176.28:8787", + "PROOF_SERVER_URLS": "http://54.236.176.28:8787,http://100.110.163.82:8787,http://100.102.173.61:8787,http://100.85.244.73:8787", "PROOF_SERVER_TOKEN_FILE": "/home/allaun/.config/ene/language-proof-server.token" }, "enabled": true