Add MVP dependencies and best-effort CI

Author: Jonathan D.A. Jewell

.github/workflows/mvp-smoke.yml

@@ -0,0 +1,37 @@
+# SPDX-License-Identifier: AGPL-3.0-or-later
+name: MVP Smoke (Best Effort)
+
+on:
+  push:
+    branches: [main]
+  pull_request:
+    branches: [main]
+
+permissions: read-all
+
+env:
+  CARGO_TERM_COLOR: always
+
+jobs:
+  mvp-smoke:
+    name: MVP Smoke
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+    steps:
+      - name: Checkout repository
+        uses: actions/checkout@b4ffde65f46336ab88eb53be808477a3936bae11 # v4
+
+      - name: Setup Rust toolchain
+        uses: dtolnay/rust-toolchain@6d9817901c499d6b02debbb57edb38d33daa680b # stable
+        with:
+          toolchain: stable
+
+      - name: Cache Cargo
+        uses: Swatinem/rust-cache@ad397744b0d591a723ab90405b7247fac0e6b8db # v2
+
+      - name: Build release
+        run: cargo build --release
+
+      - name: MVP smoke checks (best effort)
+        run: just --justfile Justfile mvp-env

Justfile

@@ -79,3 +79,7 @@ pre-commit: fmt-check lint test
 # MVP 1.0 smoke checks
 mvp:
     ./scripts/mvp-smoke.sh
+
+# MVP 1.0 dependency checklist (best-effort)
+mvp-env:
+    ./scripts/mvp-smoke.sh || true

README.adoc

@@ -188,6 +188,16 @@ just security      # Trivy, cargo-audit
 just coverage      # Test coverage
 ```
 
+=== MVP Smoke (Best Effort)
+
+```bash
+# MVP smoke checks (reports missing provers, does not fail)
+just mvp
+
+# Dependency checklist (always non-fatal)
+just mvp-env
+```
+
 == Documentation
 
 - link:CONTRIBUTING.md[Contributing Guidelines]

docs/MVP-1.0-DEPS.adoc

@@ -0,0 +1,76 @@
+= ECHIDNA MVP 1.0 Dependencies
+:toc: macro
+:toclevels: 2
+
+This document lists external prover dependencies for the 1.0 MVP and how to verify them.
+
+TOC::[]
+
+== Core Provers (12)
+
+|===
+| Prover | Executable | Notes
+
+| Agda
+| `agda`
+| Install via system package or Agda tooling.
+
+| Coq
+| `coqtop`
+| Coq/Rocq interactive toplevel.
+
+| Lean
+| `lean`
+| Lean 4 CLI (elan recommended).
+
+| Isabelle
+| `isabelle`
+| Isabelle server + tools.
+
+| Z3
+| `z3`
+| SMT solver.
+
+| CVC5
+| `cvc5`
+| SMT solver.
+
+| Metamath
+| `metamath`
+| Metamath verifier.
+
+| HOL Light
+| `hol-light`
+| HOL Light executable wrapper.
+
+| Mizar
+| `mizar`
+| Mizar system (verifier + MML).
+
+| PVS
+| `pvs`
+| PVS environment.
+
+| ACL2
+| `acl2`
+| ACL2 environment.
+
+| HOL4
+| `hol4`
+| HOL4 environment.
+|===
+
+== Quick Check
+
+Run:
+
+----
+just mvp
+----
+
+Missing executables are reported explicitly. This is expected on dev machines.
+
+== Optional Helpers
+
+* `just mvp-env` (best-effort checklist) prints what is missing.
+* Prefer installing provers locally for full MVP validation.

docs/MVP-1.0.adoc

@@ -53,6 +53,8 @@ TOC::[]
 
 * Script exists to check prover executables are available (or clearly report missing).
 * Script runs minimal prove/verify for each prover when available.
+* Dependency checklist is documented in `docs/MVP-1.0-DEPS.adoc`.
+* Dependency checklist is documented in `docs/MVP-1.0-DEPS.adoc`.
 
 == Release Prep