diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index ed50439..9cf8ce7 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -11,7 +11,7 @@ status = "active" # active | paused | archived [project-context] name = "arghda-core" -purpose = "Multi-backend proof-workspace manager — the 'Flying Logic for provers/solvers' engine. A four-state triage workspace (inbox/working/proven/rejected) as file moves, per-backend lint packs targeting the silent-failure class, a backend-parametric import-graph DAG, a demote-only status-propagating reasoning graph, and a JSON + event-stream contract a visual layer (arghda-studio) consumes. Eight backends across both interaction models (Agda, Cubical-Agda, Idris2, Lean4, Coq/Rocq, Isabelle/HOL assistants; Z3, CVC5 solvers). It never proves anything itself; the tools do." +purpose = "Multi-backend proof-workspace manager — the 'Flying Logic for provers/solvers' engine. A four-state triage workspace (inbox/working/proven/rejected) as file moves, per-backend lint packs targeting the silent-failure class, a backend-parametric import-graph DAG, a demote-only status-propagating reasoning graph, and a JSON + event-stream contract a visual layer (arghda-studio) consumes. Nine backends across both interaction models (Agda, Cubical-Agda, Idris2, Lean4, Coq/Rocq, Isabelle/HOL, Mizar assistants; Z3, CVC5 solvers). It never proves anything itself; the tools do." completion-percentage = 92 [position] @@ -50,7 +50,7 @@ milestones = [ { name = "M7: Echidna dispatch seam (optional route to orchestrator :8090, same Outcome)", completion = 70 }, { name = "M8: Coq/Rocq adapter (--heavy provisioning; Section-aware postulate classifier)", completion = 90 }, { name = "M9: Isabelle adapter (--heavy; dogfood tropical-resource-typing .thy)", completion = 90 }, - { name = "M10: Mizar adapter (detect-only first; highest uncertainty)", completion = 0 }, + { name = "M10: Mizar adapter (detect-only first; highest uncertainty)", completion = 85 }, { name = "M11: studio JSON freeze (reason/0.1) + Groove manifest", completion = 100 }, ] # M0 provisioning verified in-container 2026-07-01: agda 2.6.3 (+stdlib v2.3 @@ -63,8 +63,14 @@ milestones = [ # /opt, symlinked to /usr/local/bin/isabelle; `isabelle version` → Isabelle2025; # doctor [OK] isabelle. NB the provision script's Isabelle URL was stale # (/dist/Isabelle2024… 404s once a newer release is current) — FIXED at source -# to the archived /website-/dist/ path + bumped to Isabelle2025. Mizar -# remains scripted (behind --mizar) but not installed (distribution manual). +# to the archived /website-/dist/ path + bumped to Isabelle2025. MIZAR NOW +# INSTALLED (2026-07-01) — the "highest uncertainty" one turned out tractable: +# mizar.org → mizar.uwb.edu.pl ships a STATICALLY-LINKED i386 tarball +# (mizar-8.1.15_5.94.1493) that runs on x86_64 with NO 32-bit libs; unpacked to +# /opt/mizar (binaries + MML flat), verifier/accom symlinked to /usr/local/bin; +# `verifier -v` → Mizar 8.1.15; doctor [OK] mizar. Runtime needs MIZFILES= +# /opt/mizar. The provision script's install_mizar was upgraded from a warn-stub +# to a real installer + verify line. # Remaining M0: `arghda doctor` Rust subcommand (interim: `just doctor` shells # the script's --verify-only table). # @@ -184,6 +190,33 @@ milestones = [ # doctor → [OK] isabelle assistant Isabelle2025. Remaining 10%: session- # qualified / relative-path imports + dependency-ordered multi-session builds. # +# M10 landed 2026-07-01 (85%, third heavy-tail backend — and a REAL verify, not +# the planned detect-only). Foundation-first: the "highest uncertainty" one +# turned out tractable — Mizar 8.1.15's static i386 verifier runs on x86_64, so +# it became a genuine dogfood. src/prover/mizar.rs (`Mizar`): Assistant kind, +# extensions [miz], command `verifier`. NO lint pack (empty by design): Mizar +# has no sorry/admit escape hatch — an incomplete proof is just a verifier +# error, and a normal article can't add axioms — so soundness IS the verifier +# (verdict is binary). check_file (ground-truthed vs Mizar 8.1.15): MIZFILES +# unset → Unavailable (the MML data dir is the precondition — honest, not a +# fake pass); binary absent → Unavailable; else copy the .miz (+ siblings) to a +# temp dir, run `accom` then `verifier` (env MIZFILES), and read the sibling +# `.err` — EMPTY + exit 0 → Proven, non-empty/exit≠0 → Error (Mizar +# reports errors in .err, the authoritative signal). Imports: the `environ` +# block directives (vocabularies/notations/theorems/…), lower-cased to match +# on-disk stems; MML refs external/dropped. Roots: none (Mizar has no +# aggregator convention — honest empty set, nothing wired). probe() overridden +# to `verifier -v`. Wired: backend_for "mizar" + KNOWN_BACKENDS + all four +# --backend help strings + about line. Provision script's install_mizar upgraded +# from a warn-stub to a real installer (static-i386 tarball + symlinks) + a +# verify line + MIZAR_TAR pin. 167 tests (+6 mizar unit +2 mizar integration; +# graph tests hermetic — environ text only, run tool-less). DOGFOODED vs real +# Mizar 8.1.15 (MIZFILES=/opt/mizar): check → good=proven (theorem for X being +# set holds X = X, importing XBOOLE_0) / broken=error / empty=proven; doctor → +# [OK] mizar assistant Mizar Ver. 8.1.15. Remaining 15%: local-article +# cross-references need prel export (miz2prel) for the throwaway session; no +# root convention. +# # M7 landed 2026-07-01 (70%): the Echidna dispatch seam — completes the # engine-spine deliverable (M0-M7 + M11). src/dispatch.rs: `Dispatch { Local, # Echidna { base_url } }` + `run(backend, file, include_root) -> Outcome` @@ -347,7 +380,8 @@ actions = [ "M3 follow-on: DONE — `reason --workspace ` sources real verdicts from a `proven/` state (workspace_verdicts) + demotes stale-proven via the content-hash closure. Refinement follow-ons bucket now complete.", "M8 (Coq/Rocq): DONE (90%) — coqc 8.18.0 provisioned + adapter built + dogfooded (proven/admitted/postulated/error) with Section-aware postulate classifier. Remaining: _CoqProject logical paths + dependency-ordered compilation.", "M9 (Isabelle): DONE (90%) — Isabelle2025 provisioned + adapter built + dogfooded (proven/admitted/postulated/error) via session-build; ROOT-based roots, imports-clause edges. Remaining: session-qualified imports + dependency-ordered multi-session builds.", - "M10 (Mizar): next, foundation-first — detect-only first (distribution is manual/niche via mizar.org; provision honestly, check_file → Unavailable until a real toolchain confirms invocation). Then climb to M6 lake-env, M4 totality lint, M7 Echidna client.", + "M10 (Mizar): DONE (85%) — turned out to be a REAL verify, not detect-only: static i386 verifier runs on x86_64; provisioned + adapter (accom+verifier+.err) + dogfooded (proven/error). HEAVY TAIL M8-M10 COMPLETE. Remaining: local-article prel export.", + "Next, climb up: M6 (lake-env/LEAN_PATH so imported Lean files get audited), M4 (totality-hole ?name + per-def partial lint for Idris2), M7 (real Echidna HTTP client, feature-gated). Each its own focused draft PR, gate green, real-tool dogfood where installed.", ] [maintenance-status] @@ -356,14 +390,15 @@ last-result = "pass" # unknown | pass | warn | fail open-warnings = 0 open-failures = 0 # `just check` (fmt-check + clippy -D warnings + build + test + SPDX) green -# post-M9: 118 lib + 41 integration = 159 tests pass. codeql.yml added -# (code-scanning gate fix). M9 Isabelle adapter dogfooded vs real Isabelle2025 -# (proven/admitted/postulated/error; reason --check; imports edges; ROOT roots; -# wired; doctor [OK] isabelle). M8 Coq adapter dogfooded vs real coqc 8.18.0. -# reason --workspace verdicts+staleness dogfooded. Lean #print axioms audit -# dogfooded. doctor/groove/dispatch dogfooded. EIGHT backends now: agda + -# agda-cubical + idris2 + lean4 + coq + isabelle (Assistant), z3 + cvc5 -# (Solver). Dogfooded historically vs echo-types + agda-unused. +# post-M10: 124 lib + 43 integration = 167 tests pass. codeql.yml added +# (code-scanning gate fix). M10 Mizar adapter dogfooded vs real Mizar 8.1.15 +# (proven/error via accom+verifier+.err; MIZFILES=/opt/mizar; doctor [OK] +# mizar). M9 Isabelle dogfooded vs Isabelle2025; M8 Coq dogfooded vs coqc +# 8.18.0. reason --workspace verdicts+staleness dogfooded. Lean #print axioms +# audit dogfooded. doctor/groove/dispatch dogfooded. NINE backends now: agda + +# agda-cubical + idris2 + lean4 + coq + isabelle + mizar (Assistant), z3 + cvc5 +# (Solver). HEAVY TAIL M8-M10 COMPLETE. Dogfooded historically vs echo-types + +# agda-unused. [ecosystem] part-of = ["arghda"] diff --git a/scripts/provision-provers.sh b/scripts/provision-provers.sh index dafe202..98af78c 100644 --- a/scripts/provision-provers.sh +++ b/scripts/provision-provers.sh @@ -36,6 +36,7 @@ LEAN_VER="v4.13.0" # tropical-resource-typing lean-toolch CVC5_VER="1.2.0" # cvc5 static-binary release COQ_VER="8.18.0" # opam (with --heavy) ISABELLE_VER="Isabelle2025" # TUM tarball (with --heavy) +MIZAR_TAR="mizar-8.1.15_5.94.1493-i386-linux.tar" # mizar.uwb.edu.pl (--mizar) STDLIB_DIR=/opt/agda-stdlib CUBICAL_DIR=/opt/agda-cubical @@ -218,8 +219,29 @@ install_isabelle() { } install_mizar() { - have mizar && { log "mizar present"; return; } - warn "mizar not auto-installed: distribution is manual (mizar.org). Flagged as UNKNOWN." + command -v verifier >/dev/null 2>&1 && { log "mizar (verifier) present"; return; } + # mizar.org (→ mizar.uwb.edu.pl) ships a statically-linked i386 tarball that + # runs on x86_64 with no 32-bit libs. Outer tar → mizbin/mizshare/mizdoc + # .tar.gz; binaries + the MML land flat under /opt/mizar. MIZFILES must point + # there at runtime (verifier/accom read the MML from it). + local base="http://mizar.uwb.edu.pl/~softadm/pub/system/i386-linux" + local tar="${MIZAR_TAR}" + log "installing mizar ${tar} (i386 static, ~55 MB)…" + if curl -fSL -m 300 "${base}/${tar}" -o /tmp/mizar.tar 2>/dev/null; then + mkdir -p /opt/mizar && tar -xf /tmp/mizar.tar -C /opt/mizar 2>/dev/null || true + for inner in mizbin.tar.gz mizshare.tar.gz; do + [ -f "/opt/mizar/${inner}" ] && tar -xzf "/opt/mizar/${inner}" -C /opt/mizar 2>/dev/null + done + ln -sf /opt/mizar/verifier /usr/local/bin/verifier + ln -sf /opt/mizar/accom /usr/local/bin/accom + if command -v verifier >/dev/null 2>&1; then + log "mizar installed; set MIZFILES=/opt/mizar to run checks" + else + warn "mizar unpack produced no verifier binary" + fi + else + warn "mizar download failed: ${base}/${tar}" + fi } # ============================================================================= @@ -252,6 +274,7 @@ run_doctor() { verify "zig" zig version verify "coqc" coqc --version verify "isabelle" isabelle version + verify "mizar" verifier -v [ -f "${CUBICAL_DIR}/cubical.agda-lib" ] \ && REPORT+=("OK | cubical-lib | ${CUBICAL_DIR}") \ || REPORT+=("MISSING | cubical-lib | (flag --cubical still works without it)") diff --git a/src/lib.rs b/src/lib.rs index ccffe22..3de4fde 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -35,8 +35,8 @@ pub use graph::{build as build_graph, ImportGraph}; pub use groove::{manifest as groove_manifest, GrooveManifest}; pub use lint::{default_rules, rules_with_config, run_lints, LintRule, RuleConfig}; pub use prover::{ - default_backend, Agda, AgdaCubical, Backend, BackendKind, Coq, Idris2, Isabelle, Lean, Outcome, - Probe, Smt, Verdict, + default_backend, Agda, AgdaCubical, Backend, BackendKind, Coq, Idris2, Isabelle, Lean, Mizar, + Outcome, Probe, Smt, Verdict, }; pub use reason::{ build as build_reason, workspace_verdicts, Junct, ReasonDocument, ReasonEdge, ReasonNode, diff --git a/src/main.rs b/src/main.rs index 431dda0..2ebe2b8 100644 --- a/src/main.rs +++ b/src/main.rs @@ -5,8 +5,8 @@ use anyhow::{Context, Result}; use arghda_core::lint::LintContext; use arghda_core::{ build_dag, build_reason, event, groove_manifest, run_lints, unused, watcher, Agda, AgdaCubical, - Backend, BackendKind, Coq, Dispatch, Idris2, Isabelle, Lean, LintRule, Probe, RuleConfig, Smt, - State, Verdict, Workspace, + Backend, BackendKind, Coq, Dispatch, Idris2, Isabelle, Lean, LintRule, Mizar, Probe, + RuleConfig, Smt, State, Verdict, Workspace, }; use clap::{Parser, Subcommand}; use std::path::{Path, PathBuf}; @@ -24,6 +24,7 @@ const KNOWN_BACKENDS: &[&str] = &[ "lean4", "coq", "isabelle", + "mizar", "z3", "cvc5", ]; @@ -38,10 +39,11 @@ fn backend_for(name: &str) -> Result> { "lean4" => Ok(Box::new(Lean)), "coq" => Ok(Box::new(Coq)), "isabelle" => Ok(Box::new(Isabelle)), + "mizar" => Ok(Box::new(Mizar)), "z3" => Ok(Box::new(Smt::z3())), "cvc5" => Ok(Box::new(Smt::cvc5())), other => anyhow::bail!( - "unknown backend `{other}` (known: agda, agda-cubical, idris2, lean4, coq, isabelle, z3, cvc5)" + "unknown backend `{other}` (known: agda, agda-cubical, idris2, lean4, coq, isabelle, mizar, z3, cvc5)" ), } } @@ -50,7 +52,7 @@ fn backend_for(name: &str) -> Result> { #[command( name = "arghda", version, - about = "Proof-workspace manager for provers/solvers (Agda, Cubical, Idris2, Lean4, Coq, Isabelle, Z3, CVC5)" + about = "Proof-workspace manager for provers/solvers (Agda, Cubical, Idris2, Lean4, Coq, Isabelle, Mizar, Z3, CVC5)" )] struct Cli { #[command(subcommand)] @@ -78,7 +80,7 @@ enum Cmd { #[arg(long)] config: Option, /// Backend: `agda` (default), `agda-cubical`, `idris2`, `lean4`, - /// `coq`, `isabelle`, `z3`, `cvc5`. + /// `coq`, `isabelle`, `mizar`, `z3`, `cvc5`. #[arg(long, default_value = "agda")] backend: String, /// Also run the external `agda-unused` analyser and re-emit its @@ -98,7 +100,7 @@ enum Cmd { #[arg(long)] include_root: Option, /// Backend: `agda` (default), `agda-cubical`, `idris2`, `lean4`, - /// `coq`, `isabelle`, `z3`, `cvc5`. + /// `coq`, `isabelle`, `mizar`, `z3`, `cvc5`. #[arg(long, default_value = "agda")] backend: String, /// Where the check runs: `local` (default) or `echidna[=]` @@ -126,7 +128,7 @@ enum Cmd { #[arg(long)] config: Option, /// Backend: `agda` (default), `agda-cubical`, `idris2`, `lean4`, - /// `coq`, `isabelle`, `z3`, `cvc5`. + /// `coq`, `isabelle`, `mizar`, `z3`, `cvc5`. #[arg(long, default_value = "agda")] backend: String, }, @@ -150,7 +152,7 @@ enum Cmd { #[arg(long)] config: Option, /// Backend: `agda` (default), `agda-cubical`, `idris2`, `lean4`, - /// `coq`, `isabelle`, `z3`, `cvc5`. + /// `coq`, `isabelle`, `mizar`, `z3`, `cvc5`. #[arg(long, default_value = "agda")] backend: String, /// Run the backend on every node to populate REAL prover verdicts diff --git a/src/prover/mizar.rs b/src/prover/mizar.rs new file mode 100644 index 0000000..f4a0fc8 --- /dev/null +++ b/src/prover/mizar.rs @@ -0,0 +1,348 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! The Mizar backend. +//! +//! Assistant model, and — unlike Coq/Lean/Isabelle — Mizar has **no** `sorry`/ +//! `admit`-style escape hatch: an incomplete or wrong proof is simply a +//! verifier error, and a normal article cannot introduce axioms (only the MML +//! system articles carry the built-in axioms). So the verdict is essentially +//! binary and the lint pack is empty by design; soundness is the verifier's. +//! +//! Mizar checks in two steps against the MML data dir (`MIZFILES`): `accom` +//! accommodates the `environ` block, then `verifier` checks the article and +//! writes errors to a sibling `.err` file — an EMPTY `.err` is the +//! authoritative "verified clean" signal (Mizar reports errors in that file, +//! though the verifier also exits non-zero on error). Ground-truthed against +//! Mizar 8.1.15 (statically-linked i386, runs on x86_64): +//! * `MIZFILES` unset → [`Verdict::Unavailable`] (the MML data dir is the +//! verifier's precondition; without it no honest check is possible). +//! * `verifier`/`accom` binary absent → [`Verdict::Unavailable`]. +//! * ran, `.err` empty and exit 0 → [`Verdict::Proven`]. +//! * ran, `.err` non-empty (or exit non-zero) → [`Verdict::Error`]. +//! +//! [`Backend::check_file`] copies the target `.miz` (and sibling `.miz` files, +//! best-effort for local cross-references) into a temp dir so the source tree +//! stays clean. Article names are the file stem (`ordinal1` ↔ `ordinal1.miz`), +//! so [`crate::graph::module_name_of`] is reused. Import edges come from the +//! `environ` block's directives (`vocabularies`/`notations`/`theorems`/…), +//! lower-cased to match the on-disk stem; only in-tree articles become edges +//! (the MML is external). Local-article prel export (`miz2prel`) and a root +//! convention are documented follow-ons. + +use super::{probe_tool_arg, Backend, BackendKind, Outcome, Probe, Verdict}; +use crate::graph; +use crate::lint::{LintRule, RuleConfig}; +use anyhow::{Context, Result}; +use std::fs; +use std::path::{Path, PathBuf}; +use std::process::Command; +use std::time::{SystemTime, UNIX_EPOCH}; +use walkdir::WalkDir; + +const TAIL_LINES: usize = 40; + +/// The `environ` directives that reference other articles. +const ENVIRON_DIRECTIVES: &[&str] = &[ + "vocabularies", + "notations", + "constructors", + "registrations", + "definitions", + "expansions", + "equalities", + "theorems", + "schemes", + "requirements", +]; + +/// The Mizar proof checker. +#[derive(Clone, Copy, Debug, Default)] +pub struct Mizar; + +impl Backend for Mizar { + fn name(&self) -> &'static str { + "mizar" + } + + fn kind(&self) -> BackendKind { + BackendKind::Assistant + } + + fn extensions(&self) -> &'static [&'static str] { + &["miz"] + } + + fn safe_mode(&self) -> Option<&'static str> { + // Mizar has no admit/sorry construct; soundness is the verifier. + None + } + + fn check_file(&self, file: &Path, include_root: &Path) -> Result { + // The MML data dir is the verifier's precondition. Without it no honest + // check is possible, so report Unavailable (with the reason) rather + // than run a doomed verify and mislabel it Error. + let Ok(mizfiles) = std::env::var("MIZFILES") else { + return Ok(Outcome { + available: false, + exit_code: None, + ok: false, + output_tail: "MIZFILES not set — Mizar needs its MML data dir".to_string(), + kind: BackendKind::Assistant, + verdict: Verdict::Unavailable, + }); + }; + + let stem = file + .file_stem() + .and_then(|s| s.to_str()) + .unwrap_or("article") + .to_string(); + + let nanos = SystemTime::now() + .duration_since(UNIX_EPOCH) + .map(|d| d.as_nanos()) + .unwrap_or(0); + let work = + std::env::temp_dir().join(format!("arghda-miz-{}-{}", std::process::id(), nanos)); + if fs::create_dir_all(&work).is_err() { + return Ok(Outcome::unavailable(BackendKind::Assistant)); + } + + // Copy sibling articles (best-effort for local refs), then the target. + for entry in WalkDir::new(include_root) + .into_iter() + .filter_map(|e| e.ok()) + { + let p = entry.path(); + if p.extension().and_then(|s| s.to_str()) == Some("miz") { + if let Some(name) = p.file_name() { + let _ = fs::copy(p, work.join(name)); + } + } + } + let _ = fs::copy(file, work.join(format!("{stem}.miz"))); + + // Step 1: accommodate the environment. + let accom = Command::new("accom") + .arg(&stem) + .current_dir(&work) + .env("MIZFILES", &mizfiles) + .output(); + if let Err(e) = &accom { + let _ = fs::remove_dir_all(&work); + if e.kind() == std::io::ErrorKind::NotFound { + return Ok(Outcome::unavailable(BackendKind::Assistant)); + } + } + + // Step 2: verify. + let output = Command::new("verifier") + .arg(&stem) + .current_dir(&work) + .env("MIZFILES", &mizfiles) + .output(); + + let result = match output { + Ok(out) => { + let mut combined = String::from_utf8_lossy(&out.stdout).into_owned(); + combined.push_str(&String::from_utf8_lossy(&out.stderr)); + let err_path = work.join(format!("{stem}.err")); + let err_len = fs::metadata(&err_path).map(|m| m.len()).unwrap_or(1); + // Authoritative: an empty `.err` (with a clean exit) is verified. + let verdict = if out.status.success() && err_len == 0 { + Verdict::Proven + } else { + Verdict::Error + }; + // On error, surface the first error line(s) from `.err`. + if verdict == Verdict::Error { + if let Ok(errs) = fs::read_to_string(&err_path) { + if !errs.trim().is_empty() { + combined.push_str("\n.err: "); + combined.push_str(errs.lines().next().unwrap_or("").trim()); + } + } + } + Ok(Outcome { + available: true, + exit_code: out.status.code(), + ok: verdict == Verdict::Proven, + output_tail: tail(&combined, TAIL_LINES), + kind: BackendKind::Assistant, + verdict, + }) + } + Err(e) if e.kind() == std::io::ErrorKind::NotFound => { + Ok(Outcome::unavailable(BackendKind::Assistant)) + } + Err(e) => Err(e.into()), + }; + + let _ = fs::remove_dir_all(&work); + result + } + + fn module_name_of(&self, file: &Path, include_root: &Path) -> Option { + graph::module_name_of(file, include_root) + } + + fn module_to_path(&self, module: &str, include_root: &Path) -> PathBuf { + let mut p = include_root.to_path_buf(); + for part in module.split('.') { + p.push(part); + } + p.set_extension("miz"); + p + } + + fn direct_imports(&self, file: &Path) -> Result> { + let contents = + fs::read_to_string(file).with_context(|| format!("reading {}", file.display()))?; + Ok(parse_environ_imports(&contents)) + } + + fn discover_roots(&self, _include_root: &Path) -> Vec { + // Mizar has no aggregator / entry-article convention (articles are + // listed in a project's text/ dir); an empty root set is honest. + Vec::new() + } + + fn lint_rules(&self, _cfg: &RuleConfig) -> Result>> { + // Mizar has no sorry/admit escape hatch; nothing to warn on. + Ok(Vec::new()) + } + + fn command(&self) -> &'static str { + "verifier" + } + + fn probe(&self) -> Probe { + // Mizar's version query is `verifier -v` (prints the banner). + probe_tool_arg(self.name(), self.kind(), self.command(), "-v") + } +} + +/// Extract the articles referenced by a Mizar `environ` block's directives +/// (`vocabularies`/`notations`/`theorems`/…), lower-cased to match on-disk +/// stems. `::` line comments are stripped; only the region between `environ` +/// and the body's `begin` is scanned. +fn parse_environ_imports(contents: &str) -> Vec { + // Strip `::` line comments, then work on the whitespace token stream. + let decommented: String = contents + .lines() + .map(|l| l.split("::").next().unwrap_or(l)) + .collect::>() + .join("\n"); + let tokens: Vec<&str> = decommented.split_whitespace().collect(); + + let Some(env_pos) = tokens.iter().position(|t| *t == "environ") else { + return Vec::new(); + }; + let end = tokens[env_pos + 1..] + .iter() + .position(|t| *t == "begin") + .map(|p| env_pos + 1 + p) + .unwrap_or(tokens.len()); + + let mut out = Vec::new(); + for tok in &tokens[env_pos + 1..end] { + if ENVIRON_DIRECTIVES.contains(tok) { + continue; + } + let name: String = tok + .chars() + .filter(|c| c.is_alphanumeric() || *c == '_') + .collect::() + .to_ascii_lowercase(); + if !name.is_empty() && !out.contains(&name) { + out.push(name); + } + } + out +} + +fn tail(s: &str, n: usize) -> String { + let lines: Vec<&str> = s.lines().collect(); + let start = lines.len().saturating_sub(n); + lines[start..].join("\n") +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn mizar_backend_identity() { + assert_eq!(Mizar.name(), "mizar"); + assert_eq!(Mizar.kind(), BackendKind::Assistant); + assert_eq!(Mizar.extensions(), &["miz"]); + assert_eq!(Mizar.command(), "verifier"); + } + + #[test] + fn module_to_path_uses_miz_extension() { + assert_eq!( + Mizar.module_to_path("ordinal1", Path::new("/r")), + PathBuf::from("/r/ordinal1.miz") + ); + } + + #[test] + fn environ_directives_parsed_and_lowercased() { + let tmp = tempfile::NamedTempFile::new().unwrap(); + std::fs::write( + tmp.path(), + "environ\n\ + :: a comment mentioning THEOREMS\n\ + vocabularies XBOOLE_0, SUBSET_1;\n\ + notations XBOOLE_0;\n\ + theorems TARSKI, XBOOLE_0; :: trailing comment\n\ + begin\n\ + theorem for X being set holds X = X;\n", + ) + .unwrap(); + let imports = Mizar.direct_imports(tmp.path()).unwrap(); + assert!(imports.contains(&"xboole_0".to_string())); + assert!(imports.contains(&"subset_1".to_string())); + assert!(imports.contains(&"tarski".to_string())); + // Directive keywords are not imports; deduped. + assert!(!imports + .iter() + .any(|i| i == "vocabularies" || i == "theorems")); + assert_eq!( + imports.iter().filter(|i| *i == "xboole_0").count(), + 1, + "deduped" + ); + } + + #[test] + fn no_environ_yields_no_imports() { + let tmp = tempfile::NamedTempFile::new().unwrap(); + std::fs::write(tmp.path(), "begin\ntheorem X;\n").unwrap(); + assert!(Mizar.direct_imports(tmp.path()).unwrap().is_empty()); + } + + #[test] + fn mizar_has_no_lint_rules() { + // Mizar has no admit/sorry construct — the lint pack is empty by design. + assert!(Mizar.lint_rules(&RuleConfig::default()).unwrap().is_empty()); + } + + #[test] + fn check_file_is_honest_about_availability() { + // Never a fabricated pass, whatever the environment: with MIZFILES + // unset or the binary absent → Unavailable; with both present → a real + // Proven/Error from the verifier's `.err`. `ok` iff Proven. + let tmp = tempfile::tempdir().unwrap(); + let f = tmp.path().join("art.miz"); + std::fs::write(&f, "environ\nbegin\n").unwrap(); + let out = Mizar.check_file(&f, tmp.path()).unwrap(); + assert!(matches!( + out.verdict, + Verdict::Proven | Verdict::Error | Verdict::Unavailable + )); + assert_eq!(out.ok, out.verdict == Verdict::Proven); + } +} diff --git a/src/prover/mod.rs b/src/prover/mod.rs index e41d236..ddeebfb 100644 --- a/src/prover/mod.rs +++ b/src/prover/mod.rs @@ -31,6 +31,7 @@ pub mod agda; pub mod idris2; pub mod isabelle; pub mod lean; +pub mod mizar; pub mod rocq; pub mod smt; @@ -38,6 +39,7 @@ pub use agda::{Agda, AgdaCubical}; pub use idris2::Idris2; pub use isabelle::Isabelle; pub use lean::Lean; +pub use mizar::Mizar; pub use rocq::Coq; pub use smt::Smt; diff --git a/tests/fixtures/mizar/base.miz b/tests/fixtures/mizar/base.miz new file mode 100644 index 0000000..045c4d1 --- /dev/null +++ b/tests/fixtures/mizar/base.miz @@ -0,0 +1,4 @@ +environ + vocabularies XBOOLE_0; + notations XBOOLE_0; +begin diff --git a/tests/fixtures/mizar/orphan.miz b/tests/fixtures/mizar/orphan.miz new file mode 100644 index 0000000..8dc9727 --- /dev/null +++ b/tests/fixtures/mizar/orphan.miz @@ -0,0 +1,3 @@ +environ + +begin diff --git a/tests/fixtures/mizar/user.miz b/tests/fixtures/mizar/user.miz new file mode 100644 index 0000000..cb9bc75 --- /dev/null +++ b/tests/fixtures/mizar/user.miz @@ -0,0 +1,3 @@ +environ + theorems BASE, XBOOLE_0; +begin diff --git a/tests/mizar.rs b/tests/mizar.rs new file mode 100644 index 0000000..1ebeac2 --- /dev/null +++ b/tests/mizar.rs @@ -0,0 +1,62 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) + +//! Mizar backend, exercised through the backend-parametric graph/dag/reason +//! path. These tests are hermetic — they only parse `.miz` text (the `environ` +//! block's directives), so they run with or without the `verifier`/`accom` +//! binaries and `MIZFILES`. The real verify (`check_file` → accom + verifier + +//! `.err`) is covered by the unit test in `src/prover/mizar.rs` (honest either +//! way) and by manual dogfooding against Mizar 8.1.15. + +use arghda_core::lint::unpinned_headline::DEFAULT_HEADLINE_PATTERN; +use arghda_core::{build_dag, build_reason, Backend, LintRule, Mizar}; +use std::collections::{BTreeMap, BTreeSet}; +use std::path::PathBuf; + +fn mizar_fixture() -> PathBuf { + let mut p = PathBuf::from(env!("CARGO_MANIFEST_DIR")); + p.push("tests"); + p.push("fixtures"); + p.push("mizar"); + p +} + +fn no_rules() -> Vec> { + Vec::new() +} + +#[test] +fn mizar_environ_graph_over_the_fixture() { + let root = mizar_fixture(); + let roots = Mizar.discover_roots(&root); + let dag = build_dag(&root, &roots, &no_rules(), DEFAULT_HEADLINE_PATTERN, &Mizar).unwrap(); + + let mut ids: Vec<&str> = dag.nodes.iter().map(|n| n.id.as_str()).collect(); + ids.sort_unstable(); + assert_eq!(ids, vec!["base", "orphan", "user"]); + + // `user`'s environ references `BASE` (in-tree, lower-cased) → an edge; the + // MML reference `XBOOLE_0` is external and dropped. + assert!(dag + .edges + .iter() + .any(|e| e.from == "user" && e.to == "base" && e.kind == "imports")); + assert!( + !dag.edges.iter().any(|e| e.to == "xboole_0"), + "MML import dropped as external" + ); + assert!(!dag.edges.iter().any(|e| e.to == "orphan")); +} + +#[test] +fn mizar_has_no_root_convention() { + // Mizar has no aggregator / entry-article convention — an empty root set is + // honest, so nothing is "wired" (unlike Agda's All.agda cone). + let root = mizar_fixture(); + assert!(Mizar.discover_roots(&root).is_empty()); + + let dag = build_dag(&root, &[], &no_rules(), DEFAULT_HEADLINE_PATTERN, &Mizar).unwrap(); + let doc = build_reason(dag, &Mizar, &BTreeMap::new(), &BTreeSet::new()); + assert!(doc.crt_roots.is_empty()); + assert!(doc.nodes.iter().all(|n| !n.wired)); +}