Containerfile.full claims "all tier 1-4 provers" but ships only Z3/Agda/Lean/Metamath

[hyperpolymath]

Summary

.containerization/Containerfile.full is documented as including all tier 1-4 provers but the built image only contains four: Z3, Agda, Lean 4, Metamath. Coq, CVC5, Idris2, Isabelle, Dafny, F*, and every tier 3-4 prover are absent. Users asking for prover=Coq etc. through /api/verify get 422: Failed to run coqc.

Reproduce

Build the full image and ask for any non-Z3/Agda/Lean/Metamath prover:

podman build -f .containerization/Containerfile.full -t echidna:full .
podman run --rm -p 8090:8090 echidna:full server --port 8090 --host 0.0.0.0
curl -X POST http://localhost:8090/api/verify \
  -H "Content-Type: application/json" \
  -d '{"prover":"Coq","content":"Theorem t : 0+0=0. Proof. reflexivity. Qed."}'

Response: {"error":"Verification error: Failed to run coqc"}

Root cause

The "Stage 4: Prover Installer" section of Containerfile.full installs only:

• z3 (via apt)
• ghc + cabal-install (as dependency builders for Agda)
• Agda (via cabal)
• Lean 4 (via elan)
• metamath (built from source)

No coqc, cvc5, idris2, isabelle, dafny, fstar, hol_light, mizar, hol4, pvs, acl2, tlaps, vampire, eprover, etc. are installed. The ProverKind enum in src/rust/provers/ declares support for many of these, but calling them 500s at runtime.

Meanwhile the header comment reads:

# ECHIDNA Full Containerfile - Includes all Tier 1-4 provers

Expected

Either:

1. Fix the container: add the missing provers. Coq (apt: coq), CVC5 (apt or GitHub release), Idris2 (via pack), Isabelle (direct install), Dafny (.NET), F* (opam), etc.
2. Fix the docs: rename to Containerfile.standard or similar; update header comment to list exactly which provers are shipped.

Impact

Downstream deploys (nesy-solver playground, Phase E3) that expose prover as a user choice get runtime failures for anything but Z3/Agda/Lean/Metamath, with confusing error messages. Playground users submitting Coq see "Failed to run coqc" which looks like a misconfiguration rather than a missing dependency.

Related

• Z3 /api/verify rejects valid SMT-LIB queries: treats user input as proof obligation #10 (Z3 /api/verify verdict semantics)

[hyperpolymath]

Resolved in fbad8e6 by aligning the Containerfile wording with what is actually bundled. now documents a curated prover set and explicitly lists current bundled provers (), instead of claiming all tier 1-4 provers.

[hyperpolymath]

Resolution details (clean copy):

• Addressed in commit fbad8e6.
• Containerfile.full wording now matches the shipped payload.
• It now documents a curated set and explicitly lists current bundled provers:
  • Z3
  • Agda
  • Lean 4
  • Metamath
  • Isabelle2025-2
• Removed the inaccurate blanket claim that all Tier 1-4 provers are included.