Commit graph

4 commits

Author SHA1 Message Date
5bc4865424 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)
2026-06-21 01:24:56 -05:00
b038778361 feat(lean): SDPVerify, GoormaghtighCert, Hachimoji modules; Gremlin mathblob graph loader; branch cleanup
- SDPVerify.lean: certificate verification engine (714 lines, compiles cleanly)
- GoormaghtighCert.lean: Goormaghtigh conjecture SDP certificate
- HachimojiManifoldAxiom/HachimojiSubstitution: Hachimoji DNA encoding
- GeneticBraidBridge.lean: genetic algorithm braid bridge
- load_dependency_graph/load_module_graph: Gremlin Cosmos DB graph loaders
- test_graph_queries/rrc_math_xref: graph verification queries
- Gremlin mathblob DB provisioned and accessible
- Branch cleanup: deleted 11 stale remote branches

Build: 3297 jobs, 0 errors (lake build Semantics.SDPVerify)
2026-06-19 23:06:16 -05:00
45048db9cc feat(infra): token-saver MCP — free local compute for any MCP client
8 tools, all routing to free compute first:
  verify_build, classify_proof, compile_check, linter_check,
  generate_proof (neon → paid fallback), format_code, doc_lookup, health

Any MCP-compatible agent (Claude Code, OpenCode, Cursor) can call
these tools and avoid burning API tokens on compilation/verification.
2026-06-16 20:04:40 -05:00
568f8686c5 feat(infra): token-saver MCP — routes to free local compute first
TokenSaver MCP (token_saver_mcp.py):
  - verify_build:    qfox-1 build server (HTTP, 0 tokens)
  - classify_proof:  rrc-watchdog exe (local Lean, 0 tokens)
  - compile_check:   lake env lean (local, 0 tokens)
  - generate_proof:  neon DeepSeek-Prover-V2 first (CPU, 0 tokens),
                     falls back to OpenRouter DeepSeek V4 Flash (paid)

Registered in opencode.json as 'token-saver'.

Build: 3571 jobs, 0 errors
2026-06-16 20:02:32 -05:00