Skip to content

roadmap: Pre-built Podman images for all 12 provers — gated on each prover's Containerfile build #61

Description

@hyperpolymath

Origin

ROADMAP.adoc §"Remaining Work (v0.2.0 -- Q1-Q2 2026)", "Deployment (MEDIUM PRIORITY)" (line 132):

  • Pre-built Podman images for all 12 provers

The "12 provers" count matches the canonical core-prover count per echidna docs/PROVER_COUNT.md (12 core; 128 total).

Scope

Per-prover Containerfile + image-publishing CI for the 12 core provers:

  • Containerfile.<prover> per backend with reproducible build (pinned upstream source/binary, SHAKE3-512 verified per echidna's integrity layer)
  • GitHub Actions / Forgejo Actions workflow that builds and publishes to GHCR on each upstream release of the prover
  • Image-pull tests in the echidnabot smoke suite (referenced in compose-spec issue roadmap: Docker Compose + PostgreSQL deployment — gated on upstream PostgreSQL CI image #60)
  • Versioning convention: ghcr.io/hyperpolymath/echidnabot-prover-<name>:<upstream-version>

PR count: ~12+ (one per prover Containerfile, plus the publish workflow, plus image-pull tests).

Dependencies

  • UPSTREAM-BLOCKED per-prover: each of the 12 core provers needs its upstream to ship a buildable source / binary. Several core provers (Lean 4, Coq, Isabelle, Z3, CVC5) already publish official images and need only a thin wrapper; specialised tools (Metamath, HOL Light, Mizar) need bespoke Containerfile work
  • Sibling: Docker Compose setup (issue roadmap: Docker Compose + PostgreSQL deployment — gated on upstream PostgreSQL CI image #60) — the prebuilt images are what the compose spec consumes
  • No echidnabot-internal blocker; this is mostly infrastructure-and-images work

Why filed

To make the v0.2.0 Deployment commitment trackable. Today the bullet lives only as a checklist line in ROADMAP.adoc with no issue. The "12 prover images" track is the gating dependency for any horizontal-scale deploy (compose, K8s) and deserves its own tracker so the per-prover blockers can be linked individually.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew capability or improvement to existing behaviourmeta:roadmapForward planning; not yet actionable work

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions