From 2f9cab246fe729d5d75c0d2551251bb1dae2ef45 Mon Sep 17 00:00:00 2001 From: arena-agent <297053741+arena-agent@users.noreply.github.com> Date: Fri, 9 Oct 2026 19:09:41 +0000 Subject: [PATCH] feat(corpus): wire all 17 adapters into the CLI dispatcher `echidna corpus ingest --adapter` only dispatched agda, coq, lean and idris2, although src/rust/corpus/ ships 17 ingest adapters. Add the remaining 13 (acl2_books, dafny, fstar, hol4, hol_light, isabelle, metamath, minif2f, mizar, proofnet, smtlib, tptp, why3) to the match, list all 17 in the unknown-adapter error and the --adapter help text. Adds tests/corpus_cli_dispatch.rs: every advertised name must reach its adapter (no "Unknown corpus adapter" fallthrough), and an unknown name must exit non-zero listing the supported set. Co-authored-by: arena-agent <297053741+arena-agent@users.noreply.github.com> --- src/rust/main.rs | 32 +++++++++++++- tests/corpus_cli_dispatch.rs | 82 ++++++++++++++++++++++++++++++++++++ 2 files changed, 112 insertions(+), 2 deletions(-) create mode 100644 tests/corpus_cli_dispatch.rs diff --git a/src/rust/main.rs b/src/rust/main.rs index 33e5f686..889f67e8 100644 --- a/src/rust/main.rs +++ b/src/rust/main.rs @@ -241,7 +241,9 @@ enum CorpusOp { /// Path to the project root. #[arg(short, long)] root: PathBuf, - /// Adapter to use (currently only `agda`). + /// Adapter to use: agda, coq, lean, idris2, acl2_books, dafny, + /// fstar, hol4, hol_light, isabelle, metamath, minif2f, mizar, + /// proofnet, smtlib, tptp, why3. #[arg(short, long, default_value = "agda")] adapter: String, /// Where to write the JSON index. Defaults to @@ -1317,9 +1319,35 @@ fn corpus_command(op: CorpusOp, formatter: &OutputFormatter) -> Result<()> { .with_context(|| format!("lean ingest of {}", root.display()))?, "idris2" | "idris" => corpus::idris2::ingest(&root) .with_context(|| format!("idris2 ingest of {}", root.display()))?, + "acl2_books" => corpus::acl2_books::ingest(&root) + .with_context(|| format!("acl2_books ingest of {}", root.display()))?, + "dafny" => corpus::dafny::ingest(&root) + .with_context(|| format!("dafny ingest of {}", root.display()))?, + "fstar" => corpus::fstar::ingest(&root) + .with_context(|| format!("fstar ingest of {}", root.display()))?, + "hol4" => corpus::hol4::ingest(&root) + .with_context(|| format!("hol4 ingest of {}", root.display()))?, + "hol_light" => corpus::hol_light::ingest(&root) + .with_context(|| format!("hol_light ingest of {}", root.display()))?, + "isabelle" => corpus::isabelle::ingest(&root) + .with_context(|| format!("isabelle ingest of {}", root.display()))?, + "metamath" => corpus::metamath::ingest(&root) + .with_context(|| format!("metamath ingest of {}", root.display()))?, + "minif2f" => corpus::minif2f::ingest(&root) + .with_context(|| format!("minif2f ingest of {}", root.display()))?, + "mizar" => corpus::mizar::ingest(&root) + .with_context(|| format!("mizar ingest of {}", root.display()))?, + "proofnet" => corpus::proofnet::ingest(&root) + .with_context(|| format!("proofnet ingest of {}", root.display()))?, + "smtlib" => corpus::smtlib::ingest(&root) + .with_context(|| format!("smtlib ingest of {}", root.display()))?, + "tptp" => corpus::tptp::ingest(&root) + .with_context(|| format!("tptp ingest of {}", root.display()))?, + "why3" => corpus::why3::ingest(&root) + .with_context(|| format!("why3 ingest of {}", root.display()))?, other => { return Err(anyhow::anyhow!( - "Unknown corpus adapter '{}' (supported: agda, coq, lean, idris2)", + "Unknown corpus adapter '{}' (supported: agda, coq, lean, idris2, acl2_books, dafny, fstar, hol4, hol_light, isabelle, metamath, minif2f, mizar, proofnet, smtlib, tptp, why3)", other )) }, diff --git a/tests/corpus_cli_dispatch.rs b/tests/corpus_cli_dispatch.rs new file mode 100644 index 00000000..f5c519d4 --- /dev/null +++ b/tests/corpus_cli_dispatch.rs @@ -0,0 +1,82 @@ +// SPDX-License-Identifier: MPL-2.0 + +//! Dispatch tests for `echidna corpus ingest --adapter `. +//! +//! Every adapter name advertised in the CLI must reach its adapter's +//! `ingest` function rather than the "Unknown corpus adapter" fallback. +//! An empty project root is used so no real prover corpus is needed; the +//! adapters may legitimately find nothing and fail, but the dispatch error +//! must never appear for a supported name. + +use std::path::Path; +use std::process::{Command, Output}; + +const SUPPORTED: &[&str] = &[ + "agda", + "coq", + "lean", + "idris2", + "acl2_books", + "dafny", + "fstar", + "hol4", + "hol_light", + "isabelle", + "metamath", + "minif2f", + "mizar", + "proofnet", + "smtlib", + "tptp", + "why3", +]; + +fn ingest(dir: &Path, adapter: &str) -> Output { + let root = dir.join("project"); + std::fs::create_dir_all(&root).expect("create project root"); + let out = dir.join(format!("{adapter}.json")); + Command::new(env!("CARGO_BIN_EXE_echidna")) + .current_dir(dir) + .args(["corpus", "ingest", "--root"]) + .arg(&root) + .args(["--adapter", adapter, "--out"]) + .arg(&out) + .output() + .expect("run echidna corpus ingest") +} + +fn combined(out: &Output) -> String { + format!( + "{}{}", + String::from_utf8_lossy(&out.stdout), + String::from_utf8_lossy(&out.stderr) + ) +} + +#[test] +fn every_advertised_adapter_is_dispatched() { + let tmp = tempfile::tempdir().expect("tempdir"); + for adapter in SUPPORTED { + let out = ingest(tmp.path(), adapter); + let text = combined(&out); + assert!( + !text.contains("Unknown corpus adapter"), + "adapter `{adapter}` fell through to the unknown-adapter arm: {text}" + ); + } +} + +#[test] +fn unknown_adapter_is_rejected() { + let tmp = tempfile::tempdir().expect("tempdir"); + let out = ingest(tmp.path(), "not_a_real_adapter"); + assert!(!out.status.success(), "unknown adapter must exit non-zero"); + let text = combined(&out); + assert!( + text.contains("Unknown corpus adapter 'not_a_real_adapter'"), + "unexpected error text: {text}" + ); + for adapter in SUPPORTED { + assert!(text.contains(adapter), "error should list `{adapter}`: {text}"); + } +}