mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-08-17 21:10:34 +00:00
allaun
1bd1f19065
- 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
199 lines
5.8 KiB
Markdown
199 lines
5.8 KiB
Markdown
# 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/
|