From e9811d11caebc0eac5ddc19a38d39a5aeb09d540 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 29 Jul 2026 08:15:56 +0100 Subject: [PATCH] docs: document hosting topology for humans and machines MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Adds the missing map of where ECHIDNA actually runs, in both registers: - docs/HOSTING.md — the three public surfaces (Cloudflare Pages for the site, Hetzner behind Caddy for the API, Cloudflare Email Routing for contact), how each is built, and the two constraints that bite when editing the site: the SSG hard-fails on a11y violations, and its copyTree is text-only so binaries need cp. - .machine_readable/deployment.a2ml — the same topology as structured data, including the API's limits and the risks of exposing an unauthenticated service that spawns provers on user input. Both record the two current blockers honestly: repository-wide Actions startup_failure (a minimal probe workflow fails identically, so it is not a workflow-file fault), and an apex that resolves to Cloudflare but has no origin behind it. Both also carry the diagnostic that keeps catching people out: a workflow which fails at startup registers no check run, so gh pr checks reports success while every gate is dead — and a workflow listed by path rather than name has never been parsed. docs/deployment/DEPLOYMENT_GUIDE.md is reduced to a superseded stub. It described a 2025-11 v0.1.0 deployment whose next step was 'deploy to GitLab', referenced an unrelated migration, and quoted a fixed prover count that the canonical-reference policy forbids in prose. Kept as a stub so existing links do not dead-end. Verified: .githooks/validate-a2ml.sh passes (exit 0) with the new manifest present. Co-Authored-By: Claude Opus 5 --- .machine_readable/deployment.a2ml | 116 +++++ docs/HOSTING.md | 121 ++++++ docs/deployment/DEPLOYMENT_GUIDE.md | 647 +--------------------------- 3 files changed, 254 insertions(+), 630 deletions(-) create mode 100644 .machine_readable/deployment.a2ml create mode 100644 docs/HOSTING.md 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.