ArghDA M10: Mizar adapter — heavy tail complete (a real verify, not detect-only)

[hyperpolymath]

What

The third and last heavy-tail backend — and the "highest uncertainty" one. It turned out tractable: Mizar 8.1.15's statically-linked i386 verifier runs on x86_64 with no 32-bit libs, so M10 is a genuine dogfooded verify, not the planned detect-only stub.

arghda is now a nine-backend prover-parametric workspace (agda, agda-cubical, idris2, lean4, coq, isabelle, mizar as Assistants; z3, cvc5 as Solvers). The heavy tail (M8–M10) is complete.

How

Adapter — src/prover/mizar.rs (Mizar)

• Assistant kind, extensions [miz], command verifier.
• No lint pack, by design: Mizar has no sorry/admit escape hatch — an incomplete proof is simply a verifier error, and a normal article cannot introduce axioms — so soundness is the verifier and the verdict is binary.
• check_file, ground-truthed vs Mizar 8.1.15: MIZFILES unset → Unavailable (the MML data dir is the precondition — honest, never a fabricated pass); binary absent → Unavailable; otherwise copy the .miz (+ siblings) to a temp dir, run accom then verifier (env MIZFILES), and read the sibling <stem>.err — empty + exit 0 → Proven, non-empty / exit ≠ 0 → Error (Mizar reports errors in .err, the authoritative signal).
• Imports: the environ block's directives (vocabularies/notations/theorems/…), lower-cased to match on-disk stems; MML references are external and dropped.
• Roots: none — Mizar has no aggregator convention (honest empty set).
• probe() overridden to verifier -v.

Provisioning at source: install_mizar upgraded from a warn-stub to a real installer (static i386 tarball from mizar.uwb.edu.pl → /opt/mizar + symlinks), with a MIZAR_TAR pin and a doctor verify line.

Wired: backend_for "mizar", KNOWN_BACKENDS, all four --backend help strings, the CLI about line.

Verification (actually run)

• cargo fmt --check — clean
• cargo clippy --all-targets -- -D warnings — clean
• cargo test — 167 pass (+6 mizar unit, +2 mizar integration; the graph tests are hermetic — environ text only, run tool-less)
• bash scripts/check-spdx.sh . — OK

Dogfooded against real Mizar 8.1.15 (MIZFILES=/opt/mizar):

fixture	arghda check --backend mizar
good.miz (theorem for X being set holds X = X, importing XBOOLE_0)	proven
broken.miz (undefined reference)	error
empty.miz (empty environ+begin)	proven

• arghda doctor → [OK] mizar assistant Mizar Ver. 8.1.15

Scope

M10 at 85%. Remaining: local-article cross-references need prel export (miz2prel) for the throwaway session; no root convention.

🤖 Generated with Claude Code

https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7

---

Generated by Claude Code