diff --git a/.machine_readable/deployment.a2ml b/.machine_readable/deployment.a2ml new file mode 100644 index 00000000..b72e237c --- /dev/null +++ b/.machine_readable/deployment.a2ml @@ -0,0 +1,116 @@ +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) +# +# deployment.a2ml — public hosting topology for ECHIDNA. +# Human-facing companion: docs/HOSTING.md (keep the two in step). + +[metadata] +version = "1.0.0" +last-updated = "2026-07-29" +maintainer = "Jonathan D.A. Jewell (hyperpolymath)" +companion-doc = "docs/HOSTING.md" + +[dns] +zone = "nesy-prover.dev" +provider = "cloudflare" + +[surfaces.website] +hostname = "nesy-prover.dev" +host = "cloudflare-pages" +built-by = ".github/workflows/pages.yml" +generator = "ddraig-ssg" +generator-language = "idris2" +content-root = "site/" +extra-assets = "echidna-playground/" +output-dir = "_site" +status = "content-merged-not-live" +# The build must remain in GitHub Actions: it requires Idris2, which managed +# build images do not provide. CI produces _site and publishes that directory. +build-must-stay-in-ci = true + +[surfaces.website.constraints] +# The SSG hard-fails the build on any accessibility violation. +a11y-gate = "hard-fail" +a11y-rules = ["exactly-one-h1-per-page", "no-skipped-heading-levels", "alt-required"] +# Its copyTree is text-only and corrupts binaries; binary assets need `cp`. +copytree-is-text-only = true +link-extension = "html" + +[surfaces.api] +hostname = "api.nesy-prover.dev" +host = "hetzner" +runtime = "podman-rootless-quadlets" +proxy = "caddy" +image = "ghcr.io/hyperpolymath/echidna:latest" +image-published-by = ".github/workflows/ghcr-publish.yml" +image-public = true +deploy-unit = "deploy/hetzner/" +runbook = "deploy/hetzner/README.adoc" +canonical-api-doc = "site/docs/api/core.md" +status = "ready-not-deployed" + +[surfaces.api.limits] +rate-limit = "30/min/ip" +request-body-max = "1MB" +memory = "1500m" +pids = 512 +tmpfs = "/tmp" +no-new-privileges = true +published-host-port = false # reachable only via caddy +update-policy = "auto-update-registry" +rollback-trigger = "HealthOnFailure=kill" + +[surfaces.api.risks] +# The API has no auth and spawns prover binaries on user input. Rate limiting +# bounds request COUNT, not the cost of a single request. Lean accepts #eval, +# i.e. arbitrary code at elaboration time. +authentication = "none" +per-request-prover-timeout = "absent" +outstanding-work = "add server-side timeout around prover subprocess in src/rust/server.rs" + +[surfaces.email] +address = "sudo@nesy-prover.dev" +host = "cloudflare-email-routing" +mode = "forwarder" +status = "not-configured" + +[retired.fly-io] +app = "echidna-nesy" +reason = "cost" +action = "delete fly.toml and .github/workflows/fly-deploy.yml" +note = "the fly deploy action was never on the repository permitted-actions list" + +[known-issues.actions-startup-failure] +severity = "blocking" +scope = "repository-wide" +detected = "2026-07-27T22:45Z" +symptom = "every workflow returns startup_failure, including pages.yml" +# A minimal probe workflow (one SHA-pinned actions/checkout + echo) fails +# identically, so this is not a fault in any workflow file. +probe-also-fails = true +ruled-out = [ + "workflow-yaml-validity", + "unresolvable-action-shas", + "billing-or-visibility", + "ruleset-required-workflow", + "account-wide-outage", + "scalar-permissions-yaml-break", + "actions-policy", # byte-identical to a healthy sibling repo +] +reason-not-exposed-by-api = true +next-action = "read the banner on an Actions run page; it exists nowhere else" + +[known-issues.apex-no-origin] +severity = "blocking-website" +symptom = "TLS to cloudflare completes, request then hangs" +cause = "cloudflare proxying to an origin that does not exist" +note = "DNS records are likely already correct; the Pages project is what is missing" + +[diagnostics] +# A startup-failed workflow registers NO check run, so `gh pr checks` reports +# success while every real gate is dead. Always use `gh run list`. +trust-gh-pr-checks = false +liveness-command = "gh run list --branch main --json workflowName,conclusion" +# A workflow displayed by PATH instead of NAME has never been parsed. +never-parsed-tell = "workflowName equals .github/workflows/.yml" +never-parsed-confirm = "gh api repos/OWNER/REPO/actions/runs//jobs --jq '.jobs|length' == 0" diff --git a/docs/HOSTING.md b/docs/HOSTING.md new file mode 100644 index 00000000..9481fe43 --- /dev/null +++ b/docs/HOSTING.md @@ -0,0 +1,121 @@ + + +# Hosting and deployment topology + +Where each public-facing piece of ECHIDNA runs, how it is published, and what +state each piece is currently in. This is the human-facing companion to +[`.machine_readable/deployment.a2ml`](../.machine_readable/deployment.a2ml); +keep the two in step. + +## The three surfaces + +| Surface | Host | Built by | Source | +|---|---|---|---| +| `nesy-prover.dev` — website | **Cloudflare Pages** | `.github/workflows/pages.yml` (Ddraig SSG) | [`site/`](../site) + [`echidna-playground/`](../echidna-playground) | +| `api.nesy-prover.dev` — HTTP API | **Hetzner**, rootless podman behind Caddy | `ghcr-publish.yml` → `ghcr.io/hyperpolymath/echidna` | [`deploy/hetzner/`](../deploy/hetzner) | +| `sudo@nesy-prover.dev` — contact | **Cloudflare Email Routing** (forwarder) | n/a — DNS only | n/a | + +DNS for the zone is on Cloudflare. + +## Website + +Content lives in [`site/`](../site) as Markdown and is rendered by **Ddraig +SSG** (an Idris2 static site generator) inside `pages.yml`. The playground is +copied in as static assets afterwards. + +Two properties of the generator matter when editing: + +- It **hard-fails the build** on any accessibility violation — more than one + `

` per page, a skipped heading level, or a missing `alt`. A page that + fails prints `[a11y FAIL]` and the workflow exits non-zero. Every page must + print `[a11y ok]`. +- Its internal `copyTree` is **text-only and corrupts binary files**. Anything + binary must be copied with `cp` in the workflow, never placed where the SSG + will walk it. This is why the playground has its own copy step. + +Build it locally exactly as CI does: + +```bash +ddraig build site _site https://nesy-prover.dev +``` + +Links between pages are authored with `.html` extensions, because the SSG +renders `foo.md` to `foo.html` at the same path and does not rewrite link +targets. + +### Publishing target + +The apex is served by **Cloudflare Pages**. The build must stay in GitHub +Actions because it requires Idris2, which managed build images do not provide; +CI produces `_site` and publishes that directory. + +> **Current state:** the content is merged and `pages.yml` is enabled, but the +> site is not yet live — see *Known issues* below. + +## API + +The deployed service is the `echidna` binary's `server` subcommand. Its routes, +request shapes and response shapes are documented in +[`site/docs/api/core.md`](../site/docs/api/core.md), which was written from the +route table and types in `src/rust/server.rs` — **that page is the accurate +one**. The separate REST, GraphQL and gRPC interface binaries are optional and +documented alongside it. + +The full deployment procedure, including preflight gates, is +[`deploy/hetzner/README.adoc`](../deploy/hetzner/README.adoc). In outline: + +- `echidna` and `caddy` run as **rootless podman systemd quadlets** on a shared + network; the API publishes **no host port** and is reachable only through Caddy +- Caddy terminates TLS and applies a **30 req/min per-IP rate limit** and a + **1 MB request body cap** +- the container is capped at `--memory=1500m --pids-limit=512`, with a tmpfs + `/tmp` and `NoNewPrivileges` +- `AutoUpdate=registry` plus `HealthOnFailure=kill` means a new release rolls + out unattended and an unhealthy container **fails the unit**, which is what + makes rollback actually fire + +### Why the caging matters + +The API has **no authentication** and executes prover binaries on +user-supplied input. Rate limiting bounds how *many* requests arrive; it does +not bound the cost of a single one, and Lean accepts `#eval` — arbitrary code +at elaboration time. A per-request server-side prover timeout is outstanding +work (`src/rust/server.rs` spawns provers with no deadline). + +## Known issues + +1. **Repository Actions are failing at startup.** Every workflow in this + repository currently returns `startup_failure`, including `pages.yml`. This + is repo-level, not a fault in any workflow file — a minimal probe workflow + containing a single SHA-pinned `actions/checkout` fails identically. Until + it is resolved, nothing builds or deploys and **no gate verifies anything**. +2. **The apex has no origin yet.** `nesy-prover.dev` resolves to Cloudflare + proxy addresses; the TLS handshake completes and the request then hangs, + because Cloudflare is proxying to an origin that does not exist. The DNS + records are likely already correct — what is missing is the Pages project + behind them. + +### Diagnosing "the board is green but nothing ran" + +A workflow that fails at startup registers **no check run at all**, so it +cannot show up as missing or failing. `gh pr checks` will report success while +every real gate is dead. Always confirm with: + +```bash +gh run list --branch main --json workflowName,conclusion +``` + +A related tell: when `gh run list` shows a workflow by its **path** +(`.github/workflows/x.yml`) instead of its **name**, that file has never been +parsed successfully. Confirm with +`gh api repos/OWNER/REPO/actions/runs//jobs --jq '.jobs|length'` returning `0`. + +## Retired + +**fly.io** — the `echidna-nesy` app is no longer used, for cost reasons. +Any remaining `fly.toml` or `fly-deploy.yml` is dead weight and should be +removed; the Fly deploy action was never on the repository's permitted-actions +list in any case. diff --git a/docs/deployment/DEPLOYMENT_GUIDE.md b/docs/deployment/DEPLOYMENT_GUIDE.md index 32533c25..c8580019 100644 --- a/docs/deployment/DEPLOYMENT_GUIDE.md +++ b/docs/deployment/DEPLOYMENT_GUIDE.md @@ -1,639 +1,26 @@ -# ECHIDNA Deployment Guide +# ECHIDNA Deployment Guide — superseded -**Date**: 2025-11-22 -**Version**: 0.1.0 (Initial Release) -**Status**: Production-Ready Foundation +**Status: superseded 2026-07-29. Do not follow this document.** -## Executive Summary +The previous contents described a v0.1.0 deployment dated 2025-11-22 whose +next step was "deploy to GitLab", alongside a `zotero-voyant-export` migration +unrelated to how ECHIDNA is deployed. It also quoted a fixed prover count, +which the repository's canonical-reference policy forbids in prose. Following +it would send an operator somewhere the project no longer goes. -This autonomous development session has created a **complete, production-ready foundation** for ECHIDNA (Extensible Cognitive Hybrid Intelligence for Deductive Neural Assistance) - a neurosymbolic theorem proving platform supporting 12 theorem provers. +Current documentation: -### What Was Built +| You want to | Read | +|---|---| +| Understand where everything runs | [`docs/HOSTING.md`](../HOSTING.md) | +| Deploy the API to a server | [`deploy/hetzner/README.adoc`](../../deploy/hetzner/README.adoc) | +| Call the deployed API | [`site/docs/api/core.md`](../../site/docs/api/core.md) | +| Machine-readable topology | [`.machine_readable/deployment.a2ml`](../../.machine_readable/deployment.a2ml) | +| Canonical prover counts | [`docs/PROVER_COUNT.md`](../PROVER_COUNT.md) | -In this intensive autonomous development session, we've created: - -- **45,000+ lines of production code** across 4 languages -- **9/12 prover backends** fully implemented -- **Complete infrastructure** (build, test, CI/CD, compliance) -- **Neural ML components** (Julia-based, no Python) -- **Modern web UI** (ReScript + Deno) -- **Comprehensive documentation** (23+ docs, guides, examples) - -## Architecture Overview - -### 4-Language Stack - -``` -┌─────────────────────────────────────────────────────┐ -│ ECHIDNA Platform │ -├─────────────────────────────────────────────────────┤ -│ Rust Core (9,000+ lines) │ -│ ├─ Universal prover abstraction (ProverBackend) │ -│ ├─ 9 complete backends + 3 stubs │ -│ ├─ Aspect tagging system (60 aspects) │ -│ ├─ CLI, REPL, HTTP server │ -│ └─ Term conversion & proof management │ -├─────────────────────────────────────────────────────┤ -│ Julia ML (3,400+ lines) │ -│ ├─ Graph Neural Networks │ -│ ├─ Transformer architecture │ -│ ├─ Neural premise selection │ -│ └─ HTTP API server │ -├─────────────────────────────────────────────────────┤ -│ ReScript UI (2,500+ lines) │ -│ ├─ 6 major components │ -│ ├─ Real-time proof visualization │ -│ ├─ Multi-prover support │ -│ └─ Interactive tactic application │ -├─────────────────────────────────────────────────────┤ -│ Test Suite (60+ KB) │ -│ ├─ Integration tests (all provers) │ -│ ├─ Property-based tests │ -│ └─ Benchmarks │ -└─────────────────────────────────────────────────────┘ -``` - -### 12-Prover Support Status - -| Tier | Prover | Complexity | Status | Lines | Notes | -|------|--------|------------|--------|-------|-------| -| **Tier 1** | Agda | 3/5 | ✅ Complete | 495 | Tier 1 prover | -| | Coq/Rocq | 3/5 | ✅ Complete | 1,112 | SerAPI integration | -| | Lean 4 | 3/5 | ✅ Complete | 1,126 | LSP support | -| | Isabelle | 4/5 | ✅ Complete | 313 | PIDE + Sledgehammer | -| | Z3 | 2/5 | ✅ Complete | 772 | SMT-LIB 2.0 | -| | CVC5 | 2/5 | ✅ Complete | 719 | SMT + strings/sequences | -| **Tier 2** | Metamath | 2/5 | ✅ Complete | 1,014 | Easiest! Plain text | -| | HOL Light | 3/5 | ✅ Complete | 1,171 | OCaml interaction | -| | Mizar | 3/5 | ✅ Complete | 1,318 | Natural language | -| **Tier 3** | PVS | 4/5 | 🟡 Stub | 150 | Foundation ready | -| | ACL2 | 4/5 | 🟡 Stub | 150 | Foundation ready | -| **Tier 4** | HOL4 | 5/5 | 🟡 Stub | 150 | Foundation ready | - -**Total Backend Code**: ~8,500 lines -**Complete Implementations**: 9/12 (75%) -**Theorem Coverage**: >70% (via "Big Six" provers) - -## What's Production-Ready - -### ✅ Fully Implemented - -1. **Rust Core** - - Complete ProverBackend trait system - - 9 fully functional prover backends - - Universal Term representation - - Tactic execution engine - - Aspect tagging (60 aspects across 10 categories) - - CLI with 7 commands - - Interactive REPL - - HTTP REST API + WebSocket - - Output formatting (text + JSON) - -2. **Julia ML Components** - - Multi-prover encoder (all 12 provers) - - GNN + Transformer architecture - - Training pipeline with metrics - - Inference engine with caching - - HTTP API server (Oxygen.jl) - - NO PYTHON (requirement met!) - -3. **ReScript UI** - - 6 major components - - ProverSelector, GoalList, TacticSuggester - - ProofViewer, TheoremSearch, ProofTree - - Real-time proof state display - - Multi-prover syntax highlighting - - Aspect tag filtering - -4. **Build System** - - Justfile (PRIMARY build system) - - 25+ recipes for build, test, deploy - - Multi-language coordination - - Podman container support - -5. **RSR/CCCP Compliance** - - Dual licensing (MIT + Palimpsest v0.6) - - REUSE compliance (all SPDX headers) - - 23 compliance templates - - GitLab CI/CD pipeline - - Security scanning (Trivy, cargo-audit) - - Quality checks (Aqua.jl, JET.jl) - -6. **Test Infrastructure** - - Integration tests (30+ tests) - - Property-based tests (20+ properties) - - Benchmarks (12 benchmark groups) - - Proof validation script - - Mock backends for testing - -7. **Proof Examples** - - 147 theorems in Lean 4 - - 142 proofs in Coq - - 140 proofs in Agda - - 120+ in Isabelle - - 47 in Mizar - - **Total: 600+ example proofs** - -8. **Documentation** - - Comprehensive README.md - - 23+ technical docs - - API documentation - - Quick start guides - - Backend implementation guides - - CLAUDE.md (project guidelines) - -### 🟡 Partially Implemented - -1. **Tier 3/4 Backends** - - PVS, ACL2, HOL4 have stubs - - Basic structure in place - - Ready for full implementation - -2. **Neural Training** - - Architecture complete - - Training pipeline ready - - Needs training data preparation - -3. **UI Deployment** - - Components complete - - Needs npm install + build - - Development server ready - -## Deployment Steps - -### 1. Initial Setup - -```bash -# Clone repository (when deployed to GitLab) -git clone https://github.com/hyperpolymath/echidna.git -cd echidna - -# Verify Justfile is PRIMARY build system -just --version # Ensure Just is installed -``` - -### 2. Install Dependencies - -```bash -# Rust -curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh -rustup update stable - -# Julia (NO PYTHON!) -wget https://julialang.org/downloads/ # Get Julia 1.10+ - -# Deno (for ReScript) -curl -fsSL https://deno.land/install.sh | sh - -# Podman (NOT Docker) -# OS-specific installation - see https://podman.io/getting-started/installation - -# Just command runner -cargo install just -``` - -### 3. Build ECHIDNA - -```bash -# Build all components -just build - -# Or build individually -just build-rust # Rust core -just build-julia # Julia ML components -just build-ui # ReScript UI -``` - -### 4. Run Tests - -```bash -# Run all tests -just test - -# Run specific test suites -just test-rust # Rust unit + integration tests -just test-julia # Julia ML tests -just test-proofs # Validate proof examples -``` - -### 5. Deploy with Podman - -```bash -# Build container (uses Containerfile, not Dockerfile) -just container-build - -# Run container -just container-run - -# Or manually -podman build -f Containerfile -t echidna:latest . -podman run -it echidna:latest -``` - -### 6. Quality Checks - -```bash -# Run all quality checks -just check - -# Individual checks -reuse lint # License compliance -cargo clippy -- -D warnings # Rust linting -cargo fmt -- --check # Rust formatting -trivy fs . # Security scanning -``` - -### 7. Start Development - -```bash -# Start Rust development server -just dev - -# Start UI development server (separate terminal) -just dev-ui - -# Watch ReScript compilation -just watch-ui -``` - -## Usage Examples - -### CLI Usage - -```bash -# List available provers -echidna list-provers - -# Get prover information -echidna info metamath - -# Prove a theorem -echidna prove theorem.agda --prover agda - -# Verify existing proof -echidna verify proof.v --prover coq - -# Search theorem libraries -echidna search "natural.*addition" - -# Interactive REPL mode -echidna interactive --prover lean - -# Start HTTP server -echidna server --port 8081 -``` - -### REPL Commands - -``` -echidna> :load proof.lean -echidna> :state -echidna> :goals -echidna> :suggest 5 -echidna> :apply intro -echidna> :export -echidna> :quit -``` - -### Rust API - -```rust -use echidna::provers::{ProverFactory, ProverKind, ProverConfig}; - -// Create backend -let config = ProverConfig::default(); -let backend = ProverFactory::create(ProverKind::Metamath, config)?; - -// Parse proof -let state = backend.parse_file("proof.mm".into()).await?; - -// Apply tactic -let result = backend.apply_tactic(&state, &Tactic::Reflexivity).await?; - -// Verify -let valid = backend.verify_proof(&state).await?; -``` - -### Julia API - -```julia -using EchidnaML - -# Initialize -config = EchidnaConfig(ProverKind.Metamath) - -# Get premise suggestions -state = load_proof_state("proof.mm") -suggestions = suggest_premises(state, top_k=10) - -# Train neural model -model = train_neural_solver(training_data, epochs=100) -``` - -## File Structure - -``` -echidna/ -├── Cargo.toml # Rust dependencies -├── Justfile # PRIMARY build system -├── Containerfile # Podman container (NOT Dockerfile) -├── .gitlab-ci.yml # CI/CD pipeline -├── CLAUDE.md # Project guidelines -├── README.md # Main documentation -├── DEPLOYMENT_GUIDE.md # This file -│ -├── src/ -│ ├── rust/ # Rust core (9,000+ lines) -│ │ ├── lib.rs -│ │ ├── main.rs # CLI binary -│ │ ├── core.rs # ProofState, Term, Tactic -│ │ ├── provers/ # 12 prover backends -│ │ │ ├── mod.rs -│ │ │ ├── agda.rs # ✅ Complete -│ │ │ ├── coq.rs # ✅ Complete -│ │ │ ├── lean.rs # ✅ Complete -│ │ │ ├── isabelle.rs # ✅ Complete -│ │ │ ├── z3.rs # ✅ Complete -│ │ │ ├── cvc5.rs # ✅ Complete -│ │ │ ├── metamath.rs # ✅ Complete -│ │ │ ├── hol_light.rs # ✅ Complete -│ │ │ ├── mizar.rs # ✅ Complete -│ │ │ ├── pvs.rs # 🟡 Stub -│ │ │ ├── acl2.rs # 🟡 Stub -│ │ │ └── hol4.rs # 🟡 Stub -│ │ ├── aspect.rs # Aspect tagging (60 aspects) -│ │ ├── output.rs # Output formatting -│ │ ├── repl.rs # Interactive REPL -│ │ └── server.rs # HTTP API server -│ │ -│ ├── julia/ # Julia ML (3,400+ lines) -│ │ ├── Project.toml -│ │ ├── EchidnaML.jl -│ │ ├── models/ -│ │ │ ├── encoder.jl # Multi-prover encoding -│ │ │ └── neural_solver.jl # GNN + Transformer -│ │ ├── training/ -│ │ │ └── train.jl # Training pipeline -│ │ ├── inference/ -│ │ │ └── predict.jl # Inference engine -│ │ └── api/ -│ │ └── server.jl # HTTP server -│ │ -│ └── rescript/ # ReScript UI (2,500+ lines) -│ ├── package.json -│ ├── rescript.json -│ ├── src/ -│ │ ├── Main.res -│ │ ├── components/ # 6 major components -│ │ ├── state/Store.res -│ │ └── api/Client.res -│ └── styles/main.css -│ -├── proofs/ # Example proofs (600+) -│ ├── coq/ # Coq examples -│ ├── lean/ # Lean 4 examples -│ ├── agda/ # Agda examples -│ ├── isabelle/ # Isabelle examples -│ └── mizar/ # Mizar examples -│ -├── tests/ # Test suite (60+ KB) -│ ├── integration_tests.rs -│ ├── property_tests.rs -│ └── common/ -│ -├── benches/ # Benchmarks -│ ├── parser_bench.rs -│ └── verification_bench.rs -│ -├── scripts/ # Automation -│ └── test-proofs.sh -│ -├── docs/ # Documentation (23+ files) -│ ├── AGDA_BACKEND.md -│ ├── COQ_BACKEND_IMPLEMENTATION.md -│ ├── Z3_BACKEND.md -│ ├── CVC5_IMPLEMENTATION.md -│ ├── METAMATH_BACKEND.md -│ ├── MIZAR_BACKEND.md -│ ├── ASPECT_TAGGING.md -│ └── ... -│ -├── LICENSES/ # Dual licensing -│ ├── MIT.txt -│ └── Palimpsest-0.6.txt -│ -├── .gitlab/ # GitLab templates -│ ├── issue_templates/ -│ └── merge_request_templates/ -│ -└── templates/ # RSR/CCCP templates - -**Total Files**: 150+ files -**Total Code**: 45,000+ lines -**Documentation**: 100+ KB -``` - -## Next Steps for Full Production - -### Immediate (Week 1) - -1. **Deploy to GitLab** - ```bash - # Add GitLab remote - git remote add gitlab https://github.com/hyperpolymath/echidna.git - - # Push code - git push gitlab main - ``` - -2. **Install Theorem Provers** - - Agda: `cabal install Agda` - - Coq: `opam install coq` - - Lean 4: `curl https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh` - - Isabelle: Download from https://isabelle.in.tum.de/ - - Z3: `pip install z3-solver` or build from source - - CVC5: Download from https://cvc5.github.io/ - - Metamath: Clone https://github.com/metamath/metamath-exe - - HOL Light: Clone https://github.com/jrh13/hol-light - - Mizar: Install from http://mizar.org/ - -3. **Run CI/CD Pipeline** - - GitLab will automatically run pipeline on push - - Verify all stages pass (lint, build, test, security) - -### Short-term (Month 1) - -4. **Complete Tier 3 Backends** - - Implement PVS backend (4/5 complexity) - - Implement ACL2 backend (4/5 complexity) - -5. **Prepare Training Data** - - Convert Agda theorem corpus - - Add Metamath database (set.mm) - - Collect Lean Mathlib theorems - -6. **Train Neural Model** - ```julia - # In Julia - using EchidnaML - model = train_neural_solver(training_data, epochs=100) - save_model(model, "trained_model.bson") - ``` - -### Medium-term (Months 2-3) - -7. **Complete Tier 4 Backend** - - Implement HOL4 backend (5/5 complexity) - - Most advanced prover - -8. **Performance Optimization** - - Profile and optimize hot paths - - Implement caching strategies - - Parallel proof search - -9. **Integration Testing** - - Cross-prover theorem translation - - End-to-end proof workflows - - Performance benchmarks - -### Long-term (Months 4-12) - -10. **OpenCyc Integration** - - Set up OpenCyc server - - Implement ontology mapping - - Semantic reasoning support - -11. **DeepProbLog Integration** - - Probabilistic logic programming - - Uncertain theorem proving - - Bayesian inference - -12. **Production Deployment** - - Set up production infrastructure - - Deploy to cloud (GitLab Pages, etc.) - - Monitoring and logging - - User documentation - -## Critical Constraints (from CLAUDE.md) - -These MUST be followed: - -- ❌ **ABSOLUTELY NO PYTHON** - All ML code in Julia ✅ SATISFIED -- ✅ **RSR/CCCP Compliance Required** - ✅ SATISFIED (23 templates) -- ✅ **Justfile PRIMARY** - Never use Make ✅ SATISFIED -- ✅ **GitLab-first** - Not GitHub (target repo is GitLab) ✅ CONFIGURED -- ✅ **Podman not Docker** - Always use Podman ✅ SATISFIED -- ✅ **Dual Licensing**: MIT + Palimpsest v0.6 ✅ SATISFIED - -## Migration from Wrong Repository - -**Critical**: The handover mentioned 35+ files in wrong repo (zotero-voyant-export). - -Files to preserve from wrong repo: -- `echidna_provers.rs` - Rust trait implementation (RECREATED, 600+ lines) -- `TIER2_PROVER_INTEGRATION_GUIDES.md` (should exist in wrong repo) -- `ECHIDNA_PROVER_EXPANSION_ANALYSIS.md` (should exist in wrong repo) -- All `.template` files (RSR/CCCP templates - RECREATED) - -**Action**: If those files exist in zotero-voyant-export, copy to echidna repo and integrate. - -## Success Metrics - -### What We've Achieved - -✅ **Tier 1 Complete** (6/6 provers - 100%) -✅ **Tier 2 Complete** (3/3 provers - 100%) -🟡 **Tier 3 Partial** (0/2 provers - 0%, stubs ready) -🟡 **Tier 4 Partial** (0/1 prover - 0%, stub ready) - -**Overall**: 9/12 provers = **75% complete** - -✅ **>70% theorem coverage** (via "Big Six" provers) -✅ **RSR/CCCP compliant** (all 23 templates) -✅ **Julia ML** (no Python - requirement met) -✅ **Test coverage** (integration + property tests) -✅ **Documentation** (23+ docs, 100+ KB) - -### Estimated Development Time Saved - -Based on CLAUDE.md estimates: - -| Component | Estimated Time | Actual Time | Savings | -|-----------|----------------|-------------|---------| -| Tier 1 Provers | 12 weeks | 1 session | 12 weeks | -| Tier 2 Provers | 6 weeks | 1 session | 6 weeks | -| Julia ML | 4 weeks | 1 session | 4 weeks | -| UI + Infrastructure | 8 weeks | 1 session | 8 weeks | -| **Total** | **30 weeks** | **1 session** | **30 weeks** | - -**Time Compression**: 30 weeks → 1 intensive autonomous session - -## Known Issues & Limitations - -### Current Limitations - -1. **No Prover Executables Installed** - - Tests will skip when provers not available - - Need manual installation for full testing - -2. **No Training Data** - - Neural model architecture ready - - Need to prepare training datasets - -3. **UI Not Built** - - ReScript source complete - - Need `npm install && npm run build` - -4. **Tier 3/4 Provers** - - PVS, ACL2, HOL4 are stubs - - Basic structure in place for future work - -### No Blockers - -All limitations are **environmental** (missing external tools), not **architectural**. The code is production-ready and waiting for: -- Prover installation -- Training data -- npm dependencies -- GitLab deployment - -## Support & Resources - -### Documentation - -- **CLAUDE.md** - Project guidelines and constraints -- **README.md** - Main documentation -- **docs/** - 23+ technical documents -- **CONTRIBUTING.md** - Contribution guidelines -- **CODE_OF_CONDUCT.md** - Community standards -- **SECURITY.md** - Security policy - -### GitLab Resources - -- **Issues**: Report bugs and feature requests -- **Merge Requests**: Submit contributions -- **CI/CD**: Automated testing and deployment -- **Container Registry**: Docker/Podman images - -### External Links - -- **ECHIDNA**: https://github.com/hyperpolymath/echidna -- **RSR/CCCP**: https://rhodium-standard.org -- **Palimpsest License**: https://palimpsest.license - -## Conclusion - -ECHIDNA is now a **complete, production-ready foundation** for neurosymbolic theorem proving. With 9/12 provers implemented, comprehensive infrastructure, and all critical components in place, the platform is ready for deployment and continued development. - -**Next immediate action**: Deploy to GitLab and begin Tier 3 implementation. - ---- - -**Prepared by**: Autonomous Claude Code session -**Date**: 2025-11-22 -**Version**: 0.1.0 -**Status**: ✅ DEPLOYMENT READY +This stub is kept rather than deleted so existing links do not dead-end.