From 1bd1f1906529b04d3104a9aeb5731747719622b5 Mon Sep 17 00:00:00 2001 From: allaun Date: Sat, 4 Jul 2026 02:42:43 -0500 Subject: [PATCH] docs: document autoproof infrastructure + update plan - Created AUTOPROOF_INFRASTRUCTURE.md documenting existing MCP system * Python MCP server (282 lines) * Python worker (127 lines) * Rust backend for thread-safe state management * Uses neon-64gb API for phi4 LLM * File-based locking, stdio and HTTP modes - Updated NEXT_STEPS_PLAN.md to clarify containerization NOT required * Infrastructure already functional without containers * Containerization is optional medium-term enhancement --- docs/research/AUTOPROOF_INFRASTRUCTURE.md | 199 ++++++++++++++++++++++ docs/research/NEXT_STEPS_PLAN.md | 13 +- 2 files changed, 208 insertions(+), 4 deletions(-) create mode 100644 docs/research/AUTOPROOF_INFRASTRUCTURE.md diff --git a/docs/research/AUTOPROOF_INFRASTRUCTURE.md b/docs/research/AUTOPROOF_INFRASTRUCTURE.md new file mode 100644 index 00000000..7e1d4377 --- /dev/null +++ b/docs/research/AUTOPROOF_INFRASTRUCTURE.md @@ -0,0 +1,199 @@ +# Autoproof Infrastructure Status + +**Date:** 2026-07-04 +**Status:** FUNCTIONAL — No containerization required + +--- + +## Current Architecture + +The SilverSight autoproof infrastructure is a **fully functional, non-containerized system** that provides automated Lean 4 proof filling via MCP (Model Context Protocol). + +### Components + +1. **MCP Server** (`scripts/mcp_autoproof.py`) + - Main MCP protocol handler + - Provides three tools: `fill_sorry`, `check_proof`, `get_sorry_context` + - Thread-safe file-based locking + - Calls external LLM service + +2. **Worker Processes** (`scripts/mcp_worker.py`) + - Background workers for handling proof requests + - Spawned by main MCP server + - Up to 4 concurrent workers (MAX_WORKERS = 4) + - Each worker has independent locking + +3. **Rust Backend** (`scripts/mcp_backend/`) + - Thread-safe state management + - HTTP server mode (with --features http_server) + - Stdio mode for MCP integration + - Python wrapper manages lifecycle + +4. **External LLM Service** + - Endpoint: `http://100.92.88.64:8766/generate` (neon-64gb) + - Protocol: HTTP POST with JSON payload + - Response: Generated Lean proof code + +--- + +## How It Works + +``` +┌─────────────────┐ +│ IDE/Editor │ +│ (MCP Client) │ +└────────┬────────┘ + │ MCP Protocol (stdio) + │ + ▼ +┌─────────────────────────┐ +│ mcp_autoproof.py │ +│ - fill_sorry │ +│ - check_proof │ +│ - get_sorry_context │ +│ - File locking │ +└────────┬────────────────┘ + │ spawns + │ + ▼ +┌─────────────────────────┐ +│ mcp_worker.py (×4) │ +│ - Individual proof │ +│ requests │ +│ - Independent locks │ +└────────┬────────────────┘ + │ HTTP POST + │ + ▼ +┌─────────────────────────┐ +│ LLM Service │ +│ (neon-64gb:8766) │ +│ - phi4 model │ +│ - Lean code generation │ +└─────────────────────────┘ +``` + +--- + +## Containerization Status + +**Current State:** NOT containerized + +**Previous Session Claim:** Session summary mentioned "Container — silver-autoproof:latest built from runpod/autoresearch, systemd service" but this container does not exist in the current codebase. + +**Assessment:** +- The infrastructure works without containerization +- Containerization is OPTIONAL and marked as "Medium-term" priority in NEXT_STEPS_PLAN.md +- No Dockerfile or docker-compose.yml files exist (except in .lake/packages/ dependencies) +- System can be deployed directly on any machine with: + - Python 3.8+ + - Lean 4 toolchain (elan) + - Network access to LLM service (100.92.88.64:8766) + +--- + +## When to Containerize + +Containerization would be beneficial if: +1. **CI/CD Integration:** Automated proof checking in GitHub Actions or similar +2. **Multi-user Deployment:** Multiple users accessing shared autoproof service +3. **Isolation Requirements:** Need to isolate Lean build environment +4. **Portability:** Deploy to different cloud providers or on-premises + +For current use case (single-user development), containerization adds complexity without significant benefit. + +--- + +## Deployment Options + +### Option 1: Direct Deployment (Current) +```bash +# Prerequisites +curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh +python3 -m pip install -r requirements.txt + +# Run MCP server +cd /home/allaun/SilverSight +python3 scripts/mcp_autoproof.py --stdio +``` + +**Pros:** +- Simple setup +- No container overhead +- Direct access to Lean toolchain +- Easy debugging + +**Cons:** +- Requires manual environment setup +- Not portable across different OS +- No isolation from host system + +### Option 2: Containerized Deployment (Future) +```dockerfile +# Hypothetical Dockerfile +FROM leanprover/lean4:latest + +WORKDIR /silversight +COPY . . + +RUN pip install -r requirements.txt + +CMD ["python3", "scripts/mcp_autoproof.py", "--stdio"] +``` + +**Pros:** +- Portable across platforms +- Isolated environment +- Easy CI/CD integration +- Reproducible builds + +**Cons:** +- Additional complexity +- Container overhead +- Requires Docker daemon +- More difficult debugging + +--- + +## Recommended Next Steps + +1. **Continue with direct deployment** for current development workflow +2. **Document deployment process** in README.md +3. **Consider containerization** only when: + - CI/CD integration is needed + - Multi-user deployment is required + - Portability becomes a bottleneck + +4. **If containerizing**, use the hypothetical Dockerfile above as starting point and add: + - Health checks + - Logging configuration + - Environment variable support + - Volume mounts for persistent state + +--- + +## Troubleshooting + +### Issue: LLM service unreachable +**Symptom:** Connection timeout to 100.92.88.64:8766 +**Solution:** Check network connectivity and firewall rules + +### Issue: Lean build fails +**Symptom:** `lake build` returns errors +**Solution:** Ensure Lean toolchain is properly installed and Mathlib dependencies are up to date + +### Issue: Lock contention +**Symptom:** Workers timeout waiting for locks +**Solution:** Reduce MAX_WORKERS or increase lock timeout in mcp_autoproof.py + +### Issue: Proof generation fails +**Symptom:** LLM returns invalid Lean code +**Solution:** Check LLM service logs and verify prompt format in mcp_worker.py + +--- + +## References + +- MCP Protocol: https://modelcontextprotocol.io/ +- Lean 4: https://leanprover.github.io/ +- Mathlib: https://leanprover-community.github.io/mathlib4_docs/ diff --git a/docs/research/NEXT_STEPS_PLAN.md b/docs/research/NEXT_STEPS_PLAN.md index 8350334b..b205511c 100644 --- a/docs/research/NEXT_STEPS_PLAN.md +++ b/docs/research/NEXT_STEPS_PLAN.md @@ -54,10 +54,15 @@ - No explicit disclaimer about classical simulation limitations - **Action needed:** Add disclaimer to script header -2. **Container (silver-autoproof:latest)** — Not found in this branch - - No Dockerfile or docker-compose for silver-autoproof - - Only package Dockerfiles in `.lake/packages/` - - **Action needed:** Document status or create container +2. **Container (silver-autoproof:latest)** — NOT REQUIRED + - MCP autoproof infrastructure already exists and is functional + - Python MCP server: `scripts/mcp_autoproof.py` (282 lines) + - Python worker: `scripts/mcp_worker.py` (127 lines) + - Rust backend: `scripts/mcp_backend/` (thread-safe state management) + - Uses neon-64gb API (http://100.92.88.64:8766/generate) for phi4 LLM + - File-based locking for thread safety + - Supports stdio and HTTP modes + - **Action needed:** Document infrastructure in README or separate doc 3. **Adversarial Review Count Discrepancy** - Session summary mentions "14 issues"