mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
allaun
4490dc28a7
- Move canonical FixedPoint to Core/SilverSight/FixedPoint.lean - Add SilverSightRRC library: RRC logogram gates, receipt bridge, AVM ISA - Add AVMIsa.Emit as the sole top-level JSON output boundary - Add rrc-emit-fixture executable and Python I/O shims - Update AGENTS.md, glossary, project map, and build baseline Build: 2981 jobs, 0 errors (lake build)
456 lines
24 KiB
Python
456 lines
24 KiB
Python
#!/usr/bin/env python3
|
|
"""Generate a living, regenerable project map for SilverSight.
|
|
|
|
Usage:
|
|
python3 docs/generate_project_map.py
|
|
|
|
Outputs:
|
|
docs/PROJECT_MAP.json — machine-readable project map
|
|
docs/PROJECT_MAP.md — human-readable project map
|
|
|
|
The map is derived from the actual filesystem, lakefile.lean roots, and
|
|
hand-curated annotations in RESEARCH_STACK_SOURCE below. Re-run this script
|
|
after adding or moving modules.
|
|
"""
|
|
|
|
from __future__ import annotations
|
|
|
|
import json
|
|
import re
|
|
from collections import defaultdict
|
|
from pathlib import Path
|
|
from typing import Any
|
|
|
|
|
|
REPO_ROOT = Path(__file__).resolve().parents[1]
|
|
OUT_JSON = REPO_ROOT / "docs" / "PROJECT_MAP.json"
|
|
OUT_MD = REPO_ROOT / "docs" / "PROJECT_MAP.md"
|
|
|
|
# Hand-curated mapping from SilverSight file to Research-Stack source module.
|
|
# Use None when there is no Research-Stack source.
|
|
RESEARCH_STACK_SOURCE: dict[str, str | None] = {
|
|
"Core/SilverSightCore.lean": None,
|
|
"formal/CoreFormalism/FixedPoint.lean": "0-Core-Formalism/lean/Semantics/Semantics/FixedPoint.lean",
|
|
"formal/CoreFormalism/Tactics.lean": "0-Core-Formalism/lean/Semantics/Semantics/Tactics.lean",
|
|
"formal/CoreFormalism/Q16_16Numerics.lean": "0-Core-Formalism/lean/Semantics/Semantics/Q16_16Numerics.lean",
|
|
"formal/CoreFormalism/DynamicCanal.lean": "0-Core-Formalism/lean/Semantics/Semantics/DynamicCanal.lean",
|
|
"formal/CoreFormalism/Bind.lean": "0-Core-Formalism/lean/Semantics/Semantics/Bind.lean",
|
|
"formal/CoreFormalism/BraidBracket.lean": "0-Core-Formalism/lean/Semantics/Semantics/BraidBracket.lean",
|
|
"formal/CoreFormalism/BraidStrand.lean": "0-Core-Formalism/lean/Semantics/Semantics/BraidStrand.lean",
|
|
"formal/CoreFormalism/BraidCross.lean": "0-Core-Formalism/lean/Semantics/Semantics/BraidCross.lean",
|
|
"formal/CoreFormalism/BraidField.lean": "0-Core-Formalism/lean/Semantics/Semantics/BraidField.lean",
|
|
"formal/CoreFormalism/SidonSets.lean": "0-Core-Formalism/lean/Semantics/Semantics/SidonSets.lean",
|
|
"formal/CoreFormalism/SieveLemmas.lean": "0-Core-Formalism/lean/Semantics/Semantics/SieveLemmas.lean",
|
|
"formal/CoreFormalism/InteractionGraphSidon.lean": "0-Core-Formalism/lean/Semantics/Semantics/InteractionGraphSidon.lean",
|
|
"formal/CoreFormalism/BraidEigensolid.lean": "0-Core-Formalism/lean/Semantics/Semantics/BraidEigensolid.lean",
|
|
"formal/CoreFormalism/BraidSpherionBridge.lean": "0-Core-Formalism/lean/Semantics/Semantics/BraidSpherionBridge.lean",
|
|
"formal/CoreFormalism/ChentsovFinite.lean": "0-Core-Formalism/lean/Semantics/Semantics/ChentsovBridge.lean",
|
|
"formal/CoreFormalism/HachimojiBase.lean": None,
|
|
"formal/CoreFormalism/HachimojiCodec.lean": None,
|
|
"formal/CoreFormalism/HachimojiManifoldAxiom.lean": None,
|
|
"formal/PVGS_DQ_Bridge/PVGS_DQ_Bridge_fixed.lean": "0-Core-Formalism/lean/Semantics/Semantics/PVGS_DQ_Bridge.lean",
|
|
"formal/PVGS_DQ_Bridge/section1_pvgs_params.lean": "0-Core-Formalism/lean/Semantics/Semantics/PVGS_DQ_Bridge.lean",
|
|
"formal/PVGS_DQ_Bridge/section2_hermite_sieve.lean": "0-Core-Formalism/lean/Semantics/Semantics/PVGS_DQ_Bridge.lean",
|
|
"formal/PVGS_DQ_Bridge/section3_variety_isomorphism.lean": "0-Core-Formalism/lean/Semantics/Semantics/PVGS_DQ_Bridge.lean",
|
|
"formal/PVGS_DQ_Bridge/section4_rrc_kernel.lean": "0-Core-Formalism/lean/Semantics/Semantics/PVGS_DQ_Bridge.lean",
|
|
"formal/PVGS_DQ_Bridge/section5_quantum_sensing.lean": "0-Core-Formalism/lean/Semantics/Semantics/PVGS_DQ_Bridge.lean",
|
|
"formal/PVGS_DQ_Bridge/section6_effective_bounds.lean": "0-Core-Formalism/lean/Semantics/Semantics/PVGS_DQ_Bridge.lean",
|
|
"formal/PVGS_DQ_Bridge/section7_master_receipt.lean": "0-Core-Formalism/lean/Semantics/Semantics/PVGS_DQ_Bridge.lean",
|
|
"formal/PVGS_DQ_Bridge/pvgs_receipt_hash.py": "4-Infrastructure/shim/pvgs_receipt_hash.py",
|
|
"formal/UniversalEncoding/UniversalMathEncoding.lean": "0-Core-Formalism/lean/Semantics/Semantics/UniversalMathEncoding.lean",
|
|
"formal/UniversalEncoding/ChiralitySpace.lean": "0-Core-Formalism/lean/Semantics/Semantics/ChiralitySpace.lean",
|
|
"formal/BindingSite/BindingSiteCodec.lean": "0-Core-Formalism/lean/Semantics/Semantics/BindingSite/BindingSiteCodec.lean",
|
|
"formal/BindingSite/BindingSiteEntropy.lean": "0-Core-Formalism/lean/Semantics/Semantics/BindingSite/BindingSiteEntropy.lean",
|
|
"formal/BindingSite/BindingSiteHachimoji.lean": "0-Core-Formalism/lean/Semantics/Semantics/BindingSite/BindingSiteHachimoji.lean",
|
|
"python/chaos_game.py": "4-Infrastructure/shim/chaos_game_16d.py",
|
|
"python/sidon_address.py": "4-Infrastructure/shim/sidon_generation_kernel.py",
|
|
"python/spectral_profile.py": "4-Infrastructure/shim/geometric_entropy_explorer.py",
|
|
"python/q16_canonical.py": None,
|
|
"python/test_search.py": None,
|
|
"qubo/finsler_metric.py": "4-Infrastructure/shim/qaoa_adapter.py",
|
|
"qubo/qubo_builder.py": "4-Infrastructure/shim/qaoa_adapter.py",
|
|
"qubo/qaoa_circuit.py": "4-Infrastructure/shim/qaoa_adapter.py",
|
|
"qubo/classical_solver.py": "4-Infrastructure/shim/qubo_highs.py",
|
|
"qubo/test_optimize.py": None,
|
|
"tests/test_q16_canonical.py": None,
|
|
"tests/quarantine/q16_roundtrip_test.legacy.py": "tests/q16_roundtrip_test.py",
|
|
}
|
|
|
|
# Short role descriptions for key files.
|
|
ROLE_DESCRIPTIONS: dict[str, str] = {
|
|
"Core/SilverSightCore.lean": "Invariant core: Hachimoji states, Receipt, AVM δ, TIC axiom, library interface.",
|
|
"formal/CoreFormalism/FixedPoint.lean": "Canonical Q16_16 fixed-point type; source of truth for cross-language determinism.",
|
|
"formal/CoreFormalism/Tactics.lean": "Shared tactic macros used across CoreFormalism modules.",
|
|
"formal/CoreFormalism/Q16_16Numerics.lean": "Numeric helpers and bounds over canonical Q16_16.",
|
|
"formal/CoreFormalism/DynamicCanal.lean": "Dynamic canal primitives for braid/spherion flow.",
|
|
"formal/CoreFormalism/Bind.lean": "Bind/connective primitives used by braid modules.",
|
|
"formal/CoreFormalism/BraidBracket.lean": "Braid bracket algebra.",
|
|
"formal/CoreFormalism/BraidStrand.lean": "8-strand braid model.",
|
|
"formal/CoreFormalism/BraidCross.lean": "Braid crossing representation and residuals.",
|
|
"formal/CoreFormalism/BraidField.lean": "Field operations on braid states.",
|
|
"formal/CoreFormalism/SidonSets.lean": "Sidon-set definitions, extremal function, Johnson/Lindström bounds, Singer theorem.",
|
|
"formal/CoreFormalism/SieveLemmas.lean": "Coprime-sieve observers and CRT reconstruction.",
|
|
"formal/CoreFormalism/InteractionGraphSidon.lean": "Typed interaction graphs, bounded Sidon witness, weak-axis CRT reconstruction.",
|
|
"formal/CoreFormalism/BraidEigensolid.lean": "Eigensolid fixed-point theory for BraidStorm topology.",
|
|
"formal/CoreFormalism/BraidSpherionBridge.lean": "Braid-to-spherion bridge and topological mixing.",
|
|
"formal/CoreFormalism/ChentsovFinite.lean": "Finite Chentsov theorem for the 8-state Hachimoji simplex.",
|
|
"formal/CoreFormalism/HachimojiBase.lean": "Base definitions for the 8-state Hachimoji alphabet.",
|
|
"formal/CoreFormalism/HachimojiCodec.lean": "Hachimoji encode/decode for UTF-8 strings.",
|
|
"formal/CoreFormalism/HachimojiManifoldAxiom.lean": "Axioms tying Hachimoji states to statistical manifold structure.",
|
|
"formal/PVGS_DQ_Bridge/PVGS_DQ_Bridge_fixed.lean": "Master PVGS dual-quaternion bridge receipt.",
|
|
"formal/PVGS_DQ_Bridge/section1_pvgs_params.lean": "Photon-varied Gaussian state parameters.",
|
|
"formal/PVGS_DQ_Bridge/section2_hermite_sieve.lean": "Hermite-sieve construction for PVGS.",
|
|
"formal/PVGS_DQ_Bridge/section3_variety_isomorphism.lean": "Variety isomorphism linking PVGS states.",
|
|
"formal/PVGS_DQ_Bridge/section4_rrc_kernel.lean": "RRC kernel embedded in PVGS bridge.",
|
|
"formal/PVGS_DQ_Bridge/section5_quantum_sensing.lean": "Quantum-sensing bounds within PVGS.",
|
|
"formal/PVGS_DQ_Bridge/section6_effective_bounds.lean": "Effective bounds for dual-quaternion operations.",
|
|
"formal/PVGS_DQ_Bridge/section7_master_receipt.lean": "Top-level PVGS receipt assembly.",
|
|
"formal/PVGS_DQ_Bridge/pvgs_receipt_hash.py": "Python helper to hash PVGS receipts.",
|
|
"formal/UniversalEncoding/UniversalMathEncoding.lean": "50-token universal math address space.",
|
|
"formal/UniversalEncoding/ChiralitySpace.lean": "Chirality classification space.",
|
|
"formal/BindingSite/BindingSiteCodec.lean": "Binding-site codec for amino-acid/protein sketches.",
|
|
"formal/BindingSite/BindingSiteEntropy.lean": "Entropy calculations for binding sites.",
|
|
"formal/BindingSite/BindingSiteHachimoji.lean": "Binding-site classification into Hachimoji states.",
|
|
"python/chaos_game.py": "16D chaos-game basin sampler.",
|
|
"python/sidon_address.py": "Sidon label generation for collision-free addressing.",
|
|
"python/spectral_profile.py": "Spectral/entropy profile exploration.",
|
|
"python/q16_canonical.py": "Canonical Q16_16 Python reference implementation.",
|
|
"python/test_search.py": "Search-layer sanity tests.",
|
|
"qubo/finsler_metric.py": "Finsler-Randers metric and QUBO formulation.",
|
|
"qubo/qubo_builder.py": "QUBO/Ising/Pauli problem builder.",
|
|
"qubo/qaoa_circuit.py": "QAOA circuit generation and classical simulation.",
|
|
"qubo/classical_solver.py": "HiGHS MIP bridge + TSP assignment relaxation.",
|
|
"qubo/test_optimize.py": "Optimization-layer unit tests.",
|
|
"tests/test_q16_canonical.py": "Canonical Q16_16 unit tests.",
|
|
"tests/quarantine/q16_roundtrip_test.legacy.py": "Archived C <-> Python roundtrip test; waiting on C bridge.",
|
|
}
|
|
|
|
# Which files are on the Receipt boundary (produce or consume Receipts).
|
|
RECEIPT_BOUNDARY: set[str] = {
|
|
"Core/SilverSightCore.lean",
|
|
"formal/PVGS_DQ_Bridge/PVGS_DQ_Bridge_fixed.lean",
|
|
"formal/PVGS_DQ_Bridge/section7_master_receipt.lean",
|
|
"formal/PVGS_DQ_Bridge/pvgs_receipt_hash.py",
|
|
}
|
|
|
|
# Explicit layers as they appear in the conceptual architecture.
|
|
LAYERS: list[dict[str, Any]] = [
|
|
{"id": "core", "name": "Core", "path": "Core", "description": "Invariant core: no imports except Mathlib; defines Receipt and AVM."},
|
|
{"id": "coreformalism", "name": "CoreFormalism", "path": "formal/CoreFormalism", "description": "Canonical Q16_16, Sidon, braid, and Hachimoji foundations."},
|
|
{"id": "pvgs_dq_bridge", "name": "PVGS_DQ_Bridge", "path": "formal/PVGS_DQ_Bridge", "description": "Photon-varied Gaussian state dual-quaternion bridge."},
|
|
{"id": "universal_encoding", "name": "UniversalEncoding", "path": "formal/UniversalEncoding", "description": "Universal math address space and chirality."},
|
|
{"id": "binding_site", "name": "BindingSite", "path": "formal/BindingSite", "description": "Amino-acid / protein binding sketches."},
|
|
{"id": "python_shim", "name": "PythonShims", "path": "python", "description": "I/O and feature extraction; no admissibility logic."},
|
|
{"id": "qubo_shim", "name": "QUBOShims", "path": "qubo", "description": "QUBO/QAOA/Finsler optimization shims."},
|
|
{"id": "tests", "name": "Tests", "path": "tests", "description": "Verification fixtures."},
|
|
{"id": "infrastructure", "name": "Infrastructure", "path": ".github", "description": "CI workflows and repo scripts."},
|
|
{"id": "docs", "name": "Docs", "path": "docs", "description": "Architecture, contracts, and generated maps."},
|
|
]
|
|
|
|
|
|
def parse_lakefile_roots(text: str) -> list[str]:
|
|
"""Extract the explicit root module names from lakefile.lean."""
|
|
roots: list[str] = []
|
|
in_roots = False
|
|
for line in text.splitlines():
|
|
stripped = line.strip()
|
|
if stripped.startswith("roots := #["):
|
|
in_roots = True
|
|
stripped = stripped[len("roots := #[") :]
|
|
if in_roots:
|
|
for token in stripped.split(","):
|
|
token = token.strip()
|
|
if token.startswith("`"):
|
|
roots.append(token[1:])
|
|
if "]" in stripped:
|
|
in_roots = False
|
|
break
|
|
return roots
|
|
|
|
|
|
def lean_path_to_module(rel: Path) -> str:
|
|
"""formal/CoreFormalism/FixedPoint.lean -> CoreFormalism.FixedPoint"""
|
|
parts = rel.with_suffix("").parts
|
|
return ".".join(parts[1:]) if len(parts) > 1 else ".".join(parts)
|
|
|
|
|
|
def extract_lean_imports(text: str) -> list[str]:
|
|
return [m.group(1).strip() for line in text.splitlines() if (m := re.match(r"^\s*import\s+(.+)", line))]
|
|
|
|
|
|
def extract_python_imports(text: str) -> list[str]:
|
|
imports: list[str] = []
|
|
for line in text.splitlines():
|
|
if m := re.match(r"^\s*import\s+([\w.]+)", line):
|
|
imports.append(m.group(1))
|
|
elif m := re.match(r"^\s*from\s+([\w.]+)\s+import", line):
|
|
imports.append(m.group(1))
|
|
return imports
|
|
|
|
|
|
def file_status(rel: str) -> str:
|
|
if "quarantine" in rel:
|
|
return "quarantined"
|
|
if rel.endswith(".legacy.py"):
|
|
return "archived"
|
|
return "active"
|
|
|
|
|
|
def discover_files() -> list[dict[str, Any]]:
|
|
entries: list[dict[str, Any]] = []
|
|
lean_roots = parse_lakefile_roots((REPO_ROOT / "lakefile.lean").read_text())
|
|
root_set = set(lean_roots)
|
|
|
|
for path in sorted(REPO_ROOT.rglob("*")):
|
|
rel = path.relative_to(REPO_ROOT).as_posix()
|
|
if path.is_dir():
|
|
continue
|
|
if any(part.startswith(".") for part in path.relative_to(REPO_ROOT).parts):
|
|
# Skip hidden dirs (.git, .lake, .github? we want .github)
|
|
if not rel.startswith(".github/"):
|
|
continue
|
|
if "__pycache__" in rel or ".pytest_cache" in rel:
|
|
continue
|
|
|
|
language: str
|
|
kind: str
|
|
if rel.endswith(".lean"):
|
|
language = "lean"
|
|
kind = "core" if rel.startswith("Core/") else "formal"
|
|
elif rel.endswith(".py"):
|
|
language = "python"
|
|
if rel.startswith("python/"):
|
|
kind = "python_shim"
|
|
elif rel.startswith("qubo/"):
|
|
kind = "qubo_shim"
|
|
elif rel.startswith("tests/"):
|
|
kind = "test"
|
|
else:
|
|
kind = "script"
|
|
elif rel.startswith(".github/workflows/"):
|
|
language = "yaml"
|
|
kind = "ci"
|
|
elif rel.startswith(".github/scripts/"):
|
|
language = "python"
|
|
kind = "ci_script"
|
|
elif rel.endswith(".md"):
|
|
language = "markdown"
|
|
kind = "doc"
|
|
elif rel.endswith(".cff") or rel.endswith(".toml") or rel.endswith(".json") or rel.endswith(".txt"):
|
|
language = "config"
|
|
kind = "config"
|
|
else:
|
|
language = "other"
|
|
kind = "other"
|
|
|
|
text = path.read_text(errors="ignore")
|
|
imports: list[str] = []
|
|
module_name: str | None = None
|
|
build_target: str | None = None
|
|
if language == "lean":
|
|
imports = extract_lean_imports(text)
|
|
module_name = lean_path_to_module(Path(rel))
|
|
if module_name in root_set:
|
|
build_target = module_name
|
|
elif module_name.startswith("CoreFormalism."):
|
|
build_target = "SilverSightFormal"
|
|
elif module_name.startswith("SilverSightCore"):
|
|
build_target = "SilverSightCore"
|
|
else:
|
|
build_target = "SilverSightFormal"
|
|
elif language == "python":
|
|
imports = extract_python_imports(text)
|
|
|
|
layer_id = "other"
|
|
for layer in LAYERS:
|
|
if rel.startswith(layer["path"] + "/") or rel == layer["path"]:
|
|
layer_id = layer["id"]
|
|
break
|
|
|
|
entries.append({
|
|
"path": rel,
|
|
"layer": layer_id,
|
|
"language": language,
|
|
"kind": kind,
|
|
"module": module_name,
|
|
"build_target": build_target,
|
|
"status": file_status(rel),
|
|
"imports": imports,
|
|
"research_stack_source": RESEARCH_STACK_SOURCE.get(rel),
|
|
"role": ROLE_DESCRIPTIONS.get(rel, ""),
|
|
"receipt_boundary": rel in RECEIPT_BOUNDARY,
|
|
"line_count": len(text.splitlines()),
|
|
})
|
|
return entries
|
|
|
|
|
|
def build_layer_summary(entries: list[dict[str, Any]]) -> list[dict[str, Any]]:
|
|
summary: list[dict[str, Any]] = []
|
|
for layer in LAYERS:
|
|
layer_entries = [e for e in entries if e["layer"] == layer["id"]]
|
|
lean_files = [e for e in layer_entries if e["language"] == "lean"]
|
|
python_files = [e for e in layer_entries if e["language"] == "python"]
|
|
summary.append({
|
|
"id": layer["id"],
|
|
"name": layer["name"],
|
|
"path": layer["path"],
|
|
"description": layer["description"],
|
|
"file_count": len(layer_entries),
|
|
"lean_files": len(lean_files),
|
|
"python_files": len(python_files),
|
|
"active": len([e for e in layer_entries if e["status"] == "active"]),
|
|
"quarantined": len([e for e in layer_entries if e["status"] == "quarantined"]),
|
|
"archived": len([e for e in layer_entries if e["status"] == "archived"]),
|
|
})
|
|
return summary
|
|
|
|
|
|
def build_dependency_edges(entries: list[dict[str, Any]]) -> list[dict[str, str]]:
|
|
"""Build cross-file dependency edges for Lean and Python files."""
|
|
module_to_path: dict[str, str] = {e["module"]: e["path"] for e in entries if e["module"]}
|
|
edges: list[dict[str, str]] = []
|
|
for e in entries:
|
|
if e["language"] == "lean":
|
|
for imp in e["imports"]:
|
|
if imp in module_to_path:
|
|
edges.append({
|
|
"from": e["path"],
|
|
"to": module_to_path[imp],
|
|
"relation": "imports",
|
|
})
|
|
elif e["language"] == "python":
|
|
# Best-effort: map python/qubo local imports
|
|
for imp in e["imports"]:
|
|
candidate = imp.replace(".", "/") + ".py"
|
|
if (REPO_ROOT / candidate).exists():
|
|
edges.append({"from": e["path"], "to": candidate, "relation": "imports"})
|
|
return edges
|
|
|
|
|
|
def generate_markdown(data: dict[str, Any]) -> str:
|
|
lines: list[str] = []
|
|
lines.append("# SilverSight Project Map")
|
|
lines.append("")
|
|
lines.append("**Generated:** " + data["generated_at"])
|
|
lines.append("")
|
|
lines.append("**Source repo:** " + data["repo"])
|
|
lines.append("")
|
|
lines.append("**Tooling:** `python3 docs/generate_project_map.py` regenerates this file and `docs/PROJECT_MAP.json`.")
|
|
lines.append("")
|
|
lines.append("## 1. Project Overview")
|
|
lines.append("")
|
|
lines.append(f"- **Total tracked files:** {data['summary']['total_files']}")
|
|
lines.append(f"- **Lean files:** {data['summary']['lean_files']}")
|
|
lines.append(f"- **Python files:** {data['summary']['python_files']}")
|
|
lines.append(f"- **Active:** {data['summary']['active']} | **Quarantined:** {data['summary']['quarantined']} | **Archived:** {data['summary']['archived']}")
|
|
lines.append(f"- **Receipt-boundary files:** {data['summary']['receipt_boundary_files']}")
|
|
lines.append("")
|
|
lines.append("## 2. Layer Summary")
|
|
lines.append("")
|
|
lines.append("| Layer | Path | Files | Lean | Python | Active | Quarantined | Archived | Description |")
|
|
lines.append("|-------|------|-------|------|--------|--------|-------------|----------|-------------|")
|
|
for layer in data["layers"]:
|
|
lines.append(
|
|
f"| {layer['name']} | `{layer['path']}` | {layer['file_count']} | "
|
|
f"{layer['lean_files']} | {layer['python_files']} | {layer['active']} | "
|
|
f"{layer['quarantined']} | {layer['archived']} | {layer['description']} |"
|
|
)
|
|
lines.append("")
|
|
lines.append("## 3. File Inventory")
|
|
lines.append("")
|
|
for layer in data["layers"]:
|
|
layer_entries = [e for e in data["entries"] if e["layer"] == layer["id"]]
|
|
if not layer_entries:
|
|
continue
|
|
lines.append(f"### {layer['name']} (`{layer['path']}`)")
|
|
lines.append("")
|
|
lines.append("| File | Module | Build Target | Status | Receipt Boundary | Research-Stack Source | Role |")
|
|
lines.append("|------|--------|--------------|--------|------------------|----------------------|------|")
|
|
for e in layer_entries:
|
|
mod = e["module"] or "—"
|
|
bt = e["build_target"] or "—"
|
|
rb = "✅" if e["receipt_boundary"] else "—"
|
|
src = f"`{e['research_stack_source']}`" if e["research_stack_source"] else "—"
|
|
role = e["role"] or "—"
|
|
lines.append(
|
|
f"| `{e['path']}` | {mod} | {bt} | {e['status']} | {rb} | {src} | {role} |"
|
|
)
|
|
lines.append("")
|
|
lines.append("## 4. Key Build & Test Commands")
|
|
lines.append("")
|
|
lines.append("```bash")
|
|
lines.append("# Lean")
|
|
lines.append("lake build")
|
|
lines.append("lake build SilverSightFormal")
|
|
lines.append("lake build CoreFormalism.SidonSets")
|
|
lines.append("")
|
|
lines.append("# Python")
|
|
lines.append("python3 -m py_compile python/*.py qubo/*.py tests/*.py .github/scripts/*.py")
|
|
lines.append("pytest tests/ python/ qubo/ -v")
|
|
lines.append("")
|
|
lines.append("# Docs")
|
|
lines.append("python3 .github/scripts/glossary_lint.py")
|
|
lines.append("python3 docs/generate_project_map.py")
|
|
lines.append("```")
|
|
lines.append("")
|
|
lines.append("## 5. Dependency Rules")
|
|
lines.append("")
|
|
lines.append("- `Core/SilverSightCore.lean` imports nothing except Mathlib.")
|
|
lines.append("- Every library may import `Core/` and Mathlib, but **no library may import another library**.")
|
|
lines.append("- `formal/CoreFormalism/` is the canonical foundation; higher `formal/` directories may import `CoreFormalism/` but not each other.")
|
|
lines.append("- `python/` and `qubo/` are I/O shims; they may not contain admissibility logic.")
|
|
lines.append("- The `Receipt` is the only Core/library boundary.")
|
|
lines.append("")
|
|
lines.append("## 6. Legend")
|
|
lines.append("")
|
|
lines.append("| Field | Meaning |")
|
|
lines.append("|-------|---------|")
|
|
lines.append("| `active` | Builds and is part of the current surface. |")
|
|
lines.append("| `quarantined` | In `tests/quarantine/` or marked broken; not part of CI. |")
|
|
lines.append("| `archived` | Legacy filename; kept for reference only. |")
|
|
lines.append("| `Receipt Boundary` | File produces or consumes `Receipt` values across the Core/library boundary. |")
|
|
lines.append("")
|
|
return "\n".join(lines)
|
|
|
|
|
|
def main() -> None:
|
|
from datetime import datetime, timezone
|
|
|
|
entries = discover_files()
|
|
layers = build_layer_summary(entries)
|
|
edges = build_dependency_edges(entries)
|
|
|
|
active = [e for e in entries if e["status"] == "active"]
|
|
quarantined = [e for e in entries if e["status"] == "quarantined"]
|
|
archived = [e for e in entries if e["status"] == "archived"]
|
|
receipt_boundary = [e for e in entries if e["receipt_boundary"]]
|
|
|
|
data: dict[str, Any] = {
|
|
"schema": "silversight_project_map_v1",
|
|
"generated_at": datetime.now(timezone.utc).isoformat(),
|
|
"repo": "https://github.com/allaunthefox/SilverSight",
|
|
"local_path": str(REPO_ROOT),
|
|
"summary": {
|
|
"total_files": len(entries),
|
|
"lean_files": len([e for e in entries if e["language"] == "lean"]),
|
|
"python_files": len([e for e in entries if e["language"] == "python"]),
|
|
"active": len(active),
|
|
"quarantined": len(quarantined),
|
|
"archived": len(archived),
|
|
"receipt_boundary_files": len(receipt_boundary),
|
|
},
|
|
"layers": layers,
|
|
"entries": entries,
|
|
"edges": edges,
|
|
}
|
|
|
|
OUT_JSON.write_text(json.dumps(data, indent=2, ensure_ascii=False), encoding="utf-8")
|
|
OUT_MD.write_text(generate_markdown(data), encoding="utf-8")
|
|
|
|
print(f"Wrote {OUT_JSON}")
|
|
print(f"Wrote {OUT_MD}")
|
|
print(f"Tracked {len(entries)} files across {len(layers)} layers; {len(edges)} dependency edges.")
|
|
|
|
|
|
if __name__ == "__main__":
|
|
main()
|