ArghDA M10 follow-on: Mizar local-article cross-references (M10 → 95%)

A Mizar article that `Require`s a sibling — `theorems X;` on a local article X —
is now checkable. Before this, X wasn't in any library, so `accom` on the
dependent errored.

Ground-truthed the export pipeline against real Mizar 8.1.15: to reference a
local X, X must be built into a local library — `accom X; verifier X;
exporter X; transfer X` produces X's library files, and `transfer` populates a
local `./prel` the accommodator reads. `check_file` now, before checking the
target, exports each in-tree transitive dependency in topological order
(`mizar_transitive_deps` is a cycle-safe post-order DFS over environ imports;
MML references are skipped) via that 4-tool pipeline in the temp work dir.

Honesty preserved: a broken dependency fails the dependent — dogfooded a
`ybad` that requires a broken `xbad` → `error` (no false green). A valid
`y` requiring a valid `x` → `proven`.

Verification (actually run): cargo fmt --check, clippy -D warnings, cargo test
(175 pass, +1 topo-order unit), check-spdx.sh — all green. Dogfooded vs real
Mizar 8.1.15 (MIZFILES=/opt/mizar): `y.miz` with `theorems X;` using `by X:1`
→ proven (was error pre-fix); `ybad` requiring broken `xbad` → error;
`reason --check` → x/y proven, xbad/ybad error.

Honest scope: the THEOREMS cross-reference path is dogfooded end-to-end. The
same accom→verifier→exporter→transfer pipeline is Mizar's standard library
build, so definitions/notations/constructors cross-refs travel the same path,
but were not separately dogfooded (a correct definitions fixture is finicky to
author; not rabbit-holed). Residual: verify those + a session/root convention.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012MpYSh6Wy8YMBH2E3qVyT7

Author: claude

.machine_readable/6a2/STATE.a2ml

@@ -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 = 97 },
   { name = "M9: Isabelle adapter (--heavy; dogfood tropical-resource-typing .thy)", completion = 90 },
-  { name = "M10: Mizar adapter (detect-only first; highest uncertainty)", completion = 85 },
+  { name = "M10: Mizar adapter (detect-only first; highest uncertainty)", completion = 95 },
   { 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
@@ -114,6 +114,26 @@ milestones = [
 # --backend idris2` over an ipkg fixture → crt_roots ['App'], App+Helper wired.
 # M4 now 95% (remaining: totality-hole `?name` + per-def `partial` lint).
 #
+# M10 FOLLOW-ON landed 2026-07-01 (M10 85% → 95%): Mizar local-article cross-
+# references. Was: `theorems X;` on a sibling article errored (X not in the
+# library). GROUND-TRUTHED the export pipeline vs real Mizar 8.1.15: to Require
+# a local X, X must be built into a local library — `accom X; verifier X;
+# exporter X; transfer X` produces X's library files and `transfer` populates a
+# local `./prel` the accommodator reads. check_file now, before checking the
+# target, exports each in-tree transitive dep in TOPOLOGICAL order
+# (`mizar_transitive_deps` = post-order DFS over environ imports, cycle-safe,
+# MML refs skipped) via that 4-tool pipeline in the temp work dir. 175 tests
+# (+1 topo-order unit). DOGFOODED vs real Mizar 8.1.15 (MIZFILES=/opt/mizar):
+# y.miz with `theorems X;` using `by X:1` → proven (was error pre-fix); the
+# honesty case — ybad requiring a BROKEN xbad → error (a broken dep fails the
+# dependent, no false green); reason --check → x/y proven, xbad/ybad error.
+# HONEST SCOPE: the THEOREMS cross-reference path is dogfooded end-to-end. The
+# same accom→verifier→exporter→transfer pipeline is Mizar's standard library
+# build, so definitions/notations/constructors cross-refs travel the same path,
+# but were NOT separately dogfooded (a definitions fixture is finicky to author
+# correctly; not rabbit-holed). Residual 5%: verify definitions/notations
+# cross-refs + a session/root convention.
+#
 # M8 FOLLOW-ON landed 2026-07-01 (M8 90% → 97%): dependency-ordered Coq
 # compilation — multi-file projects are now checkable. Was: a bare `coqc B.v`
 # where B `Require`s an in-tree A errored "Cannot find a physical path bound to
@@ -453,7 +473,7 @@ actions = [
   "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): 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.",
   "M7 client INVESTIGATED 2026-07-01 → BLOCKED (stub stays): no confirmed Echidna HTTP contract exists (dispatch.rs says API unconfirmed; ECOSYSTEM.a2ml gives no endpoints/schema; the echidna repo is out of this session's access scope). Building a client would mean inventing an unverifiable contract — forbidden. Unblock: a published Echidna API + a reachable instance to dogfood; then wire Dispatch::run behind a cargo feature. ROADMAP TERMINUS — all tractable items done; M7's client is the sole residual, externally blocked.",
-  "HEAVY-TAIL COMPLETION CUTS (owner asked for these 2026-07-01, doing foundation-first, one PR each, real-tool dogfood): [DONE] Coq dependency-ordered compilation (M8 90→97%); [NEXT] Mizar local-article prel export via miz2prel so cross-article refs check (M10 85→~100%); [THEN] Isabelle session-qualified imports + multi-session builds (M9 90→~100%). Residual after: Coq _CoqProject custom -Q/-R prefixes (3%); arghda-studio visual layer (separate repo, out of this session's scope; AffineScript).",
+  "HEAVY-TAIL COMPLETION CUTS (owner asked 2026-07-01, foundation-first, one PR each, real-tool dogfood): [DONE] Coq dependency-ordered compilation (M8 90→97%); [DONE] Mizar local-article cross-refs via accom/verifier/exporter/transfer export pipeline (M10 85→95%, theorems path dogfooded); [NEXT/LAST] Isabelle session-qualified imports + multi-session builds (M9 90→~100%). Residual after: Coq _CoqProject custom -Q/-R prefixes (3%); Mizar definitions/notations cross-refs not separately dogfooded (5%); arghda-studio visual layer (separate repo, out of this session's scope; AffineScript).",
 ]
 
 [maintenance-status]
@@ -462,10 +482,11 @@ 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-M8-deporder: 131 lib + 43 integration = 174 tests pass. M8 dependency-
-# ordered Coq compilation dogfooded vs real coqc 8.18.0 (A←B←C chain → all
-# proven; transitive admit demotes the dependent's effective verdict, not
-# whitewashed). M4 totality-hole + partial lint dogfooded vs real idris2 0.7.0.
+# post-M10-crossref: 132 lib + 43 integration = 175 tests pass. M10 Mizar
+# local-article cross-refs dogfooded vs real Mizar 8.1.15 (y requires local x →
+# proven; broken dep → dependent error). M8 dependency-ordered Coq compilation
+# dogfooded vs real coqc 8.18.0 (A←B←C chain → all proven; transitive admit
+# demotes the dependent's effective verdict). M4 totality lint dogfooded vs idris2.
 # M6 lake-env import resolution dogfooded vs real Lean 4.13.0 + Lake 5.0.0
 # (imported file in a built lake project → proven; outside → error). codeql.yml added
 # (code-scanning gate fix). M10 Mizar adapter dogfooded vs real Mizar 8.1.15

src/prover/mizar.rs

@@ -27,8 +27,11 @@
 //! 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.
+//! (the MML is external). Local-article cross-references are supported:
+//! [`Backend::check_file`] exports each in-tree dependency in topological order
+//! (accom → verifier → exporter → transfer, populating a local `./prel` the
+//! accommodator reads) before checking the target, so a `theorems X;` on a
+//! sibling article `X` resolves. A session/root convention remains a follow-on.
 
 use super::{probe_tool_arg, Backend, BackendKind, Outcome, Probe, Verdict};
 use crate::graph;
@@ -123,6 +126,25 @@ impl Backend for Mizar {
         }
         let _ = fs::copy(file, work.join(format!("{stem}.miz")));
 
+        // Build the target's in-tree dependencies into a local library so its
+        // `theorems`/`definitions`/… directives resolve: for each dep in
+        // topological order (deps before dependents), run the export pipeline
+        // accom → verifier → exporter → transfer, which populates `./prel` in
+        // the work dir (the accommodator reads local library files from there).
+        // External MML articles are skipped (resolved from MIZFILES). Verdict-
+        // affecting failures surface honestly as a non-empty target `.err`.
+        let src = fs::read_to_string(file).unwrap_or_default();
+        let deps = mizar_transitive_deps(&parse_environ_imports(&src), include_root);
+        for dep in &deps {
+            for tool in ["accom", "verifier", "exporter", "transfer"] {
+                let _ = Command::new(tool)
+                    .arg(dep)
+                    .current_dir(&work)
+                    .env("MIZFILES", &mizfiles)
+                    .output();
+            }
+        }
+
         // Step 1: accommodate the environment.
         let accom = Command::new("accom")
             .arg(&stem)
@@ -223,6 +245,40 @@ impl Backend for Mizar {
     }
 }
 
+/// The in-tree transitive article dependencies of a Mizar file, given the
+/// articles its `environ` block references, in dependency-first (topological)
+/// order — so exporting the list left-to-right satisfies every later `accom`.
+/// External MML articles (absent under `include_root`) are skipped. Cycle-safe
+/// via the visited set.
+fn mizar_transitive_deps(direct: &[String], include_root: &Path) -> Vec<String> {
+    let mut visited = std::collections::HashSet::new();
+    let mut order = Vec::new();
+    for m in direct {
+        mizar_visit_dep(m, include_root, &mut visited, &mut order);
+    }
+    order
+}
+
+fn mizar_visit_dep(
+    module: &str,
+    include_root: &Path,
+    visited: &mut std::collections::HashSet<String>,
+    order: &mut Vec<String>,
+) {
+    if !visited.insert(module.to_string()) {
+        return;
+    }
+    // Only in-tree articles resolve to a readable `.miz`; MML articles are
+    // left for MIZFILES.
+    let Ok(src) = fs::read_to_string(include_root.join(format!("{module}.miz"))) else {
+        return;
+    };
+    for imp in parse_environ_imports(&src) {
+        mizar_visit_dep(&imp, include_root, visited, order);
+    }
+    order.push(module.to_string());
+}
+
 /// 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`
@@ -330,6 +386,25 @@ mod tests {
         assert!(Mizar.lint_rules(&RuleConfig::default()).unwrap().is_empty());
     }
 
+    #[test]
+    fn transitive_deps_are_topologically_ordered() {
+        // z requires y; y requires x; x is a leaf. Build order for z must be
+        // [x, y] (deps before dependents); MML refs are skipped.
+        let tmp = tempfile::tempdir().unwrap();
+        let r = tmp.path();
+        std::fs::write(r.join("x.miz"), "environ\nbegin\n").unwrap();
+        std::fs::write(r.join("y.miz"), "environ\n theorems X;\nbegin\n").unwrap();
+        std::fs::write(r.join("z.miz"), "environ\n theorems Y, XBOOLE_0;\nbegin\n").unwrap();
+        let deps =
+            mizar_transitive_deps(&parse_environ_imports("environ\n theorems Z;\nbegin\n"), r);
+        assert_eq!(
+            deps,
+            vec!["x".to_string(), "y".to_string(), "z".to_string()]
+        );
+        // The MML article is not staged as an in-tree dep.
+        assert!(!deps.iter().any(|m| m == "xboole_0"));
+    }
+
     #[test]
     fn check_file_is_honest_about_availability() {
         // Never a fabricated pass, whatever the environment: with MIZFILES