|
| 1 | +// SPDX-License-Identifier: PMPL-1.0-or-later |
| 2 | += docs/ — Project Documentation |
| 3 | + |
| 4 | +Project-level documentation tree. ~49 entries (subdirs + files); |
| 5 | +historically flat-organised — the 2026-04-18 audit flagged the lack of |
| 6 | +`docs/architecture/`, `docs/decisions/`, `docs/practice/`, `docs/wikis/` |
| 7 | +subtrees as a coverage gap, but the existing files are themselves |
| 8 | +well-maintained. |
| 9 | + |
| 10 | +This README provides orientation; individual files are self-describing. |
| 11 | + |
| 12 | +== Subdirectories |
| 13 | + |
| 14 | +[cols="2,4"] |
| 15 | +|=== |
| 16 | +| Path | Role |
| 17 | + |
| 18 | +| `governance/` |
| 19 | +| Authoritative governance artefacts. Currently |
| 20 | + `CRG-AUDIT-2026-04-18.adoc` (the active audit driving the v0.9.x |
| 21 | + closure list); future audits land here. |
| 22 | + |
| 23 | +| `reports/audit/` |
| 24 | +| Historical audit snapshots; currently `audit-2026-04-04.md` (M2 |
| 25 | + estate audit, "REPAIR THEN PUBLISH" verdict). |
| 26 | +|=== |
| 27 | + |
| 28 | +== Top-level files (selection) |
| 29 | + |
| 30 | +[cols="2,4"] |
| 31 | +|=== |
| 32 | +| File | Purpose |
| 33 | + |
| 34 | +| `ARCHITECTURE.md` + `ARCHITECTURE_DIAGRAMS.md` |
| 35 | +| System-level architecture overview. |
| 36 | + |
| 37 | +| `LEAN4_RUST_CORRESPONDENCE.md` |
| 38 | +| Design of the Lean → Rust correspondence (currently |
| 39 | + property-tested, not mechanised; ~85% confidence per CLAUDE.md). |
| 40 | + |
| 41 | +| `PROOF_HOLES_AUDIT.md` |
| 42 | +| Active proof-debt ledger across the 6-system stack |
| 43 | + (Coq/Lean4/Agda/Isabelle/Mizar/Z3 + Idris2 ABI). Source of truth for |
| 44 | + the `[coq-proof-status]` block in `../.machine_readable/6a2/STATE.a2ml`. |
| 45 | + |
| 46 | +| `POSIX_COMPLIANCE.md` |
| 47 | +| Per-feature POSIX compliance tracker (M1-M11 milestones; M1-M9 |
| 48 | + complete, M10-M11 partial). |
| 49 | + |
| 50 | +| `PROOF_OVERVIEW.md` + `PROPERTY_TESTING.md` + `VERIFICATION_STRATEGY_ANALYSIS.md` |
| 51 | +| Verification approach + property-testing discipline. |
| 52 | + |
| 53 | +| `SEAM_ANALYSIS_AND_IDRIS2_PLAN.md` + `ZIG_LEAN_EXTRACTION.md` |
| 54 | +| Future-direction designs (Idris2 extraction; Zig-Lean integration). |
| 55 | + |
| 56 | +| `ECHIDNA_INTEGRATION.md` |
| 57 | +| Echidna validator integration spec (audit item 10b — wiring still |
| 58 | + TODO; spec is the design source). |
| 59 | + |
| 60 | +| `PHASE2_REPORT.md` / `PHASE3_INITIAL_REPORT.md` / `PHASE6_M*_DESIGN.md` (10 docs) |
| 61 | +| Per-phase milestone designs and reports. The PHASE6_M*_DESIGN docs |
| 62 | + enumerate Phase 6 milestones M1-M13. |
| 63 | + |
| 64 | +| `USER_GUIDE.md` |
| 65 | +| End-user documentation for the `vsh` shell. |
| 66 | + |
| 67 | +| `CITATIONS.adoc` |
| 68 | +| Academic citations + references. |
| 69 | + |
| 70 | +| `CONTRIBUTOR_GUIDE_TIER1.md` |
| 71 | +| Tier-1 contribution guide. |
| 72 | + |
| 73 | +| `OCAML_EXTRACTION.md` |
| 74 | +| OCaml extraction design (companion to `../impl/ocaml/README.adoc`). |
| 75 | + |
| 76 | +| `INTEGRATION.md` |
| 77 | +| Cross-system integration notes. |
| 78 | + |
| 79 | +| `CONSOLIDATION_ANALYSIS.md` / `CONTINUATION_REPORT.md` / |
| 80 | + `SIMPLIFICATION_OPPORTUNITIES.md` |
| 81 | +| Audit-style review documents. |
| 82 | + |
| 83 | +| `COMPREHENSIVE_EXAMPLES.md` / `DEMO_EXTERNAL_COMMANDS.md` |
| 84 | +| Worked examples + REPL demos. |
| 85 | +|=== |
| 86 | + |
| 87 | +== Conventions |
| 88 | + |
| 89 | +* Mixed `.md` (legacy) and `.adoc` (current preferred per RSR |
| 90 | + conventions). New documents should use `.adoc`. |
| 91 | +* Each file is self-describing; no central index file beyond this README. |
| 92 | +* Per-domain subtrees (`governance/`, `reports/`) collect related artefacts. |
| 93 | + |
| 94 | +== See also |
| 95 | + |
| 96 | +* `../README.md` / `../EXPLAINME.adoc` — repo entry points |
| 97 | +* `../CLAUDE.md` — AI-assistant honest-status document |
| 98 | +* `../ROADMAP.adoc` — release track + audit closure list |
| 99 | +* `../.machine_readable/6a2/STATE.a2ml` — machine-readable state |
0 commit comments