mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
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
This commit is contained in:
parent
a239fb42b4
commit
1bd1f19065
2 changed files with 208 additions and 4 deletions
199
docs/research/AUTOPROOF_INFRASTRUCTURE.md
Normal file
199
docs/research/AUTOPROOF_INFRASTRUCTURE.md
Normal file
|
|
@ -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/
|
||||
|
|
@ -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"
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue