diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index e10409ca..d65e9376 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -26,6 +26,24 @@ jobs: - run: uv run pytest -q - run: make check-example + browser: + name: WebKit dependency explorer regressions + runs-on: ubuntu-latest + timeout-minutes: 15 + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + - uses: astral-sh/setup-uv@c771a70e6277c0a99b617c7a806ffedaca235ff9 # v9.0.0 + with: + version: "0.12.1" + python-version: "3.13" + enable-cache: true + - name: Install locked browser test environment + run: uv sync --frozen --extra dev --extra browser + - name: Install WebKit and Linux system dependencies + run: uv run --frozen --extra browser playwright install --with-deps webkit + - name: Run dependency explorer browser regressions + run: uv run --frozen --extra dev --extra browser pytest -q tests/test_dag_viewer_browser.py + real-lean: name: real Lean (fixture toolchain) runs-on: ubuntu-latest @@ -83,7 +101,7 @@ jobs: AUTOFORM_REQUIRE_REAL_LEAN_TESTS: "1" windows-hardening: - name: Windows inspection, subprocess, and publication hardening + name: Windows capability, inspection, subprocess, and publication hardening runs-on: windows-latest timeout-minutes: 15 steps: diff --git a/README.md b/README.md index 4549558a..fe791eaf 100644 --- a/README.md +++ b/README.md @@ -61,6 +61,10 @@ Autoform keeps the roadmap and dependency graph as Markdown under format and command contracts, or browse the [Cabannes thesis example](skills/setup/assets/cabannes-thesis-project/README.md). +The browser publication presents large roadmaps as a full-page mathematics +atlas: authored areas and bounded hierarchy preserve readable context, while +dependency edges remain distinct from containment and repository provenance. + ## Development ```bash diff --git a/autoform_cli/README.md b/autoform_cli/README.md index 15d0fde1..30645c73 100644 --- a/autoform_cli/README.md +++ b/autoform_cli/README.md @@ -33,6 +33,7 @@ Frontmatter records checked facts: ```markdown --- article_id: af_5b0e4d3c2a1f09e8d7c6b5a4 +area: Analysis & Probability declaration: theorem origin: cited statement: formalized @@ -77,12 +78,46 @@ target, `bridged` for a result introduced between source targets, and Frontmatter is optional. A container article that only supplies prose and placement needs none at all; only checked facts are recorded. +The optional `area` field assigns a container to an authored mathematical +region in the knowledge atlas. Use mathematical areas such as `Foundations` or +`Geometry & Topology`, never repository or workflow buckets such as +`MathlibExt` or `catalog-01`. Autoform does not guess areas from paths, imports, +or titles. + +For a taxonomy maintained separately from article files, `blueprint/atlas.json` +may assign the same areas without moving pages: + +```json +{"schema":"autoform-atlas/v1","areas":{"Geometry & Topology":["topology","geometry"]}} +``` + +Every listed value is a roadmap node id, each node may appear once, and a +manifest assignment must agree with any `area:` already authored on that node. + +A repository-wide inventory may use a narrative leaf to summarize an existing +Lean module containing several declarations. Such a leaf sets +`catalog: module` and omits `declaration`, so it is never dispatched as one +proof task. A completed catalog records every exact compiled public name in +`lean:` and links a declaration ledger under `blueprint/sources/` from its exact +`## Sources` section; it may assert +`statement: formalized` and `proof: formalized` when the complete module has +been checked. It contributes to the neutral inventory metric and graph status +while remaining a readable catalog page, but stays outside the mathematical +`Scoped roadmap` completion percentage. + +`check --lean-root` and `audit --lean-root` resolve every compiled name the +catalog lists and audit validates the local ledger link. They cannot prove that +the list omitted no newly added public declaration; completeness remains an +authored assertion pending repository-inventory reconciliation. + ## Assertions and derived status An article asserts only facts a human or agent verified: | Key | Meaning | | --- | --- | +| `area: Geometry & Topology` | Authored mathematical region for atlas grouping. | +| `catalog: module` | A non-dispatchable leaf cataloging one existing Lean module. | | `statement: formalized` | The Lean statement exists and compiles. Requires `lean:`. | | `statement: retracted` | A revision retracted the statement while `lean:` still names the old declaration, which stays in the build until Formalize restates the article and records `statement: formalized` in its place. Requires `lean:`; invalid with `proof: formalized` or `mathlib: true`. CI's `autoform check` at an older `AUTOFORM_REF` rejects the marker, so move the pin first; until then, retract by removing `statement` and `proof` and keeping `lean:`. | | `proof: formalized` | The Lean proof compiles. Requires `statement: formalized` and `lean:`. Under the open policy it may rest on open statements, and the article is then conditional; only the derived `fully_proved` means complete and `sorry`-free. | @@ -291,11 +326,22 @@ and read-only: it neither contacts network services nor writes findings back into the blueprint. Pass `--json` for stable machine-readable output; a nonzero exit status means the audit found at least one issue. The machine-checkable `coverage/README.md` contract contains one `Area | Coverage | Evidence` table -with `MAPPED`, `DECOMPOSED`, `DEFERRED`, or `OUT` dispositions. `MAPPED` is -nonterminal; the other three explicitly disposition an area. Audit JSON includes -canonical rows, counts, and the exact coverage source hash, while -`publication.json` records aggregate counts without duplicating the authored -rows. +with `MAPPED`, `INVENTORIED`, `DECOMPOSED`, `DEFERRED`, or `OUT` dispositions. +`MAPPED` is nonterminal. `INVENTORIED` is the terminal disposition for exact +source accounting and must link to a `catalog: module` record, directly or +through a containing roadmap scope. `DECOMPOSED` is reserved for +source-grounded declaration articles and must link to one, directly or through +a containing roadmap scope. `DEFERRED` and `OUT` record an explicit later +milestone or exclusion. Audit JSON includes canonical rows, counts, and the +exact coverage source hash, while `publication.json` records aggregate counts +without duplicating the authored rows. + +One row carries one disposition, so represent both axes with distinct, +axis-qualified `Area` labels. For example, `Repository inventory / MathlibExt` +may be `INVENTORIED` while `Mathematical exposition / MathlibExt` remains +`MAPPED` and later becomes `DECOMPOSED`; duplicate exact area labels are +invalid. A broad inventory row may link a container and classify every catalog +below it while finer exposition rows evolve independently. The contract is read as published Markdown and fails closed. A table inside an HTML comment, a fenced block, or a four-space-indented block is documentation @@ -369,11 +415,13 @@ its second paragraph, since that one implicitly closes the first. `title="hidden hides nothing at all. So is evidence that is nothing but `TODO`, `TBD`, `pending`, `placeholder`, or `unknown`, or that opens with one of those as a marker such as `TODO: choose a milestone`. A status word that merely begins a sentence is fine: -"Pending Mathlib PR 1234" names something a reader can check. `DECOMPOSED` -evidence must contain at least one complete inline link to an existing roadmap -article, and *every* link it offers must resolve, fragments included, under the -same rules the audit applies. A link missing its closing parenthesis does not -render and does not count. +"Pending Mathlib PR 1234" names something a reader can check. `INVENTORIED` and +`DECOMPOSED` evidence must contain at least one complete inline link to an +existing roadmap article. Every linked roadmap scope must contain the role the +row claims: a module inventory for `INVENTORIED`, or a declaration-bearing leaf +for `DECOMPOSED`. Every local link it offers must resolve, fragments included, +under the same rules the audit applies. A link missing its closing parenthesis +does not render and does not count. Fragment checking uses the renderer rather than predicting it. Anchors come from running Python-Markdown with the extensions the generated `mkdocs.yml` enables @@ -390,7 +438,9 @@ a heading-affecting extension cannot silently invalidate the audit. `coverage.complete` in audit and `publication.json` means exactly one thing: every row the author declared has reached a terminal disposition, so no row is still `MAPPED`. It is a statement about the contract, not a measurement of the -project. +project. Terminal dispositions close different questions: `INVENTORIED` closes +exact source accounting, while `DECOMPOSED` says the area has source-grounded +declaration articles. One does not imply the other. It does **not** claim that the declared rows cover the source exhaustively, and it says nothing about whether the linked roadmap articles are formalized or @@ -398,6 +448,31 @@ proved. A project that declares one narrow area and disposes of it reports `complete` while most of its source remains undeclared. Exhaustiveness is an authoring judgement that no local check can make. +Module inventory counts are reported separately from formalization-target +completion. The target denominator, readiness count, declaration-kind totals, +and progress-state breakdown use non-container articles carrying +`declaration`; a `catalog: module` record contributes only to the separate +module-inventory count. The coverage `counts` object always includes an integer +`INVENTORIED` key, including zero when no row uses it. Status assertions on a +catalog remain accepted. The presentation calls a fully checked catalog +`inventory checked`, not a completed definition or result. The rendered site +and `autoform check` show the module-inventory count separately from those +target metrics. + +For an existing blueprint, migrate a catalog-only `DECOMPOSED` row to +`INVENTORIED`. If the same source also has declaration articles, keep that +inventory row and add distinct, axis-qualified `DECOMPOSED` rows for the +mathematical scopes; do not overwrite the inventory claim. Existing coverage +Markdown remains readable, but emitted audit and publication coverage uses +`autoform-coverage/v2`: `INVENTORIED` is a new disposition, terminal meaning, +and counts key. The shared-explorer publication manifest uses +`autoform-publication/v2`, as described below. Until migrated, a catalog-only +`DECOMPOSED` row +remains syntactically accepted but audit reports `coverage-role-mismatch`; a +catalog not reached by any `INVENTORIED` evidence also reports +`unclassified-inventory`. Target-completion percentages may change because +catalog records are no longer included in their denominator. + Publication and audit are deliberately different gates. The generated `blueprint-pages.yml` runs `check` and `render`; it does not run `audit`. An invalid coverage contract fails `render` before any output is written, but a @@ -700,7 +775,7 @@ autoform migrate article-ids blueprint --check `article_id` accepts opaque values in the form `af_` plus 24 lowercase hex digits. The planner validates uniqueness, proposes deterministic IDs for missing articles, includes exact source hashes, and is strictly read-only. -Runtime v3 and `autoform work` expose assigned IDs immediately; applying plans +The runtime and `autoform work` expose assigned IDs immediately; applying plans and preserving publication routes across path moves remain follow-up changes. Coordinate temporary cross-machine ownership without modifying the book: @@ -744,25 +819,39 @@ autoform-visualize blueprint ``` Build the publishable site source — a book overview, aggregate progress, -statement boxes with collapsed dependency details, multi-scale dependency -maps, and direct links to Lean declarations at the current commit: +statement boxes with collapsed dependency details, a multi-scale dependency +explorer, and direct links to Lean declarations at the current commit: ```bash autoform render blueprint --output site-src --lean-root . --require-declarations ``` `render` never writes into the vault. It leads the landing page with the project -map over a summary of what is formalized and what is unblocked, places a compact +explorer over a summary of what is formalized and what is unblocked, places a compact progress summary after each chapter's opening prose, writes `structure.md` so a vault's layout can be checked against the book it produces, and shows a source icon when a `lean:` declaration resolves to a repository permalink. Its -`dependencies.md` entry point rolls dependencies through the article hierarchy, -with links to declaration maps, one-hop local contexts, and the complete DAG. -Every graph article returns to the book, and every formal statement links to -its local context. Point `mkdocs.yml` at `docs_dir: site-src` and enable -`md_in_html` plus a `pymdownx.superfences` mermaid fence; see the [repository +`dependencies.md` opens a full-viewport application and rolls dependencies +through the article hierarchy, with bounded project, chapter, and nested-scope +projections. Global search loads a layout-free index and jumps to the smallest +useful scope; the compatibility `dependencies/full.md` route renders only the +project shell and never fits the whole repository into one canvas. Every generated +site projection uses the same deterministic JSON-derived Canvas and semantic-DOM +explorer with search, filters, pan/zoom, and hash-routed node neighborhoods, so +none inherits Mermaid's text, edge, or SVG-size ceilings. Authored Mermaid remains +supported in the vault and book, including the bounded graph produced by +`autoform-visualize`. Breadcrumbs return through the explorer hierarchy to the +book, and every formal statement links to the smallest explorer scope containing +that item. Point `mkdocs.yml` at `docs_dir: site-src` and enable `md_in_html` plus a +`pymdownx.superfences` mermaid fence; see the [repository example](../skills/setup/assets/cabannes-thesis-project/mkdocs.yml). +This shared-explorer layout is recorded as `autoform-publication/v2`; it +replaces the v1 `dependencies/nodes/*.html` focus pages. Legacy +`dependencies/full.html#node=` links use the global index to redirect to the +smallest bounded scope containing that node. Existing v1 output directories +remain recognized so a normal clean render upgrades them in place. + ## Validation `autoform check` rejects cycles, missing targets, escaping paths, @@ -809,7 +898,8 @@ roadmap root and the book loses a level. `missing-chapter-article` reports a directory directly under `roadmap/` that holds articles but names no chapter. Deeper directories (the `definitions/` and `theorems/` buckets the bundled example uses) are a filing convention inside a chapter and are not checked. -`overfull-container` reports an article with more than 24 direct children, +`overfull-container` reports a mathematical article with more than 24 direct +children, or a repository-wide root subject index with more than 64, which is a table of contents rather than a chapter. Both defects leave a valid graph, which is why they need their own checks rather than falling out of `autoform check`. @@ -1095,7 +1185,7 @@ doctor, separate from any future worker fleet or machine-capability preflight. ## Runtime contract `autoform_cli.runtime` projects the canonical Markdown graph into the versioned, -deeply immutable in-memory schema `autoform-runtime/v3`. Its declared authority +deeply immutable in-memory schema `autoform-runtime/v4`. Its declared authority is `markdown-articles`: the adapter copies hierarchy, typed statement and proof dependencies, authored assertions, derived progress, provenance, and optional local Lean source locations, but it provides no persistence or write API. @@ -1106,28 +1196,38 @@ creates, synchronizes, or treats `graph.json` as an authority. Every article remains in the runtime view so consumers can preserve the book's arbitrary containment hierarchy. A node is dispatchable only when it is both a formalizable article and a leaf; narrative containers and prose-only leaves are -never proof work units. The source revision hashes exact roadmap article paths -and bytes, excluding timestamps, absolute paths, Git state, and operational -state. Optional Lean locations come from a local lexical scan and do not by -themselves establish compilation or proof correctness. - -Schema v3 retains optional durable `article_id` metadata beside the graph's -path-derived `id` and adds the project `open_statements` policy, +never proof work units. Module inventories are likewise non-formalizable, +non-dispatchable source records. The source revision hashes exact roadmap +article paths and bytes, excluding timestamps, absolute paths, Git state, and +operational state. Optional Lean locations come from a local lexical scan and do +not by themselves establish compilation or proof correctness. + +Schema v4 adds a nullable catalog discriminator for non-dispatchable module +inventories. It retains v3's optional durable `article_id` metadata beside the +graph's path-derived `id`, project `open_statements` policy, `statement_retracted` assertions, and each status's `assumes` and `waiting_on` fields. Temporary claims and local dashboard hooks may fall back to the path ID, -but durable execution records and routes must require `article_id` until the -path-move migration is complete. Operational state remains private and excluded -from runtime snapshots and publication. +but durable queues, reviews, recovery records, PR markers, execution records, +routes, providers, and logs must require `article_id` until path-move migration +is complete. Operational state remains private and excluded from runtime +snapshots and publication. ## Publication contract -`autoform render` publishes the book, derived progress, and dependency maps at -project, chapter, nested-scope, local, and full-graph scales. It never reads a +`autoform render` publishes the book, derived progress, and one dependency +explorer as bounded project, chapter, and nested-scope projections. The legacy +full route is a project-scale compatibility shell backed by a layout-free global +search index, never an all-repository node cloud. Rendering never reads a `graph.json` or an operational queue. Hidden files are omitted, while symlinks, credentials, logs, provider state, and agent/task state inside the blueprint cause the render to fail rather than silently leak them. Source and output directories must be disjoint. Every render writes `publication.json` with the source-content hash, Git ref, -article and dependency counts, and available views. It contains no timestamp or -absolute path, so identical inputs produce identical output files. +article and dependency counts, available views, and whether capture used a +retained directory descriptor or the documented portable best-effort path. It +contains no timestamp or absolute path, so identical inputs on the same +filesystem-capability class produce identical output files. +Rendering reads only one retained source snapshot. Later edits cannot mix into +the output; they instead make the dashboard report the built site as stale +until it is rendered again. diff --git a/autoform_cli/__main__.py b/autoform_cli/__main__.py index 6ac53138..e0c04fc7 100644 --- a/autoform_cli/__main__.py +++ b/autoform_cli/__main__.py @@ -380,17 +380,41 @@ def _check(args: argparse.Namespace) -> int: linker = None if args.lean_root is not None: + lean_names = tuple( + dict.fromkeys( + name + for node in graph.nodes.values() + for name in declaration_names(node.lean or "") + ) + ) try: - linker = build_linker(args.lean_root) + linker = build_linker(args.lean_root, names=lean_names) except OSError as error: print(f"error: {index_failure_message(error)}") return 1 statuses = status.derive(graph) - summary = " · ".join(f"{count} {state.label}" for state, count in status.summarize(statuses)) + containers = frozenset( + node.parent for node in graph.nodes.values() if node.parent is not None + ) + target_statuses = { + node_id: statuses[node_id] + for node_id, node in graph.nodes.items() + if node_id not in containers and node.formalizable + } + inventories = sum( + node_id not in containers and node.catalog == "module" + for node_id, node in graph.nodes.items() + ) + summary = " · ".join( + f"{count} {state.label}" for state, count in status.summarize(target_statuses) + ) print(f"OK: {len(graph.nodes)} articles, {graph.edge_count} dependencies") if summary: print(f" {summary}") + if inventories: + label = "module inventory" if inventories == 1 else "module inventories" + print(f" {inventories} {label}") if linker is None: return 0 @@ -423,6 +447,7 @@ def _audit(args: argparse.Namespace) -> int: " coverage: " f"{counts['MAPPED']} mapped · " f"{counts['DECOMPOSED']} decomposed · " + f"{counts['INVENTORIED']} inventoried · " f"{counts['DEFERRED']} deferred · " f"{counts['OUT']} out" ) diff --git a/autoform_cli/_tree_snapshot.py b/autoform_cli/_tree_snapshot.py index 8cf46d03..c08c43d0 100644 --- a/autoform_cli/_tree_snapshot.py +++ b/autoform_cli/_tree_snapshot.py @@ -154,6 +154,8 @@ def _materialize_regular_files( directories: tuple[tuple[str, tuple[str, ...]], ...], files: tuple[tuple[str, tuple[str, ...], bytes], ...], placeholders: tuple[tuple[str, tuple[str, ...]], ...], + *, + verify_bytes: bool, ) -> None: """Create a snapshot using only retained directory descriptors.""" @@ -255,16 +257,27 @@ def _materialize_regular_files( ) ) - _verify_materialized_snapshot( - descriptors[()], - root_identity, - directories, - files, - placeholders, - directory_identities, - directory_permissions, - created_files, - ) + _tree_snapshot_checkpoint("before-materialization-final-verification", "") + if verify_bytes: + _verify_materialized_snapshot( + descriptors[()], + root_identity, + directories, + files, + placeholders, + directory_identities, + directory_permissions, + created_files, + ) + else: + _verify_materialized_metadata( + descriptors, + directories, + files, + placeholders, + directory_identities, + created_files, + ) parent.verify() _verify_named_directory(parent.descriptor, name, root_identity) succeeded = True @@ -453,6 +466,55 @@ def _verify_materialized_snapshot( raise TreeSnapshotError("materialized file metadata changed before commit") +def _verify_materialized_metadata( + descriptors: dict[tuple[str, ...], int], + directories: tuple[tuple[str, tuple[str, ...]], ...], + files: tuple[tuple[str, tuple[str, ...], bytes], ...], + placeholders: tuple[tuple[str, tuple[str, ...]], ...], + directory_identities: dict[tuple[str, ...], tuple[int, int, int]], + created_files: list[tuple[tuple[str, ...], tuple[int, ...]]], +) -> None: + """Verify exact names, kinds and metadata without rereading captured bytes.""" + + expected_names: dict[tuple[str, ...], set[str]] = { + parts: set() for _relative, parts in directories + } + for _relative, parts in directories: + if parts: + expected_names.setdefault(parts[:-1], set()).add(parts[-1]) + for _relative, parts, _data in files: + expected_names.setdefault(parts[:-1], set()).add(parts[-1]) + for _relative, parts in placeholders: + expected_names.setdefault(parts[:-1], set()).add(parts[-1]) + + for parts, names in expected_names.items(): + descriptor = descriptors.get(parts) + expected_identity = directory_identities.get(parts) + if descriptor is None or expected_identity is None: + raise TreeSnapshotError("materialized tree has a missing directory") + if _directory_entry_identity(os.fstat(descriptor)) != expected_identity: + raise TreeSnapshotError("materialized directory metadata changed before commit") + if tuple(sorted(os.listdir(descriptor))) != tuple(sorted(names)): + raise TreeSnapshotError("materialized tree changed before commit") + if parts: + parent_descriptor = descriptors.get(parts[:-1]) + if parent_descriptor is None: + raise TreeSnapshotError("materialized tree has a missing directory") + _verify_named_directory(parent_descriptor, parts[-1], expected_identity) + + for parts, expected_signature in created_files: + parent_descriptor = descriptors.get(parts[:-1]) + if parent_descriptor is None: + raise TreeSnapshotError("materialized file has a missing parent") + observed = os.stat( + parts[-1], + dir_fd=parent_descriptor, + follow_symlinks=False, + ) + if _stat_signature(observed) != expected_signature: + raise TreeSnapshotError("materialized file metadata changed before commit") + + def _cleanup_materialization( parent: RetainedDirectory | None, root_name: str, @@ -630,16 +692,21 @@ def generation_revision(self) -> str: _update_digest(digest, b"identity", relative, encoded) return digest.hexdigest() - def materialize(self, destination: Path) -> None: + def materialize(self, destination: Path, *, verify_bytes: bool = True) -> None: """Write captured regular files below a fresh private directory.""" issues = self.unsupported_entries() if issues: relative, reason = issues[0] raise TreeSnapshotError(f"{relative}: {reason}") - self.materialize_regular_files(destination) + self.materialize_regular_files(destination, verify_bytes=verify_bytes) - def materialize_regular_files(self, destination: Path) -> None: + def materialize_regular_files( + self, + destination: Path, + *, + verify_bytes: bool = True, + ) -> None: """Materialize safe content after a caller has recorded invalid entries.""" directory_parts = tuple( @@ -662,6 +729,7 @@ def materialize_regular_files(self, destination: Path) -> None: for (relative, data), (_validated, parts) in zip(self.files, file_parts) ), placeholder_parts, + verify_bytes=verify_bytes, ) def unsupported_entries(self) -> tuple[tuple[str, str], ...]: diff --git a/autoform_cli/audit.py b/autoform_cli/audit.py index bedcac5f..7f2dabe9 100644 --- a/autoform_cli/audit.py +++ b/autoform_cli/audit.py @@ -13,9 +13,10 @@ from bisect import bisect_right from dataclasses import asdict, dataclass from pathlib import Path +from urllib.parse import unquote, urlsplit from . import status -from .coverage import CoverageSummary, load_coverage +from .coverage import CoverageSummary, load_coverage, validate_coverage_roles from .graph import Graph, GraphValidationError, Node, load_graph from .lean import ( _DECLARATION, @@ -27,14 +28,17 @@ snapshot_project_sources, ) from .markdown import FENCE as _FENCE -from .markdown import frontmatter_end as _frontmatter_end from .markdown import HEADING as _HEADING from .markdown import HTML_COMMENT as _HTML_COMMENT +from .markdown import frontmatter_end as _frontmatter_end from .markdown import local_target_issue as _local_target_issue from .markdown import markdown_links as _markdown_links #: More siblings than this at one level is a table of contents, not a chapter. _MAX_DIRECT_CHILDREN = 24 +#: A repository-wide subject index is itself a table of contents and can be +#: wider than a readable mathematical chapter while remaining navigable. +_MAX_ROOT_CHILDREN = 64 #: A node is reported as oversized only once its finished Lean work clears both #: an absolute floor and a large multiple of this project's own median. The @@ -176,6 +180,7 @@ def audit_graph( "formalizable article has contained articles; declaration-sized articles must be leaves", ) ) + if not article.statement_text: findings.append( AuditFinding( @@ -201,13 +206,51 @@ def audit_graph( ) ) - if len(children) > _MAX_DIRECT_CHILDREN: + if node.catalog and children: + findings.append( + AuditFinding( + article_path, + "catalog-container", + "catalog article has contained articles; a module catalog must be a leaf", + ) + ) + + if node.catalog and not _has_catalog_ledger(graph, node): + findings.append( + AuditFinding( + article_path, + "catalog-without-ledger", + "module catalog has no local declaration ledger under blueprint/sources", + ) + ) + + if ( + node.catalog + and (node.statement_formalized or node.proof_formalized) + and not declaration_names(node.lean or "") + ): + findings.append( + AuditFinding( + article_path, + "catalog-without-lean-targets", + "formalized module catalog has no exact compiled names in lean frontmatter", + ) + ) + + repository_subject_index = ( + node.id == "roadmap" + and node.parent is None + and bool(children) + and all(graph.nodes[child].path.name == "README.md" for child in children) + ) + child_limit = _MAX_ROOT_CHILDREN if repository_subject_index else _MAX_DIRECT_CHILDREN + if len(children) > child_limit: findings.append( AuditFinding( article_path, "overfull-container", f"article directly contains {len(children)} articles, more than the " - f"{_MAX_DIRECT_CHILDREN}-article limit; group them into chapters", + f"{child_limit}-article limit; group them into chapters", ) ) @@ -229,12 +272,12 @@ def audit_graph( or bool(node.mathlib_file) or derived[node_id].proved ) - if not children and formalization_evidence and not node.declaration: + if not children and formalization_evidence and not (node.declaration or node.catalog): findings.append( AuditFinding( article_path, "missing-declaration-intent", - "formalization-bearing leaf has no declaration intent metadata", + "formalization-bearing leaf has neither declaration nor catalog intent metadata", ) ) @@ -243,11 +286,31 @@ def audit_graph( if coverage_findings is None: coverage, coverage_findings = _coverage_findings(graph.blueprint_dir) findings.extend(coverage_findings) + if coverage is not None: + findings.extend(_coverage_role_findings(graph, coverage)) if lean_root is not None: findings.extend(_lean_findings(graph, lean_root)) return _result(findings, coverage=coverage) +def _has_catalog_ledger(graph: Graph, node: Node) -> bool: + """Whether a catalog links a repository-local declaration ledger.""" + + sources = (graph.blueprint_dir / "sources").resolve() + for target in node.sources: + split = urlsplit(target) + if split.scheme or split.netloc or split.query or not split.path: + continue + try: + candidate = (node.path.parent / unquote(split.path)).resolve() + candidate.relative_to(sources) + except (OSError, ValueError): + continue + if candidate.is_file(): + return True + return False + + @dataclass(frozen=True, slots=True) class _ArticleShape: statement_text: bool @@ -366,6 +429,22 @@ def _coverage_findings( return coverage, findings +def _coverage_role_findings( + graph: Graph, + coverage: CoverageSummary, +) -> list[AuditFinding]: + """Project public coverage-role issues into the audit result model.""" + + return [ + AuditFinding( + "coverage/README.md", + issue.code, + f"{issue.reason}{f' (line {issue.line})' if issue.line else ''}", + ) + for issue in validate_coverage_roles(graph, coverage) + ] + + def _lean_findings(graph: Graph, lean_root: str | Path) -> list[AuditFinding]: root = Path(lean_root).expanduser().resolve() if not root.is_dir(): @@ -378,8 +457,15 @@ def _lean_findings(graph: Graph, lean_root: str | Path) -> list[AuditFinding]: ] findings: list[AuditFinding] = [] + names_to_resolve = tuple( + dict.fromkeys( + name + for node in graph.nodes.values() + for name in declaration_names(node.lean or "") + ) + ) try: - snapshot = snapshot_project_sources(root) + snapshot = snapshot_project_sources(root, names=names_to_resolve) except OSError as error: return [ AuditFinding( @@ -410,6 +496,12 @@ def _lean_findings(graph: Graph, lean_root: str | Path) -> list[AuditFinding]: else: resolved.append(declaration) + # Catalog declarations must resolve like every other asserted Lean + # target. Only declaration-specific policy is inapplicable to a + # non-dispatchable inventory container. + if node.catalog is not None: + continue + for declaration in resolved: if _declared_deprecated(declaration, sources): findings.append( @@ -431,7 +523,7 @@ def _lean_findings(graph: Graph, lean_root: str | Path) -> list[AuditFinding]: ) ) - if resolved: + if resolved and node.catalog is None: sizes[node_id] = sum(spans[declaration.name] for declaration in resolved) findings.extend(_size_findings(graph, sizes)) diff --git a/autoform_cli/coverage.py b/autoform_cli/coverage.py index 763cca50..8f1bd12f 100644 --- a/autoform_cli/coverage.py +++ b/autoform_cli/coverage.py @@ -14,6 +14,7 @@ from collections import Counter from dataclasses import asdict, dataclass from pathlib import Path +from typing import TYPE_CHECKING from urllib.parse import unquote, urlsplit from .markdown import ( @@ -27,8 +28,11 @@ rendered_visible_text, ) -COVERAGE_SCHEMA = "autoform-coverage/v1" -COVERAGE_DISPOSITIONS = ("MAPPED", "DECOMPOSED", "DEFERRED", "OUT") +if TYPE_CHECKING: + from .graph import Graph + +COVERAGE_SCHEMA = "autoform-coverage/v2" +COVERAGE_DISPOSITIONS = ("MAPPED", "DECOMPOSED", "INVENTORIED", "DEFERRED", "OUT") _EXPECTED_HEADER = ("Area", "Coverage", "Evidence") _SEPARATOR = re.compile(r"^:?-{3,}:?$") @@ -51,6 +55,15 @@ class CoverageIssue: reason: str +@dataclass(frozen=True, order=True, slots=True) +class CoverageRoleIssue: + """One graph-semantic mismatch in an otherwise valid coverage contract.""" + + line: int + code: str + reason: str + + @dataclass(frozen=True, slots=True) class CoverageEntry: """One source area and its explicit roadmap disposition.""" @@ -88,8 +101,9 @@ def complete(self) -> bool: """Whether every author-declared row reached a terminal disposition. Terminal means the row is no longer ``MAPPED`` -- the author has either - decomposed it into roadmap articles, deferred it to a named milestone, - or excluded it with a reason. + decomposed it into declaration-sized mathematical articles, inventoried + it in module catalogs, deferred it to a named milestone, or excluded it + with a reason. This is a claim about the *contract*, not about the project. It does not establish that the declared rows cover the source exhaustively, and it @@ -144,6 +158,119 @@ def load_coverage(blueprint_dir: str | Path) -> tuple[CoverageSummary | None, tu ) +def validate_coverage_roles( + graph: Graph, + coverage: CoverageSummary, +) -> tuple[CoverageRoleIssue, ...]: + """Validate exposition and inventory evidence against *graph*. + + :func:`load_coverage` remains a syntax-only operation. Callers that already + have a validated graph use this second phase to distinguish declaration + exposition from module inventory before auditing or publishing. + """ + + contained: dict[str, list[str]] = {} + for node in graph.nodes.values(): + if node.parent is not None: + contained.setdefault(node.parent, []).append(node.id) + + issues: list[CoverageRoleIssue] = [] + inventoried: set[str] = set() + catalog_nodes = {node_id for node_id, node in graph.nodes.items() if node.catalog} + + for entry in coverage.entries: + role = { + "DECOMPOSED": "declaration", + "INVENTORIED": "catalog", + }.get(entry.disposition) + if role is None: + continue + + targets = _coverage_target_nodes(graph, coverage, entry.evidence) + role_scopes = [ + _leaf_role_nodes(graph, contained, node_id, role=role) for node_id in targets + ] + if not targets or any(not scope for scope in role_scopes): + issues.append( + CoverageRoleIssue( + entry.line, + "coverage-role-mismatch", + f"coverage area {entry.area!r} is {entry.disposition}, but each roadmap " + f"link must resolve to a {role} leaf or a container with {role} descendants", + ) + ) + + if entry.disposition == "INVENTORIED": + for scope in role_scopes: + inventoried.update(scope) + + unclassified = catalog_nodes - inventoried + if unclassified: + noun = "article" if len(unclassified) == 1 else "articles" + issues.append( + CoverageRoleIssue( + 0, + "unclassified-inventory", + f"coverage contract leaves {len(unclassified)} catalog {noun} outside " + "INVENTORIED evidence; link each inventory area directly or through a " + "containing roadmap article", + ) + ) + return tuple(issues) + + +def _coverage_target_nodes( + graph: Graph, + coverage: CoverageSummary, + evidence: str, +) -> tuple[str, ...]: + """Resolve the roadmap nodes visibly linked by one coverage evidence cell.""" + + coverage_path = graph.blueprint_dir / coverage.source_path + by_path = {node.path.resolve(): node_id for node_id, node in graph.nodes.items()} + resolved: list[str] = [] + for target in link_targets(evidence): + split = urlsplit(target) + if split.scheme or split.netloc: + continue + raw_path = unquote(split.path) + if not raw_path or "\x00" in raw_path: + continue + try: + candidate = (coverage_path.parent / Path(raw_path)).resolve() + except (OSError, RuntimeError, ValueError): + continue + node_id = by_path.get(candidate) + if node_id is not None and node_id not in resolved: + resolved.append(node_id) + return tuple(resolved) + + +def _leaf_role_nodes( + graph: Graph, + contained: dict[str, list[str]], + root_id: str, + *, + role: str, +) -> set[str]: + """Return role-bearing leaves at or beneath one coverage target.""" + + found: set[str] = set() + pending = [root_id] + seen: set[str] = set() + while pending: + node_id = pending.pop() + if node_id in seen: + continue + seen.add(node_id) + children = contained.get(node_id, ()) + if children: + pending.extend(children) + elif getattr(graph.nodes[node_id], role) is not None: + found.add(node_id) + return found + + def _parse_table(text: str) -> tuple[list[CoverageEntry], list[CoverageIssue]]: # Only published Markdown can carry the contract. Commented-out and # code-block tables are masked to blank lines first, which keeps every @@ -478,15 +605,16 @@ def _validate_evidence( if _is_placeholder(visible_evidence): issues.append(CoverageIssue(entry.line, "coverage evidence is a placeholder")) continue - if entry.disposition != "DECOMPOSED": + if entry.disposition not in {"DECOMPOSED", "INVENTORIED"}: continue + disposition = entry.disposition targets = link_targets(entry.evidence) if not targets: issues.append( CoverageIssue( entry.line, - "DECOMPOSED coverage evidence must link to at least one roadmap article", + f"{disposition} coverage evidence must link to at least one roadmap article", ) ) continue @@ -505,7 +633,7 @@ def _validate_evidence( issues.append( CoverageIssue( entry.line, - "DECOMPOSED coverage evidence has no link to an existing roadmap article", + f"{disposition} coverage evidence has no link to an existing roadmap article", ) ) return issues @@ -611,6 +739,8 @@ def _inline_code(value: str) -> str: "COVERAGE_SCHEMA", "CoverageEntry", "CoverageIssue", + "CoverageRoleIssue", "CoverageSummary", "load_coverage", + "validate_coverage_roles", ] diff --git a/autoform_cli/dag_viewer.py b/autoform_cli/dag_viewer.py new file mode 100644 index 00000000..5a2a7192 --- /dev/null +++ b/autoform_cli/dag_viewer.py @@ -0,0 +1,1619 @@ +"""Static payloads and the dependency-free Autoform graph explorer. + +The graph is laid out once, deterministically, while rendering the site. The +browser paints topology on Canvas and places ordinary DOM controls over visible +nodes, so a large graph remains responsive without becoming a bitmap-only UI. +""" + +from __future__ import annotations + +import heapq +import html +import json +import math +from collections import defaultdict +from collections.abc import Iterable, Mapping +from pathlib import Path +from urllib.parse import quote, urlsplit + +from .graph_views import INVENTORY_CHECKED_STATUS, GraphView, ViewNode +from .status import STATES + +SCHEMA = "autoform-dag-view/v2" +SEARCH_SCHEMA = "autoform-dag-search/v1" +MAX_LAYOUT_ROWS = 160 +MAX_MERMAID_CHARACTERS = 40_000 +MAX_MERMAID_EDGE_LINES = 450 + +_NODE_WIDTH = 196 +_NODE_HEIGHT = 56 +_COLUMN_GAP = 116 +_ROW_GAP = 24 + + +def requires_interactive(view: GraphView, mermaid_source: str) -> bool: + """Retain the old threshold helper for third-party integrations.""" + edge_lines = sum(bool(edge.statement_count) + bool(edge.proof_count) for edge in view.edges) + return len(mermaid_source) > MAX_MERMAID_CHARACTERS or edge_lines > MAX_MERMAID_EDGE_LINES + + +def _positions(view: GraphView) -> dict[str, dict[str, int]]: + """Return stable, bounded-row coordinates without a browser force layout.""" + if _uses_atlas(view): + return _atlas_positions(view) + all_node_ids = [node.id for node in view.nodes] + known = set(all_node_ids) + if len(known) != len(all_node_ids): + raise ValueError("dependency view contains duplicate node ids") + connected: set[str] = set() + for edge in view.edges: + if edge.source not in known or edge.target not in known: + raise ValueError("dependency view edge names an unknown node") + if edge.source in known and edge.target in known and edge.source != edge.target: + connected.update((edge.source, edge.target)) + + # Isolates are searchable inventory, not visible dependency topology by + # default. Lay out the connected graph without reserving thousands of + # blank columns, then park isolates in a separate stable grid that appears + # only when the reader asks for it. + node_ids = [node_id for node_id in all_node_ids if node_id in connected] + order_index = {node_id: index for index, node_id in enumerate(node_ids)} + outgoing: dict[str, list[str]] = {node_id: [] for node_id in node_ids} + incoming: dict[str, list[str]] = {node_id: [] for node_id in node_ids} + indegree = {node_id: 0 for node_id in node_ids} + for edge in view.edges: + if edge.source not in indegree or edge.target not in indegree or edge.source == edge.target: + continue + outgoing[edge.source].append(edge.target) + incoming[edge.target].append(edge.source) + indegree[edge.target] += 1 + + ready = [(order_index[node_id], node_id) for node_id in node_ids if indegree[node_id] == 0] + heapq.heapify(ready) + ranks = {node_id: 0 for node_id in node_ids} + placed: set[str] = set() + while ready: + _, node_id = heapq.heappop(ready) + if node_id in placed: + continue + placed.add(node_id) + for target in sorted(outgoing[node_id], key=order_index.__getitem__): + ranks[target] = max(ranks[target], ranks[node_id] + 1) + indegree[target] -= 1 + if indegree[target] == 0: + heapq.heappush(ready, (order_index[target], target)) + + # Fine graphs are acyclic, but a collapsed chapter projection can contain + # a cycle. Place that remainder in stable source order rather than failing + # or handing layout to a non-deterministic force simulation. + for node_id in node_ids: + if node_id in placed: + continue + earlier = [ranks[source] for source in incoming[node_id] if order_index[source] < order_index[node_id]] + ranks[node_id] = max(earlier, default=-1) + 1 + + by_rank: dict[int, list[str]] = defaultdict(list) + for node_id in node_ids: + by_rank[ranks[node_id]].append(node_id) + + prior_slots: dict[str, int] = {} + for rank in sorted(by_rank): + candidates = by_rank[rank] + if rank: + candidates.sort( + key=lambda node_id: ( + sum(prior_slots[source] for source in incoming[node_id] if source in prior_slots) + / max(1, sum(source in prior_slots for source in incoming[node_id])), + order_index[node_id], + ) + ) + for slot, node_id in enumerate(candidates): + prior_slots[node_id] = slot + + column_bases: dict[int, int] = {} + next_column = 0 + for rank in sorted(by_rank): + column_bases[rank] = next_column + next_column += max(1, (len(by_rank[rank]) + MAX_LAYOUT_ROWS - 1) // MAX_LAYOUT_ROWS) + + result: dict[str, dict[str, int]] = {} + for rank in sorted(by_rank): + for slot, node_id in enumerate(by_rank[rank]): + column = column_bases[rank] + slot // MAX_LAYOUT_ROWS + row = slot % MAX_LAYOUT_ROWS + result[node_id] = { + "column": column, + "height": _NODE_HEIGHT, + "order": slot, + "rank": rank, + "row": row, + "width": _NODE_WIDTH, + "x": column * (_NODE_WIDTH + _COLUMN_GAP), + "y": row * (_NODE_HEIGHT + _ROW_GAP), + } + + isolated = [node_id for node_id in all_node_ids if node_id not in connected] + isolate_base = max((position["column"] for position in result.values()), default=-2) + 2 + # A single 160-row column made a project of 30 chapters fit as unreadable + # specks. Balance inventory-only siblings for a widescreen reading surface; + # dependency-connected nodes keep their ranked DAG positions above. + cell_aspect = (_NODE_HEIGHT + _ROW_GAP) / (_NODE_WIDTH + _COLUMN_GAP) + isolate_columns = max(1, math.ceil(math.sqrt(len(isolated) * cell_aspect * (16 / 9)))) + for slot, node_id in enumerate(isolated): + column = isolate_base + slot % isolate_columns + row = slot // isolate_columns + result[node_id] = { + "column": column, + "height": _NODE_HEIGHT, + "order": slot, + "rank": 0, + "row": row, + "width": _NODE_WIDTH, + "x": column * (_NODE_WIDTH + _COLUMN_GAP), + "y": row * (_NODE_HEIGHT + _ROW_GAP), + } + return result + + +def _uses_atlas(view: GraphView) -> bool: + scopes = [node for node in view.nodes if node.kind == "scope"] + return bool(scopes) and (not view.edges or any(node.area for node in scopes)) + + +def _atlas_positions(view: GraphView) -> dict[str, dict[str, int]]: + """Pack weighted topic bubbles inside authored mathematical regions.""" + gap = 14 + + def diameter(node: ViewNode) -> int: + count = max(1, len(node.members)) + if node.kind == "scope": + return max(92, min(164, round(72 + 11 * math.log2(count + 1)))) + if node.kind == "boundary": + return 104 + return 76 + + by_area: dict[str, list[tuple[int, ViewNode]]] = defaultdict(list) + for index, node in enumerate(view.nodes): + by_area[node.area or ""].append((index, node)) + + blocks: list[tuple[str, dict[str, dict[str, int]], int, int]] = [] + for area, indexed in sorted(by_area.items(), key=lambda item: (not item[0], item[0].casefold())): + indexed.sort(key=lambda item: (-diameter(item[1]), item[1].title.casefold(), item[1].id)) + dimensions = {node.id: diameter(node) for _, node in indexed} + total_area = sum((dimensions[node.id] + gap) ** 2 for _, node in indexed) + target_width = max( + max(dimensions.values(), default=_NODE_WIDTH), + round(math.sqrt(total_area * 1.1)), + ) + local: dict[str, dict[str, int]] = {} + x = 0 + y = 34 if area else 0 + row_height = 0 + row = 0 + widest = 0 + for order, node in indexed: + size = dimensions[node.id] + if x and x + size > target_width: + x = 0 + y += row_height + gap + row += 1 + row_height = 0 + local[node.id] = { + "column": x, + "height": size, + "order": order, + "rank": 0, + "row": row, + "width": size, + "x": x, + "y": y, + } + x += size + gap + widest = max(widest, x - gap) + row_height = max(row_height, size) + blocks.append((area, local, widest, y + row_height)) + + total_block_area = sum((width + gap * 2) * (height + gap * 2) for _, _, width, height in blocks) + atlas_width = max(1, round(math.sqrt(total_block_area * 1.1))) + result: dict[str, dict[str, int]] = {} + block_x = block_y = block_row_height = 0 + for _area, local, width, height in blocks: + if block_x and block_x + width > atlas_width: + block_x = 0 + block_y += block_row_height + gap * 2 + block_row_height = 0 + for node_id, position in local.items(): + shifted = dict(position) + shifted["x"] += block_x + shifted["y"] += block_y + shifted["column"] = shifted["x"] + result[node_id] = shifted + block_x += width + gap * 2 + block_row_height = max(block_row_height, height) + return result + + +def _atlas_regions(view: GraphView, positions: Mapping[str, Mapping[str, int]]) -> list[dict[str, object]]: + regions: list[dict[str, object]] = [] + areas = sorted({node.area for node in view.nodes if node.area}, key=str.casefold) + for area in areas: + members = [node for node in view.nodes if node.area == area] + min_x = min(positions[node.id]["x"] for node in members) + min_y = min(positions[node.id]["y"] for node in members) - 34 + max_x = max(positions[node.id]["x"] + positions[node.id]["width"] for node in members) + max_y = max(positions[node.id]["y"] + positions[node.id]["height"] for node in members) + regions.append( + { + "count": len(members), + "height": max_y - min_y + 24, + "label": area, + "width": max_x - min_x + 24, + "x": min_x - 12, + "y": min_y - 12, + } + ) + return regions + + +def _palette() -> dict[str, dict[str, object]]: + palette: dict[str, dict[str, object]] = { + state.key: { + "label": state.label, + "light": {"fill": state.fill, "stroke": state.stroke, "text": state.text}, + "dark": {"fill": state.dark_fill, "stroke": state.dark_stroke, "text": state.dark_text}, + } + for state in STATES + } + planned = next(state for state in STATES if state.key == "planned") + palette[INVENTORY_CHECKED_STATUS] = { + "label": "inventory checked", + "neutral": True, + "light": {"fill": planned.fill, "stroke": planned.stroke, "text": planned.text}, + "dark": {"fill": planned.dark_fill, "stroke": planned.dark_stroke, "text": planned.dark_text}, + } + return palette + + +def write_payload( + path: Path, + view: GraphView, + *, + links: Mapping[str, str], + breadcrumbs: Iterable[tuple[str, str | None]] = (), +) -> Path: + """Write deterministic v2 graph data while preserving the v1 call shape.""" + positions = _positions(view) + degrees: dict[str, int] = {node.id: 0 for node in view.nodes} + for edge in view.edges: + if edge.source in degrees and edge.target in degrees: + degrees[edge.source] += 1 + degrees[edge.target] += 1 + + palette = _palette() + nodes: list[dict[str, object]] = [] + present_statuses: set[str] = set() + for node in view.nodes: + inventory_checked = node.catalog == "module" and any( + key == INVENTORY_CHECKED_STATUS and count for key, count in node.status_counts + ) + status_key = ( + INVENTORY_CHECKED_STATUS + if inventory_checked + else node.status_key or (node.status_counts[0][0] if node.status_counts else "planned") + ) + if status_key not in palette: + status_key = "planned" + present_statuses.add(status_key) + layout = positions[node.id] + nodes.append( + { + "area": node.area, + "catalog": node.catalog, + "column": layout["column"], # v1 readers can still place nodes. + "declaration": node.declaration, + "focus": node.focus, + "id": node.id, + "internal_dependency_count": node.internal_dependency_count, + "isolated": degrees[node.id] == 0, + "kind": node.kind, + "layout": layout, + "lean": node.lean, + "member_count": len(node.members), + "rank": layout["rank"], + "row": layout["row"], + "status": status_key, + "status_counts": {key: count for key, count in node.status_counts}, + "summary": node.summary, + "title": node.title, + "url": links.get(node.id), + } + ) + + edges = [ + {"proof": edge.proof_count, "source": edge.source, "statement": edge.statement_count, "target": edge.target} + for edge in view.edges + ] + dependency_count = sum(edge.dependency_count for edge in view.edges) + isolated_count = sum(bool(node["isolated"]) for node in nodes) + ordered_statuses = [state.key for state in STATES if state.key in present_statuses] + if INVENTORY_CHECKED_STATUS in present_statuses: + ordered_statuses.append(INVENTORY_CHECKED_STATUS) + payload = { + "counts": { + "connected": len(nodes) - isolated_count, + "dependencies": dependency_count, + "isolated": isolated_count, + "nodes": len(nodes), + }, + "edge_count": dependency_count, + "edges": edges, + "node_count": len(nodes), + "nodes": nodes, + "palette": palette, + "present_statuses": ordered_statuses, + "regions": _atlas_regions(view, positions) if _uses_atlas(view) else [], + "schema": SCHEMA, + "title": view.title, + "view": { + "breadcrumbs": [ + {"label": label, "url": url} + for label, url in breadcrumbs + ], + "focus": view.focus, + "kind": view.kind, + "presentation": "atlas" if _uses_atlas(view) else "dag", + "radius": view.radius, + "scope": view.scope, + "summary": view.summary, + }, + } + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text( + json.dumps(payload, ensure_ascii=False, sort_keys=True, separators=(",", ":")) + "\n", + encoding="utf-8", + newline="\n", + ) + return path + + +def write_search_index( + path: Path, + view: GraphView, + *, + context_links: Mapping[str, str], +) -> Path: + """Write the small global index used to jump into a hierarchical view.""" + palette = _palette() + nodes: list[dict[str, object]] = [] + for node in view.nodes: + inventory_checked = node.catalog == "module" and any( + key == INVENTORY_CHECKED_STATUS and count for key, count in node.status_counts + ) + status_key = ( + INVENTORY_CHECKED_STATUS + if inventory_checked + else node.status_key or (node.status_counts[0][0] if node.status_counts else "planned") + ) + if status_key not in palette: + status_key = "planned" + nodes.append( + { + "id": node.id, + "kind": node.kind, + "status": status_key, + "title": node.title, + "url": context_links.get(node.id), + } + ) + payload = {"node_count": len(nodes), "nodes": nodes, "schema": SEARCH_SCHEMA} + path.parent.mkdir(parents=True, exist_ok=True) + path.write_text( + json.dumps(payload, ensure_ascii=False, sort_keys=True, separators=(",", ":")) + "\n", + encoding="utf-8", + newline="\n", + ) + return path + + +def render_container( + data_href: str, + *, + script_href: str | None = None, + fallback_links: Iterable[tuple[str, str]] = (), + fallback_total: int | None = None, + layout: str = "app", + search_href: str | None = None, +) -> str: + """Return a self-contained, progressively enhanced explorer host.""" + if layout not in {"app", "embedded"}: + raise ValueError(f"unsupported dependency explorer layout: {layout}") + href = html.escape(quote(data_href, safe="/%"), quote=True) + search = html.escape(quote(search_href, safe="/%"), quote=True) if search_href else "" + search_attr = f' data-catalog-src="{search}"' if search else "" + script = ( + f'\n' + if script_href + else "" + ) + fallback = tuple( + (label, target) + for label, target in fallback_links + if target and _safe_fallback_href(target) + ) + total = max(len(fallback), fallback_total or 0) + items = "\n".join( + "
  • " + f'{html.escape(label)}' + "
  • " + for label, target in fallback + ) + inventory = ( + '
    \n' + "

    Dependency explorer fallback. " + "JavaScript is unavailable or the graph data could not be loaded.

    \n" + + (f' \n' if items else "") + + ( + f"

    Showing {len(fallback)} of {total} linked nodes. " + if total > len(fallback) + else "

    " + ) + + f'Download the complete graph data.

    \n' + "
    \n" + ) + return ( + "\n" + f'
    \n' + '

    Loading dependency explorer…

    \n' + f"{inventory}" + f"
    {script}" + ) + + +def _safe_fallback_href(value: str) -> bool: + """Allow only generated relative links in the non-JavaScript fallback.""" + if any(ord(character) < 32 for character in value) or value.startswith("//"): + return False + parsed = urlsplit(value) + return not parsed.scheme and not parsed.netloc + + +def viewer_script() -> str: + """Return the dependency-free browser runtime with leading space folded.""" + # Keep the embedded source readable in Python without shipping indentation + # that browsers do not need. Internal spaces and line breaks stay intact. + lines = (line.lstrip() for line in _SCRIPT.splitlines()) + return "\n".join(lines) + "\n" + + +_STYLE = r""" +.bp-dag-viewer { + --dag-border: var(--bp-rule, #d8dade); --dag-bg: var(--bp-surface, #fff); + --dag-panel: color-mix(in srgb, var(--dag-bg) 94%, #64748b 6%); + --dag-fg: var(--bp-fg, #1c1e21); --dag-muted: var(--bp-muted, #65676b); --dag-link: var(--bp-link, #0064e0); + position: relative; display: grid; grid-template-rows: auto minmax(0, 1fr); width: 100%; + height: clamp(38rem, calc(100svh - 7rem), 64rem); min-height: 38rem; overflow: hidden; + border: 1px solid var(--dag-border); border-radius: 14px; background: var(--dag-bg); color: var(--dag-fg); + box-shadow: 0 12px 36px rgba(15, 23, 42, .08); isolation: isolate; + font-family: var(--md-text-font-family, ui-sans-serif, system-ui, sans-serif); +} +.bp-dag-viewer[data-layout=app] { + position: fixed; z-index: 40; inset: 0; width: 100dvw; max-width: none; + height: 100dvh !important; min-height: 0; margin: 0; border: 0; border-radius: 0; box-shadow: none; +} +body.bp-dag-app-page { overflow: hidden; } +body.bp-dag-app-page .md-header, body.bp-dag-app-page .md-tabs, +body.bp-dag-app-page .md-sidebar, body.bp-dag-app-page .md-footer { display: none; } +body.bp-dag-app-page .md-main__inner { width: 100%; max-width: none; margin: 0; } +body.bp-dag-app-page .md-content { max-width: none; } +body.bp-dag-app-page .md-content__inner { margin: 0; padding: 0; } +body.bp-dag-app-page .md-content__inner::before, +body.bp-dag-app-page .md-content__inner > h1, +body.bp-dag-app-page .md-content__inner > p { display: none; } +.bp-dag-viewer *, .bp-dag-viewer *::before, .bp-dag-viewer *::after { box-sizing: border-box; } +.bp-dag-head { z-index: 8; border-bottom: 1px solid var(--dag-border); background: var(--dag-bg); } +.bp-dag-context { display: flex; align-items: center; gap: .7rem; min-height: 2.65rem; padding: .45rem .75rem .2rem; } +.bp-dag-breadcrumb { min-width: 0; flex: 1; color: var(--dag-muted); font-size: .72rem; } +.bp-dag-breadcrumb ol { display: flex; align-items: center; gap: .35rem; margin: 0; padding: 0; list-style: none; } +.bp-dag-breadcrumb li { min-width: 0; overflow: hidden; text-overflow: ellipsis; white-space: nowrap; } +.bp-dag-breadcrumb li + li::before { content: "/"; margin-right: .35rem; color: var(--dag-border); } +.bp-dag-breadcrumb [aria-current=page] { color: var(--dag-fg); font-weight: 650; } +.bp-dag-view-kind { flex: none; padding: .18rem .45rem; border: 1px solid var(--dag-border); border-radius: 999px; color: var(--dag-muted); font-size: .64rem; font-weight: 700; letter-spacing: .05em; text-transform: uppercase; } +.bp-dag-toolbar { display: flex; align-items: center; gap: .42rem; min-height: 3.35rem; padding: .35rem .65rem .6rem; font-size: .76rem; } +.bp-dag-search-wrap { position: relative; flex: 1 1 17rem; min-width: 10rem; max-width: 31rem; } +.bp-dag-search { width: 100%; min-height: 2.35rem; margin: 0; padding: .48rem .7rem .48rem 2rem; border: 1px solid var(--dag-border); border-radius: 9px; outline: 0; background: var(--dag-panel); color: var(--dag-fg); font: inherit; } +.bp-dag-search-wrap::before { content: "⌕"; position: absolute; z-index: 2; left: .7rem; top: .36rem; color: var(--dag-muted); font-size: 1rem; pointer-events: none; } +.bp-dag-search:focus { border-color: var(--dag-link); box-shadow: 0 0 0 3px color-mix(in srgb, var(--dag-link) 18%, transparent); } +.bp-dag-search-results { position: absolute; z-index: 20; top: calc(100% + .35rem); left: 0; right: 0; max-height: min(27rem, 60vh); overflow: auto; padding: .35rem; border: 1px solid var(--dag-border); border-radius: 10px; background: var(--dag-bg); box-shadow: 0 16px 38px rgba(15, 23, 42, .2); } +.bp-dag-search-results[hidden] { display: none; } +.bp-dag-results, .bp-dag-relation-list, .bp-dag-inventory-list { margin: 0; padding: 0; list-style: none; } +.bp-dag-result { display: grid; grid-template-columns: minmax(0, 1fr) auto; width: 100%; gap: .15rem .6rem; padding: .52rem .55rem; border: 0; border-radius: 7px; background: transparent; color: var(--dag-fg); text-align: left; cursor: pointer; } +.bp-dag-result:hover, .bp-dag-result:focus-visible { background: color-mix(in srgb, var(--dag-link) 9%, transparent); } +.bp-dag-result:focus-visible, .bp-dag-inventory-row:focus-visible { outline: 3px solid color-mix(in srgb, var(--dag-link) 52%, transparent); outline-offset: -3px; } +.bp-dag-result-title { overflow: hidden; font-weight: 650; text-overflow: ellipsis; white-space: nowrap; } +.bp-dag-result-id, .bp-dag-result-reason { color: var(--dag-muted); font-size: .66rem; } +.bp-dag-result-id { grid-column: 1; overflow: hidden; text-overflow: ellipsis; white-space: nowrap; font-family: ui-monospace, SFMono-Regular, Consolas, monospace; } +.bp-dag-result-reason { grid-column: 2; grid-row: 1 / span 2; align-self: center; } +.bp-dag-button, .bp-dag-filter-summary, .bp-dag-mode-button, .bp-dag-pivot, .bp-dag-hidden-button, .bp-dag-load-more { min-height: 2.25rem; padding: .38rem .58rem; border: 1px solid var(--dag-border); border-radius: 8px; background: var(--dag-bg); color: var(--dag-fg); font: inherit; font-weight: 650; cursor: pointer; } +.bp-dag-button:hover, .bp-dag-filter-summary:hover, .bp-dag-mode-button:hover, .bp-dag-pivot:hover, .bp-dag-load-more:hover { border-color: var(--dag-link); color: var(--dag-link); } +.bp-dag-button:focus-visible, .bp-dag-filter-summary:focus-visible, .bp-dag-mode-button:focus-visible, .bp-dag-pivot:focus-visible, .bp-dag-node:focus-visible, .bp-dag-sheet-handle:focus-visible { outline: 3px solid color-mix(in srgb, var(--dag-link) 45%, transparent); outline-offset: 2px; } +.bp-dag-zoom, .bp-dag-modes { display: inline-flex; flex: none; } +.bp-dag-zoom .bp-dag-button, .bp-dag-modes .bp-dag-mode-button { border-radius: 0; margin-left: -1px; } +.bp-dag-zoom :first-child, .bp-dag-modes :first-child { margin-left: 0; border-radius: 8px 0 0 8px; } +.bp-dag-zoom :last-child, .bp-dag-modes :last-child { border-radius: 0 8px 8px 0; } +.bp-dag-mode-button[aria-pressed=true], .bp-dag-pivot[aria-pressed=true] { border-color: var(--dag-link); background: color-mix(in srgb, var(--dag-link) 10%, var(--dag-bg)); color: var(--dag-link); } +.bp-dag-filters { position: relative; flex: none; } +.bp-dag-filter-summary { display: flex; align-items: center; list-style: none; white-space: nowrap; } +.bp-dag-filter-summary::-webkit-details-marker { display: none; } +.bp-dag-filter-popover { position: absolute; z-index: 18; top: calc(100% + .35rem); right: 0; width: 15rem; max-height: 23rem; overflow: auto; padding: .65rem; border: 1px solid var(--dag-border); border-radius: 10px; background: var(--dag-bg); box-shadow: 0 14px 32px rgba(15, 23, 42, .18); } +.bp-dag-filter-popover fieldset { display: grid; gap: .2rem; margin: 0; padding: 0; border: 0; } +.bp-dag-filter-popover legend { margin-bottom: .35rem; color: var(--dag-muted); font-size: .68rem; font-weight: 700; letter-spacing: .04em; text-transform: uppercase; } +.bp-dag-check { display: flex; align-items: center; gap: .45rem; min-height: 2rem; padding: .2rem .3rem; border-radius: 6px; } +.bp-dag-check:hover { background: var(--dag-panel); } +.bp-dag-check input { accent-color: var(--dag-link); } +.bp-dag-check-count { margin-left: auto; color: var(--dag-muted); font-variant-numeric: tabular-nums; } +.bp-dag-isolated { display: inline-flex; align-items: center; gap: .3rem; flex: none; white-space: nowrap; color: var(--dag-muted); } +.bp-dag-stats { display: inline-flex; align-items: center; justify-content: flex-end; min-width: 9.5rem; margin-left: auto; color: var(--dag-muted); white-space: nowrap; font-variant-numeric: tabular-nums; } +.bp-dag-hidden-button { min-height: 1.6rem; margin: 0; padding: .08rem .2rem; border: 0; background: transparent; color: var(--dag-link); } +.bp-dag-body { position: relative; display: grid; grid-template-columns: minmax(0, 1fr) 0; min-height: 0; } +.bp-dag-viewer.bp-dag-has-selection .bp-dag-body { grid-template-columns: minmax(0, 1fr) 22rem; } +.bp-dag-viewer.bp-dag-atlas .bp-dag-body { grid-template-columns: minmax(0, 62fr) minmax(22rem, 38fr); } +.bp-dag-main { position: relative; min-width: 0; min-height: 0; overflow: hidden; background: var(--dag-bg); } +.bp-dag-stage { position: absolute; inset: 0; overflow: hidden; touch-action: pan-y; cursor: grab; overscroll-behavior-x: contain; } +.bp-dag-viewer[data-layout=app] .bp-dag-stage { touch-action: none; } +.bp-dag-stage[data-dragging=true] { cursor: grabbing; } +.bp-dag-canvas, .bp-dag-node-layer { position: absolute; inset: 0; width: 100%; height: 100%; } +.bp-dag-canvas { display: block; } +.bp-dag-node-layer { overflow: hidden; pointer-events: none; } +.bp-dag-node { position: absolute; top: 0; left: 0; display: grid; align-content: center; width: 196px; height: 56px; padding: 6px 10px; overflow: hidden; border: 1.5px solid var(--dag-node-stroke); border-radius: 8px; background: var(--dag-node-fill); color: var(--dag-node-text); box-shadow: 0 2px 5px rgba(15, 23, 42, .08); text-align: left; transform-origin: 0 0; pointer-events: auto; cursor: pointer; will-change: transform; } +.bp-dag-node-title { overflow: hidden; font-size: 14px; font-weight: 680; line-height: 1.18; text-overflow: ellipsis; white-space: nowrap; } +.bp-dag-node-meta { overflow: hidden; opacity: .75; font-size: 10px; line-height: 1.2; text-overflow: ellipsis; white-space: nowrap; } +.bp-dag-node[data-selected=true] { border-width: 3px; box-shadow: 0 0 0 3px color-mix(in srgb, var(--dag-link) 24%, transparent), 0 5px 13px rgba(15, 23, 42, .18); } +.bp-dag-node[data-subdued=true] { opacity: .23; } +.bp-dag-node[data-kind=scope] { border-radius: 13px; } +.bp-dag-node[data-kind=boundary] { border-style: dashed; } +.bp-dag-viewer.bp-dag-atlas .bp-dag-node[data-kind=scope] { display: block; padding: 6px; border: 0; border-radius: 50%; background: var(--dag-status-ring, var(--dag-node-stroke)); text-align: center; } +.bp-dag-node-core { display: grid; place-content: center; width: 100%; height: 100%; padding: .8rem; border-radius: 50%; background: var(--dag-node-fill); color: var(--dag-node-text); } +.bp-dag-viewer.bp-dag-atlas .bp-dag-node[data-kind=scope] .bp-dag-node-title { display: -webkit-box; overflow: hidden; white-space: normal; -webkit-box-orient: vertical; -webkit-line-clamp: 3; } +.bp-dag-viewer.bp-dag-atlas .bp-dag-node[data-kind=scope] .bp-dag-node-meta { margin-top: .35rem; white-space: normal; } +.bp-dag-viewer.bp-dag-atlas .bp-dag-node-title { font-size: 18px; } +.bp-dag-viewer.bp-dag-atlas .bp-dag-node-meta { font-size: 11px; } +.bp-dag-density, .bp-dag-empty { position: absolute; z-index: 4; left: 50%; border: 1px solid var(--dag-border); border-radius: 999px; background: color-mix(in srgb, var(--dag-bg) 92%, transparent); color: var(--dag-muted); box-shadow: 0 3px 12px rgba(15, 23, 42, .08); pointer-events: none; } +.bp-dag-density { bottom: .7rem; padding: .25rem .55rem; transform: translateX(-50%); font-size: .66rem; } +.bp-dag-empty { top: 50%; padding: .55rem .8rem; transform: translate(-50%, -50%); font-size: .74rem; } +.bp-dag-density[hidden], .bp-dag-empty[hidden] { display: none; } +.bp-dag-inventory { position: absolute; inset: 0; display: grid; grid-template-rows: auto minmax(0, 1fr) auto; overflow: hidden; background: var(--dag-bg); } +.bp-dag-inventory[hidden] { display: none; } +.bp-dag-inventory-head { display: flex; align-items: baseline; justify-content: space-between; gap: 1rem; padding: .75rem 1rem; border-bottom: 1px solid var(--dag-border); } +.bp-dag-inventory-head h2 { margin: 0; font-size: .95rem; } +.bp-dag-inventory-summary { color: var(--dag-muted); font-size: .7rem; } +.bp-dag-inventory-scroll { overflow: auto; padding: .45rem; } +.bp-dag-inventory-row { display: grid; grid-template-columns: minmax(0, 1fr) auto; width: 100%; gap: .15rem .8rem; padding: .62rem .7rem; border: 0; border-bottom: 1px solid var(--dag-border); background: transparent; color: var(--dag-fg); text-align: left; cursor: pointer; } +.bp-dag-inventory-row:hover, .bp-dag-inventory-row:focus-visible { background: var(--dag-panel); } +.bp-dag-inventory-title { font-weight: 650; } +.bp-dag-inventory-id { grid-row: 2; overflow: hidden; color: var(--dag-muted); font: .68rem ui-monospace, SFMono-Regular, Consolas, monospace; text-overflow: ellipsis; white-space: nowrap; } +.bp-dag-inventory-meta { grid-column: 2; grid-row: 1 / span 2; align-self: center; color: var(--dag-muted); font-size: .68rem; } +.bp-dag-load-more { justify-self: center; margin: .55rem; } +.bp-dag-load-more[hidden] { display: none; } +.bp-dag-inspector { z-index: 7; width: 0; min-width: 0; overflow: hidden; border-left: 0; background: var(--dag-panel); visibility: hidden; } +.bp-dag-viewer.bp-dag-has-selection .bp-dag-inspector { width: auto; overflow: auto; border-left: 1px solid var(--dag-border); visibility: visible; } +.bp-dag-viewer.bp-dag-atlas .bp-dag-inspector { width: auto; overflow: auto; border-left: 1px solid var(--dag-border); visibility: visible; } +.bp-dag-inspector-inner { padding: .9rem; } +.bp-dag-sheet-handle { display: none; } +.bp-dag-inspector-header { display: flex; align-items: flex-start; gap: .5rem; } +.bp-dag-inspector-header h2 { flex: 1; margin: 0; font-size: 1rem; line-height: 1.25; } +.bp-dag-close { min-width: 2rem; min-height: 2rem; padding: .2rem; border: 0; background: transparent; color: var(--dag-muted); cursor: pointer; } +.bp-dag-kicker { margin: 0 0 .35rem; color: var(--dag-muted); font-size: .64rem; font-weight: 750; letter-spacing: .06em; text-transform: uppercase; } +.bp-dag-node-id { display: block; margin: .45rem 0; overflow-wrap: anywhere; color: var(--dag-muted); font: .66rem ui-monospace, SFMono-Regular, Consolas, monospace; } +.bp-dag-status-pill { display: inline-flex; align-items: center; gap: .35rem; margin: .3rem 0 .65rem; color: var(--dag-muted); font-size: .7rem; } +.bp-dag-status-pill::before { content: ""; width: .58rem; height: .58rem; border: 2px solid var(--dag-pill-stroke); border-radius: 50%; background: var(--dag-pill-fill); } +.bp-dag-open { display: inline-flex; align-items: center; justify-content: center; min-height: 2.2rem; padding: .4rem .65rem; border-radius: 8px; background: var(--dag-link); color: #fff !important; font-size: .74rem; font-weight: 700; text-decoration: none !important; } +.bp-dag-overview { color: var(--dag-muted); font-size: .76rem; line-height: 1.55; } +.bp-dag-overview strong { color: var(--dag-fg); } +.bp-dag-summary { margin: .8rem 0; color: var(--dag-fg); font-family: Georgia, "Iowan Old Style", serif; font-size: .88rem; line-height: 1.55; } +.bp-dag-lean { margin: .6rem 0 0; overflow-wrap: anywhere; color: var(--dag-muted); font: .68rem ui-monospace, SFMono-Regular, Consolas, monospace; } +.bp-dag-section { margin-top: 1rem; padding-top: .8rem; border-top: 1px solid var(--dag-border); } +.bp-dag-section h3 { margin: 0 0 .45rem; font-size: .76rem; } +.bp-dag-pivots { display: grid; grid-template-columns: repeat(3, 1fr); gap: .3rem; } +.bp-dag-pivot { min-height: 2.7rem; padding: .3rem; font-size: .66rem; } +.bp-dag-relation-button { width: 100%; padding: .35rem .25rem; overflow: hidden; border: 0; background: transparent; color: var(--dag-link); font: inherit; font-size: .72rem; text-align: left; text-overflow: ellipsis; white-space: nowrap; cursor: pointer; } +.bp-dag-relation-button:hover { text-decoration: underline; } +.bp-dag-distribution { display: grid; gap: .3rem; margin: .4rem 0 0; } +.bp-dag-distribution-row { display: grid; grid-template-columns: minmax(0, 1fr) auto; gap: .4rem; color: var(--dag-muted); font-size: .68rem; } +.bp-dag-loading, .bp-dag-error { margin: 0; padding: 1rem; } +.bp-dag-error { color: #b42318; } +.bp-dag-fallback { min-height: 0; overflow: auto; padding: 0 1rem 1rem; color: var(--dag-muted); } +.bp-dag-fallback p { max-width: 48rem; } +.bp-dag-fallback-list { display: grid; gap: .3rem; margin: .8rem 0; padding-left: 1.4rem; } +.bp-dag-viewer.bp-dag-enhancing .bp-dag-fallback { display: none; } +.bp-dag-sr-only { position: absolute !important; width: 1px !important; height: 1px !important; padding: 0 !important; overflow: hidden !important; clip: rect(0, 0, 0, 0) !important; white-space: nowrap !important; border: 0 !important; } +@media (max-width: 900px) { + .bp-dag-viewer:not([data-layout=app]) { height: max(40rem, calc(100svh - 4.5rem)); } + .bp-dag-viewer.bp-dag-has-selection .bp-dag-body { grid-template-columns: minmax(0, 1fr) 17rem; } + .bp-dag-viewer.bp-dag-atlas .bp-dag-body { grid-template-columns: minmax(0, 1fr) 19rem; } + .bp-dag-toolbar { flex-wrap: wrap; } + .bp-dag-search-wrap { max-width: none; } + .bp-dag-stats { order: 8; width: 100%; min-height: 1.4rem; margin: 0; justify-content: flex-start; } +} +@media (max-width: 680px) { + .bp-dag-viewer:not([data-layout=app]) { height: calc(100svh - 1rem); min-height: 34rem; border-radius: 10px; } + .bp-dag-viewer[data-layout=app] { min-height: 28rem; } + .bp-dag-context { padding-inline: .55rem; } + .bp-dag-toolbar { gap: .35rem; padding: .35rem .5rem .5rem; } + .bp-dag-search-wrap { flex-basis: calc(100% - .4rem); order: -2; } + .bp-dag-search, .bp-dag-button, .bp-dag-filter-summary, .bp-dag-mode-button { min-height: 2.75rem; } + .bp-dag-isolated { min-height: 2.75rem; } + .bp-dag-body { display: block; } + .bp-dag-main { position: absolute; inset: 0; } + .bp-dag-inventory { padding-bottom: 3.65rem; } + .bp-dag-inspector { position: absolute; z-index: 12; right: .45rem; bottom: .45rem; left: .45rem; width: auto; max-height: min(58%, 30rem); overflow: auto; border: 1px solid var(--dag-border); border-radius: 13px; box-shadow: 0 -8px 30px rgba(15, 23, 42, .2); visibility: visible; transform: translateY(calc(100% - 3.2rem)); transition: transform .2s ease; } + .bp-dag-viewer.bp-dag-sheet-open .bp-dag-inspector { transform: translateY(0); } + .bp-dag-sheet-handle { display: block; position: sticky; z-index: 2; top: 0; width: 100%; min-height: 3.1rem; padding: .6rem 2.2rem .45rem .7rem; overflow: hidden; border: 0; border-bottom: 1px solid var(--dag-border); background: var(--dag-panel); color: var(--dag-fg); font: inherit; font-size: .75rem; font-weight: 700; text-align: left; text-overflow: ellipsis; white-space: nowrap; cursor: pointer; } + .bp-dag-sheet-handle::before { content: ""; position: absolute; top: .35rem; left: 50%; width: 2rem; height: 3px; border-radius: 2px; background: var(--dag-border); transform: translateX(-50%); } + .bp-dag-inspector-inner { padding: .75rem; } + .bp-dag-density { bottom: 3.7rem; } +} +@media (prefers-reduced-motion: reduce) { + .bp-dag-inspector { transition: none; } + .bp-dag-node { will-change: auto; } +} +""".strip() + + +_SCRIPT = r"""/* Generated by autoform render. Edits are overwritten. */ +(function () { + "use strict"; + if (window.__AUTOFORM_DAG_VIEWER_V2__) return; + window.__AUTOFORM_DAG_VIEWER_V2__ = true; + + var NODE_W = 196, NODE_H = 56, MAX_DOM_NODES = 180, MAX_MAP_NODES = 120, LIST_PAGE = 100; + var SEARCH_PAGE = 50, RELATION_PAGE = 50, MIN_SCALE = .002, MIN_READABLE_SCALE = .8, MIN_ATLAS_SCALE = .55, hostSequence = 0; + var clamp = function (value, low, high) { return Math.max(low, Math.min(high, value)); }; + + function element(tag, className, text) { + var node = document.createElement(tag); + if (className) node.className = className; + if (text !== undefined) node.textContent = text; + return node; + } + + function button(className, text, label) { + var node = element("button", className, text); + node.type = "button"; + if (label) node.setAttribute("aria-label", label); + return node; + } + + function safeHref(value) { + if (!value || /[\u0000-\u001f]/.test(value)) return null; + try { + var url = new URL(value, window.location.href); + return /^(https?:)$/.test(url.protocol) && url.origin === window.location.origin ? value : null; + } catch (_error) { return null; } + } + + function sizeAppHost(host) { + if (host.getAttribute("data-layout") !== "app") return; + var top = Math.max(0, host.getBoundingClientRect().top); + host.style.height = Math.max(420, window.innerHeight - top) + "px"; + } + + function start(host) { + if (host.getAttribute("data-dag-ready") === "true") return; + host.setAttribute("data-dag-ready", "true"); + host.classList.add("bp-dag-enhancing"); + if (host.getAttribute("data-layout") === "app") { + document.body.classList.add("bp-dag-app-page"); sizeAppHost(host); + requestAnimationFrame(function () { sizeAppHost(host); }); + window.addEventListener("resize", function () { sizeAppHost(host); }); + } + var instance = ++hostSequence; + fetch(host.getAttribute("data-graph-src"), {credentials: "same-origin"}).then(function (response) { + if (!response.ok) throw new Error("HTTP " + response.status); + return response.json(); + }).then(function (data) { mount(host, data, instance); }).catch(function (error) { + host.classList.remove("bp-dag-enhancing"); + var loading = host.querySelector(".bp-dag-loading"); + if (loading) { + loading.textContent = "The interactive graph could not be loaded: " + error.message; + loading.classList.add("bp-dag-error"); + } + }); + } + + function mount(host, data, instance) { + if (!data || data.schema !== "autoform-dag-view/v2" || !data.palette || + !Array.isArray(data.nodes) || !Array.isArray(data.edges)) throw new Error("unsupported graph payload"); + host.textContent = ""; + host.classList.remove("bp-dag-enhancing"); + var view = data.view || {kind: "full", scope: null}; + var atlas = view.presentation === "atlas"; host.classList.toggle("bp-dag-atlas", atlas); + var palette = data.palette || {}; + var byId = new Map(), prerequisites = new Map(), dependents = new Map(), incident = new Map(); + var statusCounts = new Map(), presentStatuses = []; + data.nodes.forEach(function (node, index) { + var layout = node.layout || {}; + node._index = index; + node.x = Number.isFinite(layout.x) ? layout.x : (node.column || 0) * 312; + node.y = Number.isFinite(layout.y) ? layout.y : (node.row || 0) * 66; + node.width = Number.isFinite(layout.width) ? layout.width : NODE_W; + node.height = Number.isFinite(layout.height) ? layout.height : NODE_H; + node.isolated = node.isolated === true; + byId.set(node.id, node); + prerequisites.set(node.id, []); dependents.set(node.id, []); incident.set(node.id, []); + statusCounts.set(node.status, (statusCounts.get(node.status) || 0) + 1); + }); + data.edges.forEach(function (edge, index) { + if (prerequisites.has(edge.target) && byId.has(edge.source)) prerequisites.get(edge.target).push(edge.source); + if (dependents.has(edge.source) && byId.has(edge.target)) dependents.get(edge.source).push(edge.target); + if (incident.has(edge.source)) incident.get(edge.source).push(index); + if (incident.has(edge.target)) incident.get(edge.target).push(index); + }); + var isolateIndex = 0; + data.nodes.forEach(function (node) { + node.isolated = node.isolated || ((prerequisites.get(node.id) || []).length + (dependents.get(node.id) || []).length === 0); + node._isolateIndex = node.isolated ? isolateIndex++ : -1; + }); + var mobileIsolateBase = (data.nodes.reduce(function (largest, node) { + return node.isolated ? largest : Math.max(largest, Number.isFinite(node.column) ? node.column : 0); + }, -2) + 2) * (NODE_H + 72); + (data.present_statuses || Object.keys(palette)).forEach(function (key) { + if (statusCounts.has(key) && presentStatuses.indexOf(key) < 0) presentStatuses.push(key); + }); + statusCounts.forEach(function (_count, key) { + if (presentStatuses.indexOf(key) < 0) presentStatuses.push(key); + }); + + var mapAllowed = data.nodes.length <= MAX_MAP_NODES; + var state = { + active: [], activeDirty: true, activeIds: new Set(), direction: "both", listLimit: LIST_PAGE, mode: "graph", moved: false, + orientation: "lr", pointers: new Map(), pinch: null, query: "", searchLimit: 12, selected: null, + searchCache: [], searchCacheQuery: null, searchError: null, searchLoading: false, + searchNodes: data.nodes, searchPromise: null, spotlight: null, + mapAllowed: mapAllowed, readableCrop: false, + selectedStatuses: new Set(presentStatuses), showIsolated: view.kind !== "full", + transform: {x: 20, y: 20, scale: 1} + }; + if (!mapAllowed) state.mode = "list"; + var refs = {}, overlays = new Map(), scheduled = false, firstResize = true; + + buildShell(); + bindEvents(); + applyLocation(true); + renderInspector(); + renderInventory(true); + resize(); + redirectLegacyFocus(); + + function buildShell() { + var head = element("header", "bp-dag-head"); + var context = element("div", "bp-dag-context"); + var crumbs = element("nav", "bp-dag-breadcrumb"); + crumbs.setAttribute("aria-label", "Explorer context"); + var crumbList = element("ol"); + var trail = Array.isArray(view.breadcrumbs) && view.breadcrumbs.length ? view.breadcrumbs : [ + {label: "All mathematics", url: null} + ]; + trail.forEach(function (entry, index) { + var item = element("li"), href = safeHref(entry.url); + if (href) { var link = element("a", "", entry.label); link.href = href; item.appendChild(link); } + else { item.textContent = entry.label; if (index === trail.length - 1) item.setAttribute("aria-current", "page"); } + crumbList.appendChild(item); + }); + crumbs.appendChild(crumbList); context.appendChild(crumbs); + context.appendChild(element("span", "bp-dag-view-kind", atlas ? "knowledge atlas" : view.kind || "graph")); head.appendChild(context); + + var toolbar = element("div", "bp-dag-toolbar"); + toolbar.setAttribute("role", "toolbar"); toolbar.setAttribute("aria-label", "Dependency explorer controls"); + var searchWrap = element("div", "bp-dag-search-wrap"); + refs.search = element("input", "bp-dag-search"); + refs.search.type = "search"; refs.search.placeholder = "Search the whole roadmap ( / )"; + refs.search.setAttribute("aria-label", "Search all graph nodes"); + refs.search.setAttribute("aria-expanded", "false"); + refs.search.setAttribute("aria-controls", "bp-dag-search-results-" + instance); + refs.searchResults = element("div", "bp-dag-search-results"); refs.searchResults.id = "bp-dag-search-results-" + instance; + refs.searchResults.setAttribute("role", "region"); refs.searchResults.setAttribute("aria-label", "Search results"); + refs.searchResults.hidden = true; + searchWrap.appendChild(refs.search); searchWrap.appendChild(refs.searchResults); toolbar.appendChild(searchWrap); + + var filters = element("details", "bp-dag-filters"); + refs.filterSummary = element("summary", "bp-dag-filter-summary", "Status"); + var filterPopover = element("div", "bp-dag-filter-popover"), fieldset = element("fieldset"); + fieldset.appendChild(element("legend", "", "Statuses in this view")); refs.statusInputs = new Map(); + presentStatuses.forEach(function (key) { + var label = element("label", "bp-dag-check"), input = element("input"); + input.type = "checkbox"; input.checked = true; input.value = key; input.addEventListener("change", onStatusChange); + refs.statusInputs.set(key, input); label.appendChild(input); label.appendChild(document.createTextNode(statusLabel(key))); + label.appendChild(element("span", "bp-dag-check-count", String(statusCounts.get(key) || 0))); fieldset.appendChild(label); + }); + filterPopover.appendChild(fieldset); filters.appendChild(refs.filterSummary); filters.appendChild(filterPopover); + toolbar.appendChild(filters); + + refs.isolatedLabel = element("label", "bp-dag-isolated"); refs.isolated = element("input"); + refs.isolated.type = "checkbox"; refs.isolated.checked = state.showIsolated; refs.isolatedLabel.appendChild(refs.isolated); + refs.isolatedLabel.appendChild(document.createTextNode("Show items without edges")); + refs.isolatedLabel.hidden = !data.nodes.some(function (node) { return node.isolated; }) || + data.nodes.every(function (node) { return node.isolated; }); toolbar.appendChild(refs.isolatedLabel); + + var modes = element("div", "bp-dag-modes"); modes.setAttribute("role", "group"); modes.setAttribute("aria-label", "Explorer view"); + refs.graphMode = button("bp-dag-mode-button", mapAllowed ? (atlas ? "Atlas" : "Relations") : "Map · too many items"); + refs.graphMode.disabled = !mapAllowed; refs.listMode = button("bp-dag-mode-button", "Browse"); + modes.appendChild(refs.graphMode); modes.appendChild(refs.listMode); toolbar.appendChild(modes); + + var zoomGroup = element("div", "bp-dag-zoom"); zoomGroup.setAttribute("role", "group"); zoomGroup.setAttribute("aria-label", "Zoom controls"); + refs.zoomOut = button("bp-dag-button", "−", "Zoom out"); refs.zoomIn = button("bp-dag-button", "+", "Zoom in"); + refs.fit = button("bp-dag-button", "Fit", "Fit shown nodes"); + zoomGroup.appendChild(refs.zoomOut); zoomGroup.appendChild(refs.zoomIn); zoomGroup.appendChild(refs.fit); toolbar.appendChild(zoomGroup); + + refs.stats = element("span", "bp-dag-stats"); refs.statsText = element("span"); refs.hiddenButton = button("bp-dag-hidden-button", ""); + refs.stats.appendChild(refs.statsText); refs.stats.appendChild(refs.hiddenButton); toolbar.appendChild(refs.stats); + head.appendChild(toolbar); host.appendChild(head); + + var body = element("div", "bp-dag-body"), main = element("div", "bp-dag-main"); + refs.stage = element("section", "bp-dag-stage"); refs.stage.setAttribute("role", "region"); + refs.stage.setAttribute("aria-label", "Dependency graph. Drag with a mouse to pan, use Control or Command plus scroll to zoom, and use arrow keys between node buttons."); + refs.canvas = element("canvas", "bp-dag-canvas"); refs.canvas.setAttribute("aria-hidden", "true"); + refs.nodeLayer = element("div", "bp-dag-node-layer"); refs.density = element("div", "bp-dag-density"); refs.density.hidden = true; + refs.empty = element("div", "bp-dag-empty", "No nodes match these controls."); refs.empty.hidden = true; + refs.stage.appendChild(refs.canvas); refs.stage.appendChild(refs.nodeLayer); refs.stage.appendChild(refs.density); refs.stage.appendChild(refs.empty); + main.appendChild(refs.stage); + + refs.inventory = element("section", "bp-dag-inventory"); refs.inventory.hidden = true; + refs.inventory.setAttribute("aria-label", "Complete node inventory"); + var inventoryHead = element("div", "bp-dag-inventory-head"); inventoryHead.appendChild(element("h2", "", "Browse this scope")); + refs.inventorySummary = element("span", "bp-dag-inventory-summary"); inventoryHead.appendChild(refs.inventorySummary); + refs.inventoryScroll = element("div", "bp-dag-inventory-scroll"); refs.inventoryList = element("ul", "bp-dag-inventory-list"); + refs.inventoryScroll.appendChild(refs.inventoryList); refs.loadMore = button("bp-dag-load-more", "Show more nodes"); + refs.inventory.appendChild(inventoryHead); refs.inventory.appendChild(refs.inventoryScroll); refs.inventory.appendChild(refs.loadMore); + main.appendChild(refs.inventory); body.appendChild(main); + + refs.inspector = element("aside", "bp-dag-inspector"); refs.inspector.setAttribute("aria-label", "Node inspector"); + refs.sheetHandle = button("bp-dag-sheet-handle", "Graph details", "Toggle graph details"); + refs.sheetHandle.setAttribute("aria-expanded", "false"); + refs.inspectorInner = element("div", "bp-dag-inspector-inner"); + refs.inspectorInner.id = "bp-dag-inspector-content-" + instance; + refs.sheetHandle.setAttribute("aria-controls", refs.inspectorInner.id); + refs.inspector.appendChild(refs.sheetHandle); + refs.inspector.appendChild(refs.inspectorInner); body.appendChild(refs.inspector); host.appendChild(body); + refs.announcement = element("p", "bp-dag-sr-only"); refs.announcement.setAttribute("aria-live", "polite"); host.appendChild(refs.announcement); + refs.ctx = refs.canvas.getContext("2d"); + } + + function bindEvents() { + refs.search.addEventListener("focus", ensureGlobalSearch); + refs.search.addEventListener("input", function () { + state.query = refs.search.value.trim(); state.searchLimit = 12; state.listLimit = LIST_PAGE; + renderSearch(); renderInventory(true); if (state.query) ensureGlobalSearch(); + }); + refs.search.addEventListener("keydown", function (event) { + if (event.key === "Escape") { closeSearch(); return; } + if (event.key === "ArrowDown") { + var first = refs.searchResults.querySelector("button"); if (first) { event.preventDefault(); first.focus(); } + } else if (event.key === "Enter") { + var matches = searchMatches(); if (matches.length) { event.preventDefault(); activateNode(matches[0].node, true); } + } + }); + refs.isolated.addEventListener("change", function () { + state.showIsolated = refs.isolated.checked; state.activeDirty = true; + writeLocation("replace"); refresh(true); + }); + refs.graphMode.addEventListener("click", function () { setMode("graph", true); }); + refs.listMode.addEventListener("click", function () { setMode("list", true); }); + refs.zoomIn.addEventListener("click", function () { zoomAt(1.24, refs.stage.clientWidth / 2, refs.stage.clientHeight / 2); }); + refs.zoomOut.addEventListener("click", function () { zoomAt(.8, refs.stage.clientWidth / 2, refs.stage.clientHeight / 2); }); + refs.fit.addEventListener("click", fit); refs.hiddenButton.addEventListener("click", revealAll); + refs.loadMore.addEventListener("click", function () { state.listLimit += LIST_PAGE; renderInventory(false); }); + refs.sheetHandle.addEventListener("click", function () { + setSheet(!host.classList.contains("bp-dag-sheet-open")); + }); + refs.stage.addEventListener("pointerdown", pointerDown); refs.stage.addEventListener("pointermove", pointerMove); + refs.stage.addEventListener("pointerup", pointerUp); refs.stage.addEventListener("pointercancel", pointerUp); + refs.stage.addEventListener("wheel", function (event) { + if (!event.ctrlKey && !event.metaKey) return; + event.preventDefault(); var rect = refs.stage.getBoundingClientRect(); + zoomAt(event.deltaY < 0 ? 1.13 : .885, event.clientX - rect.left, event.clientY - rect.top); + }, {passive: false}); + refs.stage.addEventListener("keydown", function (event) { + if (event.key === "Escape" && state.selected) { clearSelection(true); event.preventDefault(); } + else if (event.key === "+" || event.key === "=") { zoomAt(1.2, refs.stage.clientWidth / 2, refs.stage.clientHeight / 2); event.preventDefault(); } + else if (event.key === "-") { zoomAt(.82, refs.stage.clientWidth / 2, refs.stage.clientHeight / 2); event.preventDefault(); } + else if (event.key === "0") { fit(); event.preventDefault(); } + }); + window.addEventListener("hashchange", function () { applyLocation(false); }); + window.addEventListener("popstate", function () { applyLocation(false); }); + document.addEventListener("keydown", function (event) { + var tag = event.target && event.target.tagName; + if ((event.key === "/" && !/^(INPUT|TEXTAREA|SELECT)$/.test(tag || "")) || + ((event.metaKey || event.ctrlKey) && event.key.toLowerCase() === "k")) { + event.preventDefault(); refs.search.focus(); refs.search.select(); + } + }); + if (window.ResizeObserver) new ResizeObserver(resize).observe(refs.stage); else window.addEventListener("resize", resize); + window.addEventListener("resize", syncSheetAccessibility); + new MutationObserver(schedule).observe(document.body, {attributes: true, attributeFilter: ["data-md-color-scheme"]}); + } + + function statusLabel(key) { return palette[key] && palette[key].label ? palette[key].label : key.replace(/_/g, " "); } + function isDark() { return document.body.getAttribute("data-md-color-scheme") === "slate"; } + function colors(node) { + var entry = palette[node.status] || palette.planned || {}; + return entry[isDark() ? "dark" : "light"] || {fill: "#fff", stroke: "#9ca3af", text: "#374151"}; + } + function statusRing(node) { + var counts = node.status_counts || {}, entries = Object.keys(counts).filter(function (key) { return counts[key] > 0; }); + var total = entries.reduce(function (sum, key) { return sum + counts[key]; }, 0), cursor = 0, stops = []; + entries.forEach(function (key) { + var entry = palette[key] || palette.planned || {}, color = entry[isDark() ? "dark" : "light"] || {}; + var end = cursor + counts[key] / Math.max(1, total) * 360; + stops.push((color.stroke || "#9ca3af") + " " + cursor + "deg " + end + "deg"); cursor = end; + }); + return stops.length ? "conic-gradient(" + stops.join(",") + ")" : "var(--dag-node-stroke)"; + } + function world(node) { + if (state.orientation === "tb" && !atlas) { + if (node.isolated) { + var mobileColumns = refs.stage.clientWidth < 540 ? 2 : 3; + return {x: (node._isolateIndex % mobileColumns) * (NODE_W + 20), + y: mobileIsolateBase + Math.floor(node._isolateIndex / mobileColumns) * (NODE_H + 22), + w: node.width, h: node.height}; + } + var row = Number.isFinite(node.row) ? node.row : Math.round(node.y / 66); + var column = Number.isFinite(node.column) ? node.column : Math.round(node.x / 312); + return {x: row * (NODE_W + 36), y: column * (NODE_H + 72), w: node.width, h: node.height}; + } + return {x: node.x, y: node.y, w: node.width, h: node.height}; + } + function screen(node) { + var box = world(node), scale = state.transform.scale; + return {x: box.x * scale + state.transform.x, y: box.y * scale + state.transform.y, w: box.w * scale, h: box.h * scale}; + } + function inViewport(box, pad) { + return box.x + box.w >= -pad && box.y + box.h >= -pad && box.x <= refs.stage.clientWidth + pad && box.y <= refs.stage.clientHeight + pad; + } + function refresh(resetList) { + if (resetList) state.listLimit = LIST_PAGE; + syncControls(); renderInspector(); renderInventory(resetList); schedule(); + } + function syncControls() { + calculateActive(); + refs.isolated.checked = state.showIsolated; + refs.statusInputs.forEach(function (input, key) { input.checked = state.selectedStatuses.has(key); }); + var enabled = state.selectedStatuses.size; + refs.filterSummary.textContent = enabled === presentStatuses.length ? "Status" : "Status · " + enabled; + refs.graphMode.setAttribute("aria-pressed", String(state.mode === "graph")); + refs.listMode.setAttribute("aria-pressed", String(state.mode === "list")); + refs.stage.hidden = state.mode !== "graph"; refs.inventory.hidden = state.mode !== "list"; + } + + function collect(start, adjacency) { + var found = new Set([start]), pending = [start]; + while (pending.length) { + (adjacency.get(pending.pop()) || []).forEach(function (id) { + if (!found.has(id)) { found.add(id); pending.push(id); } + }); + } + return found; + } + function pathSpotlight() { + if (!state.selected) return null; + if (state.spotlight) return state.spotlight; + var before = collect(state.selected.id, prerequisites), after = collect(state.selected.id, dependents); + var nodes = new Set(before); after.forEach(function (id) { nodes.add(id); }); + state.spotlight = {after: after, before: before, nodes: nodes}; return state.spotlight; + } + function calculateActive() { + if (!state.activeDirty) return; + var directional = null; + if (state.selected && state.direction === "prerequisites") directional = collect(state.selected.id, prerequisites); + if (state.selected && state.direction === "dependents") directional = collect(state.selected.id, dependents); + state.active = data.nodes.filter(function (node) { + return state.selectedStatuses.has(node.status) && (state.showIsolated || !node.isolated || node === state.selected) && + (!directional || directional.has(node.id)); + }); + state.activeIds = new Set(state.active.map(function (node) { return node.id; })); + var hidden = data.nodes.length - state.active.length; + refs.statsText.textContent = state.active.length + " of " + data.nodes.length + " shown" + (hidden ? " / " : ""); + refs.hiddenButton.textContent = hidden ? "+" + hidden + " hidden" : ""; refs.hiddenButton.hidden = hidden === 0; + refs.empty.hidden = state.active.length !== 0; + state.activeDirty = false; + } + + function schedule() { + if (scheduled || state.mode !== "graph") return; + scheduled = true; requestAnimationFrame(function () { scheduled = false; draw(); }); + } + function resize() { + syncSheetAccessibility(); + if (!refs.canvas || !refs.stage.clientWidth || !refs.stage.clientHeight) return; + var ratio = Math.min(2, window.devicePixelRatio || 1); + refs.canvas.width = Math.max(1, Math.round(refs.stage.clientWidth * ratio)); + refs.canvas.height = Math.max(1, Math.round(refs.stage.clientHeight * ratio)); + var nextOrientation = refs.stage.clientWidth <= 620 ? "tb" : "lr"; + var changed = nextOrientation !== state.orientation; state.orientation = nextOrientation; + if (firstResize || changed) { firstResize = false; fit(); } else schedule(); + } + function fit() { + calculateActive(); var nodes = state.active.length ? state.active : data.nodes; if (!nodes.length) return; + var minX = Infinity, minY = Infinity, maxX = -Infinity, maxY = -Infinity; + nodes.forEach(function (node) { + var box = world(node); minX = Math.min(minX, box.x); minY = Math.min(minY, box.y); + maxX = Math.max(maxX, box.x + box.w); maxY = Math.max(maxY, box.y + box.h); + }); + if (atlas) (data.regions || []).forEach(function (region) { + minX = Math.min(minX, region.x); minY = Math.min(minY, region.y); + maxX = Math.max(maxX, region.x + region.width); maxY = Math.max(maxY, region.y + region.height); + }); + var pad = 54, width = Math.max(1, maxX - minX), height = Math.max(1, maxY - minY); + var fitted = Math.min((refs.stage.clientWidth - pad * 2) / width, + (refs.stage.clientHeight - pad * 2) / height); + var readableFloor = atlas ? MIN_ATLAS_SCALE : MIN_READABLE_SCALE; + state.readableCrop = fitted < readableFloor; + state.transform.scale = clamp(Math.max(fitted, readableFloor), MIN_SCALE, 1.35); + state.transform.x = state.readableCrop ? pad - minX * state.transform.scale : + (refs.stage.clientWidth - width * state.transform.scale) / 2 - minX * state.transform.scale; + state.transform.y = state.readableCrop ? pad - minY * state.transform.scale : + (refs.stage.clientHeight - height * state.transform.scale) / 2 - minY * state.transform.scale; + schedule(); + } + function center(node, minimumScale) { + if (!node) return; var box = world(node); state.transform.scale = Math.max(state.transform.scale, minimumScale || .82); + state.transform.x = refs.stage.clientWidth / 2 - (box.x + box.w / 2) * state.transform.scale; + state.transform.y = refs.stage.clientHeight / 2 - (box.y + box.h / 2) * state.transform.scale; schedule(); + } + function zoomAt(factor, x, y) { + var old = state.transform.scale, next = clamp(old * factor, MIN_SCALE, 4); + state.transform.x = x - (x - state.transform.x) * next / old; + state.transform.y = y - (y - state.transform.y) * next / old; state.transform.scale = next; schedule(); + } + + function draw() { + calculateActive(); var ctx = refs.ctx, ratio = Math.min(2, window.devicePixelRatio || 1); + var width = refs.stage.clientWidth, height = refs.stage.clientHeight; + ctx.setTransform(ratio, 0, 0, ratio, 0, 0); ctx.clearRect(0, 0, width, height); drawGrid(ctx, width, height); + if (atlas) drawRegions(ctx); + var visible = state.active.filter(function (node) { return inViewport(screen(node), 80); }); + var edgeIndexes = new Set(); + visible.forEach(function (node) { (incident.get(node.id) || []).forEach(function (index) { edgeIndexes.add(index); }); }); + var spotlight = pathSpotlight(); + edgeIndexes.forEach(function (index) { + var edge = data.edges[index]; if (!state.activeIds.has(edge.source) || !state.activeIds.has(edge.target)) return; + var source = byId.get(edge.source), target = byId.get(edge.target); if (!source || !target) return; + var a = screen(source), b = screen(target); + if (!inViewport({x: Math.min(a.x, b.x), y: Math.min(a.y, b.y), + w: Math.abs(b.x - a.x) + Math.max(a.w, b.w), h: Math.abs(b.y - a.y) + Math.max(a.h, b.h)}, 40)) return; + var highlighted = !spotlight || + (spotlight.before.has(edge.source) && spotlight.before.has(edge.target)) || + (spotlight.after.has(edge.source) && spotlight.after.has(edge.target)); + if (edge.statement) drawEdge(ctx, a, b, false, highlighted, edge.statement, edge.proof ? -4 : 0); + if (edge.proof) drawEdge(ctx, a, b, true, highlighted, edge.proof, edge.statement ? 4 : 0); + }); + visible.forEach(function (node) { drawPlate(ctx, node, screen(node), !spotlight || spotlight.nodes.has(node.id)); }); + updateOverlays(visible, spotlight); + } + function drawRegions(ctx) { + var regionColors = isDark() ? + ["#17233a", "#24203b", "#16312d", "#332719", "#2d1f2a", "#1d2d3a", "#2c2b20"] : + ["#eaf1fb", "#f0ebfb", "#e8f5f0", "#fbf2df", "#f8eaf0", "#e8f3f8", "#f4f2df"]; + (data.regions || []).forEach(function (region, index) { + var box = {x: region.x * state.transform.scale + state.transform.x, + y: region.y * state.transform.scale + state.transform.y, + w: region.width * state.transform.scale, h: region.height * state.transform.scale}; + if (!inViewport(box, 60)) return; + ctx.save(); ctx.fillStyle = regionColors[index % regionColors.length]; + ctx.strokeStyle = isDark() ? "#35435c" : "#b9c7da"; ctx.lineWidth = 1.2; + rounded(ctx, box.x, box.y, box.w, box.h, 18); ctx.fill(); ctx.stroke(); + ctx.fillStyle = isDark() ? "#d9e3f2" : "#30445f"; ctx.font = "700 13px sans-serif"; + ctx.textAlign = "left"; ctx.fillText(region.label + " · " + region.count, box.x + 13, box.y + 21); + ctx.restore(); + }); + } + function drawGrid(ctx, width, height) { + ctx.save(); ctx.fillStyle = isDark() ? "rgba(255,255,255,.055)" : "rgba(15,23,42,.055)"; + var step = 32, offsetX = ((state.transform.x % step) + step) % step, offsetY = ((state.transform.y % step) + step) % step; + for (var x = offsetX; x < width; x += step) for (var y = offsetY; y < height; y += step) ctx.fillRect(x, y, 1, 1); + ctx.restore(); + } + function rounded(ctx, x, y, w, h, radius) { + var r = Math.min(radius, w / 2, h / 2); ctx.beginPath(); ctx.moveTo(x + r, y); ctx.lineTo(x + w - r, y); + ctx.quadraticCurveTo(x + w, y, x + w, y + r); ctx.lineTo(x + w, y + h - r); + ctx.quadraticCurveTo(x + w, y + h, x + w - r, y + h); ctx.lineTo(x + r, y + h); + ctx.quadraticCurveTo(x, y + h, x, y + h - r); ctx.lineTo(x, y + r); ctx.quadraticCurveTo(x, y, x + r, y); ctx.closePath(); + } + function drawPlate(ctx, node, box, highlighted) { + var color = colors(node), tiny = state.transform.scale < .32; + ctx.save(); ctx.globalAlpha = highlighted ? (tiny ? .82 : .24) : .07; ctx.fillStyle = color.fill; + ctx.strokeStyle = color.stroke; ctx.lineWidth = tiny ? 1 : 1.25; + if (atlas && node.kind === "scope") { + ctx.beginPath(); ctx.arc(box.x + box.w / 2, box.y + box.h / 2, Math.min(box.w, box.h) / 2, 0, Math.PI * 2); + ctx.fill(); ctx.stroke(); ctx.restore(); return; + } + if (tiny) ctx.fillRect(box.x, box.y, Math.max(3, box.w), Math.max(3, box.h)); + else { rounded(ctx, box.x, box.y, box.w, box.h, 7 * state.transform.scale); ctx.fill(); ctx.stroke(); } + ctx.restore(); + } + function drawEdge(ctx, a, b, dashed, highlighted, count, offset) { + var horizontal = state.orientation === "lr"; + var ax = horizontal ? a.x + a.w : a.x + a.w / 2 + offset; + var ay = horizontal ? a.y + a.h / 2 + offset : a.y + a.h; + var bx = horizontal ? b.x : b.x + b.w / 2 + offset; + var by = horizontal ? b.y + b.h / 2 + offset : b.y; + ctx.save(); ctx.globalAlpha = highlighted ? .58 : .065; ctx.strokeStyle = isDark() ? "#a8b0bb" : "#64748b"; + ctx.fillStyle = ctx.strokeStyle; ctx.lineWidth = highlighted ? 1.35 : 1; if (dashed) ctx.setLineDash([5, 5]); + ctx.beginPath(); ctx.moveTo(ax, ay); + if (horizontal) { var mx = ax + (bx - ax) * .5; ctx.bezierCurveTo(mx, ay, mx, by, bx, by); } + else { var my = ay + (by - ay) * .5; ctx.bezierCurveTo(ax, my, bx, my, bx, by); } + ctx.stroke(); ctx.setLineDash([]); + if (state.transform.scale > .18) { + ctx.beginPath(); + if (horizontal) { ctx.moveTo(bx, by); ctx.lineTo(bx - 6, by - 3.5); ctx.lineTo(bx - 6, by + 3.5); } + else { ctx.moveTo(bx, by); ctx.lineTo(bx - 3.5, by - 6); ctx.lineTo(bx + 3.5, by - 6); } + ctx.closePath(); ctx.fill(); + } + if (count > 1 && state.transform.scale > .32) { + ctx.globalAlpha = highlighted ? .82 : .2; ctx.font = Math.max(9, 10 * state.transform.scale) + "px sans-serif"; + ctx.textAlign = "center"; ctx.fillText("×" + count, (ax + bx) / 2, (ay + by) / 2 - 4); + } + ctx.restore(); + } + + function updateOverlays(visible, spotlight) { + var candidates = state.transform.scale >= .34 ? visible.slice() : []; + if (state.selected && state.activeIds.has(state.selected.id) && candidates.indexOf(state.selected) < 0) candidates.push(state.selected); + candidates.sort(function (a, b) { + if (a === state.selected) return -1; if (b === state.selected) return 1; + var ab = screen(a), bb = screen(b); return ab.y - bb.y || ab.x - bb.x || a._index - b._index; + }); + var omitted = Math.max(0, candidates.length - MAX_DOM_NODES); candidates = candidates.slice(0, MAX_DOM_NODES); + var keep = new Set(candidates.map(function (node) { return node.id; })); + overlays.forEach(function (control, id) { if (!keep.has(id)) { control.remove(); overlays.delete(id); } }); + candidates.forEach(function (node, index) { + var control = overlays.get(node.id); + if (!control) { control = makeNodeControl(node); overlays.set(node.id, control); refs.nodeLayer.appendChild(control); } + var box = screen(node), color = colors(node); + control.style.transform = "translate3d(" + box.x + "px," + box.y + "px,0) scale(" + state.transform.scale + ")"; + control.style.width = node.width + "px"; control.style.height = node.height + "px"; + control.style.setProperty("--dag-node-fill", color.fill); control.style.setProperty("--dag-node-stroke", color.stroke); + control.style.setProperty("--dag-node-text", color.text); control.dataset.selected = String(node === state.selected); + if (atlas && node.kind === "scope") control.style.setProperty("--dag-status-ring", statusRing(node)); + control.dataset.subdued = String(Boolean(spotlight && !spotlight.nodes.has(node.id))); + control.tabIndex = node === state.selected || (!state.selected && index === 0) ? 0 : -1; + }); + refs.density.hidden = !state.readableCrop && omitted === 0 && !(visible.length && state.transform.scale < .34); + refs.density.textContent = state.readableCrop ? "Readable window · pan or Browse to see all " + state.active.length + " items" : + omitted ? "+" + omitted + " node labels hidden at this zoom" : + (visible.length && state.transform.scale < .34 ? "Zoom in to reveal " + visible.length + " node labels" : ""); + } + function makeNodeControl(node) { + var control = button("bp-dag-node", ""); control.dataset.autoformNodeId = node.id; control.dataset.kind = node.kind || "node"; + var scopeMeta = node.kind === "scope" ? (node.member_count || 0) + " items · " + + (node.internal_dependency_count || 0) + " internal links" : + node.kind === "boundary" ? "External scope · open" : null; + control.setAttribute("aria-label", node.title + ", " + (scopeMeta || statusLabel(node.status)) + + (node.isolated ? ", no dependency edges in this view" : "")); + var content = atlas && node.kind === "scope" ? element("span", "bp-dag-node-core") : control; + content.appendChild(element("span", "bp-dag-node-title", node.title)); + content.appendChild(element("span", "bp-dag-node-meta", scopeMeta || statusLabel(node.status) + " · " + node.id)); + if (content !== control) control.appendChild(content); + control.addEventListener("click", function (event) { event.stopPropagation(); activateNode(node, false); }); + control.addEventListener("dblclick", function () { var href = safeHref(node.url); if (href) window.location.href = href; }); + control.addEventListener("keydown", function (event) { + if (/^Arrow(Left|Right|Up|Down)$/.test(event.key)) { + var next = nearest(node, event.key); + if (next) { + event.preventDefault(); center(next, .7); selectNode(next, "push", false); + focusNodeControl(next); + } + } else if (event.key === "Escape") { event.preventDefault(); clearSelection(true); } + }); + return control; + } + function nearest(node, key) { + var from = world(node), fx = from.x + from.w / 2, fy = from.y + from.h / 2, best = null, bestScore = Infinity; + state.active.forEach(function (candidate) { + if (candidate === node) return; + var box = world(candidate), dx = box.x + box.w / 2 - fx, dy = box.y + box.h / 2 - fy; + if ((key === "ArrowLeft" && dx >= 0) || (key === "ArrowRight" && dx <= 0) || + (key === "ArrowUp" && dy >= 0) || (key === "ArrowDown" && dy <= 0)) return; + var primary = key === "ArrowLeft" || key === "ArrowRight" ? Math.abs(dx) : Math.abs(dy); + var cross = key === "ArrowLeft" || key === "ArrowRight" ? Math.abs(dy) : Math.abs(dx); + var score = primary + cross * 2.4; if (score < bestScore) { bestScore = score; best = candidate; } + }); + return best; + } + + function pointerDown(event) { + if (event.target.closest && event.target.closest(".bp-dag-node")) return; + state.pointers.set(event.pointerId, {x: event.clientX, y: event.clientY, type: event.pointerType}); + state.moved = false; + if (event.pointerType !== "touch" || host.getAttribute("data-layout") === "app") { + refs.stage.setPointerCapture(event.pointerId); refs.stage.dataset.dragging = "true"; + } else if (state.pointers.size === 2) { + refs.stage.setPointerCapture(event.pointerId); refs.stage.dataset.dragging = "true"; + } + if (state.pointers.size === 2) state.pinch = pinchState(); + } + function pinchState() { + var points = Array.from(state.pointers.values()), dx = points[1].x - points[0].x, dy = points[1].y - points[0].y; + return {distance: Math.max(1, Math.hypot(dx, dy)), x: (points[0].x + points[1].x) / 2, y: (points[0].y + points[1].y) / 2}; + } + function pointerMove(event) { + if (!state.pointers.has(event.pointerId)) return; + var previous = state.pointers.get(event.pointerId); state.pointers.set(event.pointerId, {x: event.clientX, y: event.clientY}); + if (event.pointerType === "touch" && state.pointers.size < 2 && host.getAttribute("data-layout") !== "app") { + if (Math.abs(event.clientX - previous.x) + Math.abs(event.clientY - previous.y) > 4) state.moved = true; + return; + } + if (state.pointers.size === 1) { + var dx = event.clientX - previous.x, dy = event.clientY - previous.y; + if (Math.abs(dx) + Math.abs(dy) > 1) state.moved = true; + state.transform.x += dx; state.transform.y += dy; schedule(); + } else if (state.pointers.size === 2) { + var next = pinchState(), rect = refs.stage.getBoundingClientRect(); + state.transform.x += next.x - state.pinch.x; state.transform.y += next.y - state.pinch.y; + zoomAt(next.distance / state.pinch.distance, next.x - rect.left, next.y - rect.top); + state.pinch = next; state.moved = true; + } + } + function pointerUp(event) { + if (!state.pointers.has(event.pointerId)) return; + var wasSingle = state.pointers.size === 1; state.pointers.delete(event.pointerId); + if (state.pointers.size < 2) state.pinch = null; + if (!state.pointers.size) refs.stage.dataset.dragging = "false"; + if (event.type === "pointerup" && wasSingle && !state.moved) clearSelection(true); + } + + function searchScore(node, query) { + var title = node.title.toLocaleLowerCase(), id = node.id.toLocaleLowerCase(); + if (title === query) return [0, "Exact title"]; if (id === query) return [1, "Exact id"]; + if (title.startsWith(query)) return [2, "Title prefix"]; if (id.startsWith(query)) return [3, "Id prefix"]; + if (title.split(/\s+/).some(function (word) { return word.startsWith(query); })) return [4, "Word prefix"]; + if (title.indexOf(query) >= 0) return [5, "Title match"]; if (id.indexOf(query) >= 0) return [6, "Id match"]; + return null; + } + function ensureGlobalSearch() { + var source = host.getAttribute("data-catalog-src"); + if (!source || state.searchPromise || state.searchNodes !== data.nodes) return state.searchPromise; + state.searchLoading = true; + state.searchPromise = fetch(source, {credentials: "same-origin"}).then(function (response) { + if (!response.ok) throw new Error("HTTP " + response.status); + return response.json().then(function (index) { return {index: index, url: response.url}; }); + }).then(function (loaded) { + if (!loaded.index || loaded.index.schema !== "autoform-dag-search/v1" || !Array.isArray(loaded.index.nodes)) + throw new Error("unsupported search index"); + loaded.index.nodes.forEach(function (node, index) { + node._index = index; + if (node.url) node.url = new URL(node.url, loaded.url).href; + }); + state.searchNodes = loaded.index.nodes; state.searchCacheQuery = null; state.searchError = null; + refs.search.placeholder = "Search " + loaded.index.nodes.length.toLocaleString() + " roadmap entries"; + }).catch(function (error) { + state.searchError = error.message; + }).then(function () { + state.searchLoading = false; if (state.query) { renderSearch(); renderInventory(true); } + }); + return state.searchPromise; + } + function redirectLegacyFocus() { + var requested = locationParams().get("node"); + if (!requested || byId.has(requested) || !host.getAttribute("data-catalog-src")) return; + ensureGlobalSearch().then(function () { + var target = state.searchNodes.find(function (node) { return node.id === requested; }); + var href = target && safeHref(target.url); + if (href && new URL(href, window.location.href).href !== window.location.href) window.location.replace(href); + }); + } + function searchMatches() { + var query = state.query.toLocaleLowerCase(); if (!query) return []; + if (query === state.searchCacheQuery) return state.searchCache; + state.searchCacheQuery = query; + state.searchCache = state.searchNodes.map(function (node) { + var score = searchScore(node, query); return score ? {node: node, rank: score[0], reason: score[1]} : null; + }).filter(Boolean).sort(function (a, b) { return a.rank - b.rank || a.node._index - b.node._index; }); + return state.searchCache; + } + function renderSearch() { + refs.searchResults.textContent = ""; if (!state.query) { closeSearch(); return; } + var matches = searchMatches(), list = element("ul", "bp-dag-results"); + matches.slice(0, state.searchLimit).forEach(function (match) { + var item = element("li"), choose = button("bp-dag-result", ""); + choose.appendChild(element("span", "bp-dag-result-title", match.node.title)); + choose.appendChild(element("span", "bp-dag-result-id", match.node.id)); + choose.appendChild(element("span", "bp-dag-result-reason", match.reason)); + choose.addEventListener("click", function () { activateNode(match.node, true); }); item.appendChild(choose); list.appendChild(item); + choose.addEventListener("keydown", searchResultKeydown); + }); + refs.searchResults.appendChild(list); + if (matches.length > state.searchLimit) { + var remaining = matches.length - state.searchLimit, increment = Math.min(SEARCH_PAGE, remaining); + var more = button("bp-dag-load-more", "Show " + increment + " more of " + remaining); + more.addEventListener("click", function () { + var previous = state.searchLimit; + state.searchLimit = Math.min(matches.length, state.searchLimit + SEARCH_PAGE); renderSearch(); + var results = refs.searchResults.querySelectorAll(".bp-dag-result"); + if (results[previous]) results[previous].focus(); + }); + more.addEventListener("keydown", searchResultKeydown); + refs.searchResults.appendChild(more); + } + if (!matches.length) refs.searchResults.appendChild(element("p", "bp-dag-overview", "No matching title or article id.")); + if (state.searchLoading) refs.searchResults.appendChild(element("p", "bp-dag-overview", "Searching the whole roadmap…")); + else if (state.searchError) refs.searchResults.appendChild(element("p", "bp-dag-overview", "Whole-roadmap search is unavailable; showing this view.")); + refs.searchResults.hidden = false; refs.search.setAttribute("aria-expanded", "true"); + } + function searchResultKeydown(event) { + if (event.key === "Escape") { + event.preventDefault(); closeSearch(); refs.search.focus(); return; + } + if (event.key !== "ArrowDown" && event.key !== "ArrowUp") return; + var controls = Array.from(refs.searchResults.querySelectorAll("button")); + var index = controls.indexOf(event.currentTarget); + var next = controls[index + (event.key === "ArrowDown" ? 1 : -1)]; + if (next) { event.preventDefault(); next.focus(); } + else if (event.key === "ArrowUp") { event.preventDefault(); refs.search.focus(); } + } + function closeSearch() { refs.searchResults.hidden = true; refs.search.setAttribute("aria-expanded", "false"); } + function activateNode(node, moveCamera) { + var href = safeHref(node.url); + if (!byId.has(node.id) && href) { window.location.href = href; return; } + if (node.kind === "boundary" && href) { window.location.href = href; return; } + if (node.kind === "scope" && state.selected === node && href) { window.location.href = href; return; } + chooseNode(node, moveCamera); + } + function chooseNode(node, moveCamera) { + closeSearch(); if (!state.selectedStatuses.has(node.status)) state.selectedStatuses.add(node.status); + if (node.isolated) state.showIsolated = true; state.activeDirty = true; + state.mode = state.mapAllowed ? "graph" : "list"; + selectNode(node, "push", moveCamera && state.mapAllowed); + if (state.mapAllowed) focusNodeControl(node); + else requestAnimationFrame(function () { + var target = refs.inspectorInner.querySelector("a, button"); if (target) target.focus(); + }); + } + function focusNodeControl(node) { + requestAnimationFrame(function () { requestAnimationFrame(function () { + var control = overlays.get(node.id); if (control) control.focus(); else refs.sheetHandle.focus(); + }); }); + } + + function selectNode(node, historyMode, moveCamera) { + if (!node) return; if (!state.selected || state.selected.id !== node.id) state.direction = "both"; + state.selected = node; state.activeDirty = true; state.spotlight = null; + host.classList.add("bp-dag-has-selection"); setSheet(true); + syncControls(); renderInspector(); renderInventory(true); + refs.announcement.textContent = "Selected " + node.title + ", " + statusLabel(node.status); + if (historyMode) writeLocation(historyMode); if (moveCamera) center(node, .82); else schedule(); + } + function clearSelection(updateHistory) { + state.selected = null; state.direction = "both"; state.activeDirty = true; state.spotlight = null; + host.classList.remove("bp-dag-has-selection"); + setSheet(false); + renderInspector(); renderInventory(true); requestAnimationFrame(fit); if (updateHistory) writeLocation("push"); + } + function setSheet(open) { + host.classList.toggle("bp-dag-sheet-open", Boolean(open)); + refs.sheetHandle.setAttribute("aria-expanded", String(Boolean(open))); + syncSheetAccessibility(); + } + function syncSheetAccessibility() { + if (!refs.inspectorInner || !refs.sheetHandle) return; + var mobile = window.matchMedia && window.matchMedia("(max-width: 680px)").matches; + var collapsed = mobile && !host.classList.contains("bp-dag-sheet-open"); + if (collapsed) { + if (refs.inspectorInner.contains(document.activeElement)) refs.sheetHandle.focus(); + refs.inspectorInner.setAttribute("inert", ""); refs.inspectorInner.setAttribute("aria-hidden", "true"); + } else { + refs.inspectorInner.removeAttribute("inert"); refs.inspectorInner.removeAttribute("aria-hidden"); + } + } + function setDirection(direction) { + state.direction = direction; state.activeDirty = true; writeLocation("push"); refresh(true); fit(); + } + function revealAll() { + state.selectedStatuses = new Set(presentStatuses); state.showIsolated = true; state.direction = "both"; + state.activeDirty = true; writeLocation("replace"); refresh(true); fit(); + } + function onStatusChange() { + state.selectedStatuses = new Set(); + refs.statusInputs.forEach(function (input, key) { if (input.checked) state.selectedStatuses.add(key); }); + if (state.selected && !state.selectedStatuses.has(state.selected.status)) { + state.selected = null; state.direction = "both"; state.spotlight = null; + host.classList.remove("bp-dag-has-selection"); setSheet(false); + refs.announcement.textContent = "Selection cleared because its status is hidden."; + } + state.activeDirty = true; writeLocation("replace"); refresh(true); + } + function setMode(mode, updateHistory) { + if (mode === "graph" && !state.mapAllowed) return; + state.mode = mode; syncControls(); if (mode === "list") renderInventory(true); else schedule(); + if (updateHistory) writeLocation("replace"); + } + + function renderInspector() { + refs.inspectorInner.textContent = ""; refs.sheetHandle.textContent = state.selected ? state.selected.title : "Graph details"; + if (!state.selected) { + refs.inspectorInner.appendChild(element("p", "bp-dag-kicker", atlas ? "Mathematics knowledge map" : "Dependency explorer")); + refs.inspectorInner.appendChild(element("h2", "", data.title || (atlas ? "Mathematics atlas" : "Dependencies"))); + if (view.summary) refs.inspectorInner.appendChild(element("p", "bp-dag-summary", view.summary)); + var overview = element("p", "bp-dag-overview"); overview.appendChild(element("strong", "", data.nodes.length + (atlas ? " topics" : " nodes"))); + overview.appendChild(document.createTextNode(" · " + (data.edge_count || data.edges.length) + + " authored dependencies.")); refs.inspectorInner.appendChild(overview); + var internalDependencies = data.nodes.reduce(function (total, node) { + return total + (node.internal_dependency_count || 0); + }, 0); + if (internalDependencies) refs.inspectorInner.appendChild(element("p", "bp-dag-overview", + internalDependencies + " additional authored dependencies lie inside the visible topics.")); + if (atlas && !data.edges.length) refs.inspectorInner.appendChild(element("p", "bp-dag-overview", + "No cross-topic dependency links are authored at this level. Bubble size shows scope; rings show formalization status. Select a topic to read its mathematical overview.")); + if (atlas && (data.regions || []).length) { + var regionSection = element("section", "bp-dag-section"); regionSection.appendChild(element("h3", "", "Mathematical regions")); + var regionRows = element("div", "bp-dag-distribution"); + data.regions.forEach(function (region) { + var regionRow = element("div", "bp-dag-distribution-row"); regionRow.appendChild(element("span", "", region.label)); + regionRow.appendChild(element("span", "", String(region.count))); regionRows.appendChild(regionRow); + }); + regionSection.appendChild(regionRows); refs.inspectorInner.appendChild(regionSection); + } + var statusSection = element("section", "bp-dag-section"); statusSection.appendChild(element("h3", "", "Status at this level")); + var statusRows = element("div", "bp-dag-distribution"); + statusCounts.forEach(function (count, key) { + var statusRow = element("div", "bp-dag-distribution-row"); statusRow.appendChild(element("span", "", statusLabel(key))); + statusRow.appendChild(element("span", "", String(count))); statusRows.appendChild(statusRow); + }); + statusSection.appendChild(statusRows); refs.inspectorInner.appendChild(statusSection); + if (statusCounts.has("inventory_checked")) refs.inspectorInner.appendChild(element("p", "bp-dag-overview", + "Inventory checked is neutral: it records inspection, not a mathematical proof.")); + refs.inspectorInner.appendChild(element("p", "bp-dag-overview", + atlas ? "Click a topic to read it; click it again or use Explore topic to dive in. Browse exposes the same map as a complete accessible list." : + "The map carries dependency topology; Relations and Browse expose the same nodes as keyboard-accessible controls.")); return; + } + var node = state.selected, header = element("div", "bp-dag-inspector-header"), titleWrap = element("div"); + titleWrap.appendChild(element("p", "bp-dag-kicker", node.kind === "scope" ? "Scope" : + node.kind === "boundary" ? "External scope" : (node.declaration || "Roadmap item"))); + titleWrap.appendChild(element("h2", "", node.title)); header.appendChild(titleWrap); + var close = button("bp-dag-close", "×", "Clear node selection"); close.addEventListener("click", function () { clearSelection(true); }); + header.appendChild(close); refs.inspectorInner.appendChild(header); refs.inspectorInner.appendChild(element("code", "bp-dag-node-id", node.id)); + var pill = element("span", "bp-dag-status-pill", statusLabel(node.status)), color = colors(node); + pill.style.setProperty("--dag-pill-fill", color.fill); pill.style.setProperty("--dag-pill-stroke", color.stroke); + refs.inspectorInner.appendChild(pill); + var href = safeHref(node.url); + if (href) { + var open = element("a", "bp-dag-open", node.kind === "scope" || node.kind === "boundary" ? "Explore topic" : "Open article"); + open.href = href; refs.inspectorInner.appendChild(open); + } + if (node.summary) refs.inspectorInner.appendChild(element("p", "bp-dag-summary", node.summary)); + else if (node.kind === "scope") refs.inspectorInner.appendChild(element("p", "bp-dag-summary", + "This topic contains " + (node.member_count || 0) + " roadmap items. Explore it to see its mathematical subtopics and dependency structure.")); + if (node.lean) refs.inspectorInner.appendChild(element("p", "bp-dag-lean", "Lean: " + node.lean)); + if (node.kind === "scope" && node.internal_dependency_count) refs.inspectorInner.appendChild(element("p", "bp-dag-overview", + node.internal_dependency_count + " authored dependencies connect results inside this topic.")); + var before = prerequisites.get(node.id) || [], after = dependents.get(node.id) || []; + var path = pathSpotlight(), beforeCount = path ? path.before.size - 1 : 0; + var afterCount = path ? path.after.size - 1 : 0; + if (before.length || after.length) { + var paths = element("section", "bp-dag-section"); paths.appendChild(element("h3", "", "Path spotlight")); + var pivots = element("div", "bp-dag-pivots"); + [["Prerequisites " + beforeCount, "prerequisites", beforeCount], ["All paths", "both", 1], + ["Dependents " + afterCount, "dependents", afterCount]].forEach(function (entry) { + var pivot = button("bp-dag-pivot", entry[0]); pivot.disabled = !entry[2]; + pivot.setAttribute("aria-pressed", String(state.direction === entry[1])); + pivot.addEventListener("click", function () { setDirection(entry[1]); }); pivots.appendChild(pivot); + }); + paths.appendChild(pivots); refs.inspectorInner.appendChild(paths); + } + appendRelations("Direct prerequisites", before); appendRelations("Direct dependents", after); + var counts = node.status_counts || {}; + var entries = Array.isArray(counts) ? counts : Object.keys(counts).map(function (key) { return [key, counts[key]]; }); + if (entries.length > 1 || (node.member_count || 1) > 1) { + var distribution = element("section", "bp-dag-section"); + distribution.appendChild(element("h3", "", (node.member_count || 1) + " items in this scope")); + var rows = element("div", "bp-dag-distribution"); + entries.forEach(function (entry) { + var row = element("div", "bp-dag-distribution-row"); row.appendChild(element("span", "", statusLabel(entry[0]))); + row.appendChild(element("span", "", String(entry[1]))); rows.appendChild(row); + }); + distribution.appendChild(rows); refs.inspectorInner.appendChild(distribution); + } + } + function appendRelations(label, ids) { + if (!ids.length) return; + var section = element("section", "bp-dag-section"); section.appendChild(element("h3", "", label + " (" + ids.length + ")")); + var list = element("ul", "bp-dag-relation-list"), visible = 0; + var more = button("bp-dag-load-more", ""); + function appendNextBatch() { + var next = Math.min(visible + RELATION_PAGE, ids.length); + ids.slice(visible, next).forEach(function (id) { + var related = byId.get(id); if (!related) return; + var item = element("li"), choose = button("bp-dag-relation-button", related.title); + choose.addEventListener("click", function () { activateNode(related, true); }); item.appendChild(choose); list.appendChild(item); + }); + visible = next; + more.hidden = visible >= ids.length; + more.textContent = more.hidden ? "" : "Show " + Math.min(RELATION_PAGE, ids.length - visible) + " more"; + } + more.addEventListener("click", appendNextBatch); appendNextBatch(); + section.appendChild(list); section.appendChild(more); refs.inspectorInner.appendChild(section); + } + + function inventoryNodes() { + var nodes = data.nodes.filter(function (node) { return state.selectedStatuses.has(node.status); }); + if (state.query) return searchMatches().map(function (match) { return match.node; }).filter(function (node) { + return state.selectedStatuses.has(node.status); + }); + return nodes; + } + function renderInventory(resetScroll) { + if (!refs.inventoryList) return; + var nodes = inventoryNodes(), visible = nodes.slice(0, state.listLimit); refs.inventoryList.textContent = ""; + visible.forEach(function (node) { + var item = element("li"), row = button("bp-dag-inventory-row", ""); + row.appendChild(element("span", "bp-dag-inventory-title", node.title)); + row.appendChild(element("span", "bp-dag-inventory-id", node.id)); + row.appendChild(element("span", "bp-dag-inventory-meta", statusLabel(node.status) + (node.isolated ? " · isolated" : ""))); + row.addEventListener("click", function () { activateNode(node, true); }); item.appendChild(row); refs.inventoryList.appendChild(item); + }); + refs.inventorySummary.textContent = visible.length + " of " + nodes.length + " listed" + + (state.mapAllowed ? " · items without edges included" : " · map unavailable above " + MAX_MAP_NODES + " items"); + refs.loadMore.hidden = visible.length >= nodes.length; + refs.loadMore.textContent = visible.length < nodes.length ? "Show " + Math.min(LIST_PAGE, nodes.length - visible.length) + " more" : ""; + if (resetScroll && refs.inventoryScroll) refs.inventoryScroll.scrollTop = 0; + } + + function locationParams() { return new URLSearchParams(window.location.hash.replace(/^#/, "")); } + function applyLocation(initial) { + var params = locationParams(), node = byId.get(params.get("node")) || null, direction = params.get("direction"); + state.selected = node; + state.direction = node && /^(prerequisites|dependents|both)$/.test(direction || "") ? direction : "both"; + var requested = params.get("status"); + if (requested === "-") state.selectedStatuses = new Set(); + else if (requested) state.selectedStatuses = new Set(requested.split(",").filter(function (key) { + return presentStatuses.indexOf(key) >= 0; + })); + else state.selectedStatuses = new Set(presentStatuses); + state.showIsolated = params.has("isolates") ? params.get("isolates") === "1" : view.kind !== "full"; + state.mode = params.get("view") === "list" || !state.mapAllowed ? "list" : "graph"; + state.activeDirty = true; state.spotlight = null; + if (node) { + state.selectedStatuses.add(node.status); if (node.isolated && !params.has("isolates")) state.showIsolated = true; + host.classList.add("bp-dag-has-selection"); setSheet(true); + } else { host.classList.remove("bp-dag-has-selection"); setSheet(false); } + syncControls(); renderInspector(); renderInventory(true); schedule(); + if (node) setTimeout(function () { center(node, .82); }, initial ? 0 : 0); + } + function writeLocation(method) { + var params = new URLSearchParams(); + if (state.selected) params.set("node", state.selected.id); + if (state.selected && state.direction !== "both") params.set("direction", state.direction); + if (state.selectedStatuses.size !== presentStatuses.length) params.set("status", + state.selectedStatuses.size ? Array.from(state.selectedStatuses).join(",") : "-"); + var defaultIsolates = view.kind !== "full"; + if (state.showIsolated !== defaultIsolates) params.set("isolates", state.showIsolated ? "1" : "0"); + if (state.mode === "list") params.set("view", "list"); + var hash = params.toString(); + var target = window.location.pathname + window.location.search + (hash ? "#" + hash : ""); + var current = window.location.pathname + window.location.search + window.location.hash; + if (target === current) return; + window.history[method + "State"](null, "", target); + } + + syncControls(); + } + + function boot() { document.querySelectorAll(".bp-dag-viewer[data-graph-src]").forEach(start); } + if (document.readyState === "loading") document.addEventListener("DOMContentLoaded", boot); else boot(); +})(); +""" + + +__all__ = [ + "MAX_LAYOUT_ROWS", + "MAX_MERMAID_CHARACTERS", + "MAX_MERMAID_EDGE_LINES", + "SCHEMA", + "SEARCH_SCHEMA", + "render_container", + "requires_interactive", + "viewer_script", + "write_payload", + "write_search_index", +] diff --git a/autoform_cli/dashboard.py b/autoform_cli/dashboard.py index 2b464829..c99e3ff1 100644 --- a/autoform_cli/dashboard.py +++ b/autoform_cli/dashboard.py @@ -12,7 +12,12 @@ from .claims import ClaimTransportError, author_claim_key from .graph import GraphValidationError -from .render import LIVE_SCRIPT, PUBLICATION_MANIFEST, publication_source_revision +from .render import ( + LIVE_SCRIPT, + PUBLICATION_MANIFEST, + PUBLICATION_SCHEMA, + publication_source_revision, +) from .runtime import RuntimeGraph, RuntimeNode, RuntimeProjectionError @@ -156,7 +161,7 @@ def guarded() -> dict[str, object]: manifest = json.loads(encoded) if ( not isinstance(manifest, dict) - or manifest.get("schema") != "autoform-publication/v1" + or manifest.get("schema") != PUBLICATION_SCHEMA or manifest.get("complete") is not True or manifest.get("source_revision") != publication_source_revision(blueprint) ): diff --git a/autoform_cli/graph.py b/autoform_cli/graph.py index ebf73854..7788ca69 100644 --- a/autoform_cli/graph.py +++ b/autoform_cli/graph.py @@ -10,23 +10,28 @@ from __future__ import annotations import hashlib +import json import re -from dataclasses import dataclass +from dataclasses import MISSING, dataclass, fields, replace +from html import unescape from pathlib import Path from urllib.parse import unquote, urlsplit from .lean import declaration_names - _HEADING = re.compile(r"^ {0,3}(#{1,6})[ \t]+(.+?)[ \t]*#*[ \t]*$") _FENCE = re.compile(r"^ {0,3}(`{3,}|~{3,})") _LINK = re.compile(r"(?]+>|[^)\s]+)(?:\s+[^)]*)?\)") _HTML_COMMENT = re.compile(r"|$)", re.DOTALL) _INLINE_CODE = re.compile(r"(`+).*?\1") +_MARKDOWN_LINK_TEXT = re.compile(r"!?\[([^\]]+)\]\([^)]*\)") +_HTML_TAG = re.compile(r"<[^>]+>") ARTICLE_ID_PATTERN = re.compile(r"af_[0-9a-f]{24}\Z") _FRONTMATTER_KEYS = frozenset( { "article_id", + "area", + "catalog", "declaration", "lean", "statement", @@ -44,6 +49,9 @@ _RETRACTED = "retracted" _TRUE = frozenset({"true", "yes"}) _FALSE = frozenset({"false", "no"}) +_CATALOG_DECLARATION_KEYS = frozenset( + {"declaration", "mathlib", "mathlib_declaration", "mathlib_file"} +) #: ``## Depends on`` carries the prerequisites needed to *state* a node; #: ``## Proof depends on`` carries the extra prerequisites its *proof* needs. @@ -51,6 +59,8 @@ _STATEMENT_SECTION = "depends on" _PROOF_SECTION = "proof depends on" _SOURCES_SECTION = "sources" +ATLAS_SCHEMA = "autoform-atlas/v1" +_MAX_ATLAS_BYTES = 1_000_000 class GraphValidationError(ValueError): @@ -97,6 +107,9 @@ class Node: depth: int = 0 article_id: str | None = None source_sha256: str | None = None + catalog: str | None = None + summary: str | None = None + area: str | None = None @property def formalizable(self) -> bool: @@ -104,6 +117,32 @@ def formalizable(self) -> bool: return self.declaration is not None + +def _node_getstate(node: Node) -> list[object]: + """Keep the public slotted record append-compatible for old pickles.""" + + return [getattr(node, item.name) for item in fields(node)] + + +def _node_setstate(node: Node, state: list[object]) -> None: + node_fields = fields(node) + if len(state) > len(node_fields): + raise ValueError("Node pickle has unsupported fields") + for item, value in zip(node_fields, state, strict=False): + object.__setattr__(node, item.name, value) + for item in node_fields[len(state) :]: + if item.default is MISSING: + raise ValueError(f"Node pickle is missing required field {item.name!r}") + object.__setattr__(node, item.name, item.default) + + +# Python 3.10's frozen+slots dataclass transformation overwrites methods defined +# in the class body. Assign after decoration so every supported Python uses the +# same append-compatible state contract. +Node.__getstate__ = _node_getstate # type: ignore[method-assign] +Node.__setstate__ = _node_setstate # type: ignore[method-assign] + + @dataclass(frozen=True, slots=True) class Graph: """A validated blueprint graph, keyed by stable node id.""" @@ -133,6 +172,7 @@ class _ParsedNode: proof_targets: tuple[str, ...] source_targets: tuple[str, ...] metadata: dict[str, str] + summary: str | None @dataclass(frozen=True, slots=True) @@ -223,6 +263,20 @@ def resolve(targets: tuple[str, ...], node: _ParsedNode = parsed_node) -> list[s dependency for dependency in proof_dependencies if dependency not in dependencies ) metadata = parsed_node.metadata + if metadata.get("catalog") is not None: + if ( + metadata.get("statement") == _FORMALIZED + or metadata.get("proof") == _FORMALIZED + ) and not declaration_names(metadata.get("lean", "")): + issues.append( + f"{parsed_node.id}: formalized module catalog must list exact " + "compiled names in 'lean'" + ) + if not _catalog_has_local_ledger(parsed_node, blueprint): + issues.append( + f"{parsed_node.id}: module catalog must link a declaration ledger " + "under blueprint/sources from its '## Sources' section" + ) nodes[parsed_node.id] = Node( id=parsed_node.id, title=parsed_node.title, @@ -232,6 +286,7 @@ def resolve(targets: tuple[str, ...], node: _ParsedNode = parsed_node) -> list[s proof_dependencies=tuple(proof_dependencies), kind="article", declaration=metadata.get("declaration"), + catalog=metadata.get("catalog"), lean=metadata.get("lean"), statement_formalized=metadata.get("statement") == _FORMALIZED, statement_retracted=metadata.get("statement") == _RETRACTED, @@ -247,8 +302,11 @@ def resolve(targets: tuple[str, ...], node: _ParsedNode = parsed_node) -> list[s depth=_article_depth(parsed_node.id, parents), article_id=metadata.get("article_id"), source_sha256=source_hashes[parsed_node.id], + summary=parsed_node.summary, + area=metadata.get("area"), ) + _apply_atlas_manifest(blueprint, nodes, issues) if not issues: issues.extend(_find_cycles(nodes)) if not issues: @@ -258,6 +316,84 @@ def resolve(targets: tuple[str, ...], node: _ParsedNode = parsed_node) -> list[s return Graph(blueprint_dir=blueprint, nodes=nodes, open_statements=open_statements) +def _apply_atlas_manifest( + blueprint: Path, + nodes: dict[str, Node], + issues: list[str], +) -> None: + """Apply an optional authored taxonomy without coupling it to file layout.""" + path = blueprint / "atlas.json" + if path.is_symlink(): + issues.append("atlas.json: taxonomy must be a regular file inside the blueprint") + return + if not path.exists(): + return + if not path.is_file(): + issues.append("atlas.json: taxonomy must be a regular file inside the blueprint") + return + try: + raw = path.read_bytes() + except OSError as error: + issues.append(f"atlas.json: cannot read taxonomy: {error}") + return + if len(raw) > _MAX_ATLAS_BYTES: + issues.append(f"atlas.json: exceeds {_MAX_ATLAS_BYTES} bytes") + return + try: + payload = json.loads(raw) + except (UnicodeDecodeError, json.JSONDecodeError) as error: + issues.append(f"atlas.json: invalid JSON: {error}") + return + if not isinstance(payload, dict) or payload.get("schema") != ATLAS_SCHEMA: + issues.append(f"atlas.json: schema must be {ATLAS_SCHEMA!r}") + return + areas = payload.get("areas") + if not isinstance(areas, dict): + issues.append("atlas.json: 'areas' must be an object") + return + assigned: dict[str, str] = {} + for area, node_ids in areas.items(): + if not isinstance(area, str) or not area.strip() or not isinstance(node_ids, list): + issues.append("atlas.json: each area must be a non-empty string mapped to an array") + continue + for node_id in node_ids: + if not isinstance(node_id, str) or node_id not in nodes: + issues.append(f"atlas.json: unknown roadmap node {node_id!r}") + continue + previous = assigned.get(node_id) + if previous is not None: + issues.append(f"atlas.json: node {node_id!r} belongs to both {previous!r} and {area!r}") + continue + authored = nodes[node_id].area + if authored is not None and authored != area: + issues.append( + f"atlas.json: node {node_id!r} conflicts with its frontmatter area {authored!r}" + ) + continue + assigned[node_id] = area + for node_id, area in assigned.items(): + nodes[node_id] = replace(nodes[node_id], area=area) + + +def _catalog_has_local_ledger(node: _ParsedNode, blueprint: Path) -> bool: + sources = (blueprint / "sources").resolve() + for target in node.source_targets: + split = urlsplit(target) + if split.scheme or split.netloc or split.query or not split.path: + continue + path = Path(unquote(split.path)) + if path.is_absolute(): + continue + try: + candidate = (node.path.parent / path).resolve() + candidate.relative_to(sources) + except (OSError, ValueError): + continue + if candidate.is_file(): + return True + return False + + def _discover_nodes(blueprint: Path) -> tuple[list[_NodeSource], list[str]]: roadmap_root = blueprint / "roadmap" if not roadmap_root.is_dir(): @@ -441,10 +577,58 @@ def _parse_node(node_id: str, path: Path, text: str) -> tuple[_ParsedNode | None tuple(targets[_PROOF_SECTION]), tuple(targets[_SOURCES_SECTION]), metadata, + _extract_summary(body), ) return parsed, [] +def _extract_summary(body: str, *, limit: int = 420) -> str | None: + """Return the first reader-facing prose paragraph from a roadmap article.""" + paragraph: list[str] = [] + excluded = False + fence: tuple[str, int] | None = None + for raw in body.splitlines(): + fence_match = _FENCE.match(raw) + if fence_match: + marker = fence_match.group(1) + if fence is None: + fence = (marker[0], len(marker)) + elif marker[0] == fence[0] and len(marker) >= fence[1]: + fence = None + continue + if fence is not None: + continue + heading = _HEADING.match(raw) + if heading: + if paragraph: + break + excluded = len(heading.group(1)) == 2 and heading.group(2).strip().casefold() in { + _STATEMENT_SECTION, + _PROOF_SECTION, + _SOURCES_SECTION, + } + continue + text = raw.strip() + if not text: + if paragraph: + break + continue + if excluded or text.startswith(("- ", "* ", "+ ", "> ", "|", "$$", "\\[", " tuple[dict[str, str], int, list[str]]: if not lines or lines[0].strip() != "---": return {}, 0, [] @@ -480,6 +664,13 @@ def _parse_frontmatter(node_id: str, lines: list[str]) -> tuple[dict[str, str], continue metadata[key] = value + if "catalog" in metadata: + for key in sorted(_CATALOG_DECLARATION_KEYS.intersection(metadata)): + issues.append( + f"{node_id}: 'catalog' cannot be combined with declaration-specific " + f"frontmatter key {key!r}" + ) + if metadata.get("statement") == _RETRACTED: if "lean" not in metadata: issues.append( @@ -496,7 +687,11 @@ def _parse_frontmatter(node_id: str, lines: list[str]) -> tuple[dict[str, str], if metadata.get("proof") == _FORMALIZED and metadata.get("statement") not in {_FORMALIZED, _RETRACTED}: issues.append(f"{node_id}: proof: formalized needs statement: formalized") formalized = [key for key in ("statement", "proof") if metadata.get(key) == _FORMALIZED] - if formalized and not declaration_names(metadata.get("lean", "")): + if ( + formalized + and metadata.get("catalog") is None + and not declaration_names(metadata.get("lean", "")) + ): issues.append(f"{node_id}: {formalized[0]}: formalized needs the lean: declaration that formalizes it") return metadata, end + 1, issues @@ -509,6 +704,10 @@ def _normalize_value(node_id: str, line_number: int, key: str, value: str) -> tu if not ARTICLE_ID_PATTERN.fullmatch(value): return value, f"{location}: malformed article_id {value!r}" return value, None + if key == "catalog": + if folded != "module": + return value, f"{location}: 'catalog' accepts only 'module'" + return folded, None if key == "statement": if folded not in {_FORMALIZED, _RETRACTED}: return value, ( diff --git a/autoform_cli/graph_pages.py b/autoform_cli/graph_pages.py index a5debd82..c47e25ad 100644 --- a/autoform_cli/graph_pages.py +++ b/autoform_cli/graph_pages.py @@ -1,23 +1,24 @@ -"""Publish scalable graph projections beside the textbook blueprint. +"""Publish scalable dependency-explorer projections beside the textbook. One Markdown DAG supports several reading scales: chapters collapsed into a -project map, declarations within one chapter with external chapters collapsed -to boundaries, a theorem's one-hop neighborhood, and an optional full graph. -Every projection links back to the same book anchors and never becomes another -source of graph state. +project overview, declarations within one chapter with external chapters +collapsed to boundaries, nested scopes, and the full graph. Every projection +uses the same explorer, links back to the same book anchors, and never becomes +another source of graph state. """ from __future__ import annotations -from collections.abc import Callable, Mapping +from collections.abc import Callable, Iterable, Mapping +from dataclasses import replace from pathlib import Path +from urllib.parse import quote -from . import mermaid +from . import dag_viewer, mermaid from .graph import Graph from .graph_views import ( GraphView, chapter_view, - focus_views, full_view, group_nodes, project_view, @@ -25,8 +26,7 @@ ) from .status import NodeStatus - -NodeLinks = Callable[[Path], Mapping[str, str]] +NodeLinks = Callable[[Path, Iterable[str]], Mapping[str, str]] def write_graph_pages( @@ -36,7 +36,7 @@ def write_graph_pages( *, node_links: NodeLinks, ) -> tuple[Path, ...]: - """Write project, chapter, local, and full graph pages. + """Write project, chapter, nested-scope, and shared full-explorer pages. ``node_links`` resolves theorem ids to their published textbook anchors for each generated page. Keeping that callback in the site renderer avoids @@ -44,9 +44,9 @@ def write_graph_pages( """ destination = Path(destination).resolve() groups = group_nodes(graph) - local_views = focus_views(graph, statuses) project_page = destination / "dependencies.md" full_page = destination / "dependencies/full.md" + search_index = destination / "dependencies/index.json" chapter_pages = {group: destination / "dependencies/chapters" / f"{group or 'roadmap'}.md" for group in groups} scope_maps = scope_views(graph, statuses) containers = list(scope_maps) @@ -61,13 +61,32 @@ def write_graph_pages( for node_id in containers } scope_pages["roadmap"] = project_page - article_groups = {node_id: group for group, node_ids in groups.items() for node_id in node_ids} - focus_pages = {node_id: destination / "dependencies/nodes" / f"{node_id}.md" for node_id in article_groups} written: list[Path] = [] + complete = full_view(graph, statuses) + context_links: dict[str, str] = {} + for node in complete.nodes: + target = ( + chapter_pages["roadmap"] + if node.id == "roadmap" and "roadmap" in chapter_pages + else scope_pages.get(node.id) + ) + if target is None: + parent = graph.nodes[node.id].parent or "roadmap" + target = ( + chapter_pages["roadmap"] + if parent == "roadmap" and "roadmap" in chapter_pages + else scope_pages.get(parent, project_page) + ) + context = _published_link(target, search_index) + if node.id not in scope_pages: + context += f"#node={quote(node.id, safe='')}" + context_links[node.id] = context + dag_viewer.write_search_index(search_index, complete, context_links=context_links) + project = project_view(graph, statuses) project_item_count = sum(len(node_ids) for node_ids in groups.values()) - project_book_links = node_links(project_page) + project_book_links = node_links(project_page, _article_link_ids(project)) project_links = { view_node.id: ( _published_link( @@ -86,19 +105,26 @@ def write_graph_pages( _write_page( project_page, view=project, - statuses=statuses, + statuses=_selected_statuses(graph, statuses, project), links=project_links, - heading="Dependency maps", + heading="Mathematics atlas", lead=( - f"{project_item_count} item{'s' if project_item_count != 1 else ''} across " + f"{project_item_count} roadmap entr{'y' if project_item_count == 1 else 'ies'} across " f"{len(groups)} chapter{'s' if len(groups) != 1 else ''}." ), + navigation="", + site_root=destination, + search_href=_search_index_link(search_index, project_page), + breadcrumbs=( + ("Book", _published_link(destination / "README.md", project_page)), + ("All mathematics", None), + ), ) ) for group, chapter_page in chapter_pages.items(): view = scope_maps[group] if group in scope_maps else chapter_view(graph, statuses, group) - links = dict(node_links(chapter_page)) + links = dict(node_links(chapter_page, _article_link_ids(view))) for node in view.nodes: if node.kind == "boundary": external = node.id.removeprefix("boundary:") @@ -113,22 +139,30 @@ def write_graph_pages( else destination / "roadmap" / group / "README.md" ) navigation = _navigation( - ("Project map", _markdown_link(project_page, chapter_page)), - ("Full theorem DAG", _markdown_link(full_page, chapter_page)), + ("Dependency explorer", _markdown_link(project_page, chapter_page)), ("Open textbook chapter", _markdown_link(book_page, chapter_page)), ) written.append( _write_page( chapter_page, view=view, - statuses=_selected_statuses(statuses, view), + statuses=_selected_statuses(graph, statuses, view), links=links, - heading=view.title, + heading=_dependency_heading(view), lead=( - f"This map contains the {len(groups[group])} decomposed items in this chapter. " - "Dashed chapter boxes stand for external prerequisites or dependents." + f"This view contains {len(groups[group])} roadmap entries in this chapter. " + "Collapsed chapter nodes stand for external prerequisites or dependents." ), navigation=navigation, + site_root=destination, + search_href=_search_index_link(search_index, chapter_page), + breadcrumbs=_scope_breadcrumbs( + graph, + group, + page=chapter_page, + scope_pages=scope_pages, + project_page=project_page, + ), ) ) @@ -137,7 +171,7 @@ def write_graph_pages( continue scope_page = scope_pages[scope] view = scope_maps[scope] - links = dict(node_links(scope_page)) + links = dict(node_links(scope_page, _article_link_ids(view))) for node in view.nodes: if node.kind == "scope": nested = node.id.removeprefix("scope:") @@ -151,68 +185,97 @@ def write_graph_pages( _write_page( scope_page, view=view, - statuses=_selected_statuses(statuses, view), + statuses=_selected_statuses(graph, statuses, view), links=links, - heading=view.title, + heading=_dependency_heading(view), lead=( - "This map shows the container's direct articles. Nested containers " + "This view shows the container's direct articles. Nested containers " "are collapsed and clickable; dependency edges are rolled up from their leaves." ), navigation=_navigation( - ("Parent map", _markdown_link(parent_page, scope_page)), - ("Full theorem DAG", _markdown_link(full_page, scope_page)), + ("Parent view", _markdown_link(parent_page, scope_page)), + ("Dependency explorer", _markdown_link(project_page, scope_page)), + ), + site_root=destination, + search_href=_search_index_link(search_index, scope_page), + breadcrumbs=_scope_breadcrumbs( + graph, + scope, + page=scope_page, + scope_pages=scope_pages, + project_page=project_page, ), ) ) - complete = full_view(graph, statuses) + # Keep the old full route as a compatibility shell, but never fit every + # leaf into one unreadable canvas. Its global index redirects legacy + # ``#node=`` links into the nearest hierarchical scope. + full_project_book_links = node_links(full_page, _article_link_ids(project)) + full_project_links = { + view_node.id: ( + _published_link( + chapter_pages.get( + view_node.id.removeprefix("scope:"), + scope_pages[view_node.id.removeprefix("scope:")], + ), + full_page, + ) + if view_node.kind == "scope" + else full_project_book_links[view_node.id] + ) + for view_node in project.nodes + } written.append( _write_page( full_page, - view=complete, - statuses=statuses, - links=node_links(full_page), - heading=complete.title, + view=project, + statuses=_selected_statuses(graph, statuses, project), + links=full_project_links, + heading="Mathematics atlas", lead=( - f"{len(graph.nodes)} nodes · {graph.edge_count} dependencies. Arrows point from a " - "prerequisite to what depends on it; dashed arrows are needed only by proofs." + f"Browse {len(graph.nodes)} roadmap entries without flattening them into one canvas. " + "Search jumps directly to the relevant chapter or nested scope." + ), + navigation=_navigation( + ("Dependency explorer", _markdown_link(project_page, full_page)), + ("Download search index", search_index.name), + ), + site_root=destination, + search_href=_search_index_link(search_index, full_page), + breadcrumbs=( + ("Book", _published_link(destination / "README.md", full_page)), + ("All mathematics", _published_link(project_page, full_page)), + ("Explorer", None), ), - navigation=_navigation(("Project map", _markdown_link(project_page, full_page))), ) ) - for node_id, focus_page in focus_pages.items(): - view = local_views[node_id] - parent = graph.nodes[node_id].parent - chapter_page = scope_pages.get(parent or article_groups[node_id], chapter_pages[article_groups[node_id]]) - focus_links = node_links(focus_page) - statement_href = _markdown_document_link(focus_links[node_id]) - navigation = _navigation( - ("Project map", _markdown_link(project_page, focus_page)), - ("Chapter map", _markdown_link(chapter_page, focus_page)), - ("Full theorem DAG", _markdown_link(full_page, focus_page)), - ("Open textbook statement", statement_href), - ) - written.append( - _write_page( - focus_page, - view=view, - statuses=_selected_statuses(statuses, view), - links=focus_links, - heading=view.title, - lead=( - "This local map shows one dependency hop in either direction. " - "The highlighted item is the current focus." - ), - navigation=navigation, - ) - ) - return tuple(written) -def focus_page_path(destination: str | Path, node_id: str) -> Path: - """Return the generated local-context page for a theorem node.""" - return Path(destination).resolve() / "dependencies/nodes" / f"{node_id}.md" +def focus_page_path(destination: str | Path, node_id: str, *, parent: str | None = None) -> Path: + """Return the smallest published explorer scope that contains a node.""" + destination = Path(destination).resolve() + scope = parent if parent is not None else node_id.rpartition("/")[0] + if scope == "": + return destination / "dependencies.md" + if scope == "roadmap": + return destination / "dependencies/chapters/roadmap.md" + if "/" not in scope: + return destination / "dependencies/chapters" / f"{scope}.md" + return destination / "dependencies/scopes" / f"{scope}.md" + + +def focus_page_href( + destination: str | Path, + node_id: str, + page: str | Path, + *, + parent: str | None = None, +) -> str: + """Return a published explorer link with durable node focus in the hash.""" + target = focus_page_path(destination, node_id, parent=parent) + return f"{mermaid.relative_link(target, Path(page), '.html')}#node={quote(node_id, safe='')}" def _write_page( @@ -223,14 +286,41 @@ def _write_page( links: Mapping[str, str], heading: str, lead: str, + site_root: Path, + search_href: str, + breadcrumbs: tuple[tuple[str, str | None], ...], navigation: str = "", extra: str = "", ) -> Path: - diagram = mermaid.render_view_diagram(view, links=dict(links), include_classdefs=False) + # Size used to pick between a Mermaid diagram and the Canvas explorer. + # Keeping every projection on one payload-and-host path gives readers one + # interaction model and prevents the two renderers from drifting apart. + payload = page.with_suffix(".json") + dag_viewer.write_payload( + payload, + replace(view, title=heading), + links=links, + breadcrumbs=breadcrumbs, + ) + explorer = dag_viewer.render_container( + payload.name, + script_href=_viewer_script_link(page, site_root), + fallback_links=( + (node.title, links[node.id]) + for node in view.nodes[:50] + if links.get(node.id) + ), + fallback_total=len(view.nodes), + search_href=search_href, + ) sections = [ "---", "kind: graph", f"graph_view: {view.kind}", + "hide:", + " - navigation", + " - toc", + " - footer", "---", "", f"# {heading}", @@ -239,9 +329,9 @@ def _write_page( if navigation: sections.extend([navigation, ""]) # The legend rides on the lead sentence rather than sitting under the - # diagram: it answers a question the reader asks once, not on every page. + # explorer: it answers a question the reader asks once, not on every page. tip = mermaid.render_legend_tip(statuses) - sections.extend([f"{lead} {tip}".rstrip(), "", diagram, ""]) + sections.extend([f"{lead} {tip}".rstrip(), "", explorer, ""]) if extra: sections.extend([extra, ""]) page.parent.mkdir(parents=True, exist_ok=True) @@ -250,10 +340,34 @@ def _write_page( def _selected_statuses( + graph: Graph, statuses: dict[str, NodeStatus], view: GraphView, ) -> dict[str, NodeStatus]: - return {node_id: statuses[node_id] for node_id in view.member_ids} + containers = frozenset( + node.parent for node in graph.nodes.values() if node.parent is not None + ) + return { + node_id: statuses[node_id] + for node_id in view.member_ids + if node_id not in containers and graph.nodes[node_id].formalizable + } + + +def _dependency_heading(view: GraphView) -> str: + """Name a projected explorer view without carrying over Mermaid-era copy.""" + subject = view.title.removesuffix(" dependency map") + return f"{subject} {'dependencies' if view.edges else 'knowledge map'}" + + +def _article_link_ids(view: GraphView) -> tuple[str, ...]: + """Return only view nodes whose links come from published articles. + + Scope and boundary links are derived locally by this module. Asking the + renderer for every graph node on every scope page made a repository-wide + wiki spend quadratic time constructing links that the projection never used. + """ + return tuple(node.id for node in view.nodes if node.kind == "node") def _navigation(*items: tuple[str, str]) -> str: @@ -268,15 +382,45 @@ def _published_link(target: Path, page: Path) -> str: return mermaid.relative_link(target, page, ".html") -def _markdown_document_link(href: str) -> str: - """Turn a raw published-page URL back into a link MkDocs can validate.""" - path, separator, fragment = href.partition("#") - document = Path(path) - if document.name == "index.html": - document = document.parent / "README.md" - elif document.suffix == ".html": - document = document.with_suffix(".md") - return f"{document.as_posix()}{separator}{fragment}" +def _viewer_script_link(page: Path, site_root: Path) -> str: + """Link the viewer asset from an explicit publication root.""" + + return mermaid.relative_link( + site_root / "javascripts/blueprint-dag.js", + page, + ".js", + ) + + +def _search_index_link(search_index: Path, page: Path) -> str: + return mermaid.relative_link(search_index, page, ".json") + + +def _scope_breadcrumbs( + graph: Graph, + scope: str, + *, + page: Path, + scope_pages: Mapping[str, Path], + project_page: Path, +) -> tuple[tuple[str, str | None], ...]: + lineage: list[str] = [] + current: str | None = scope + while current and current != "roadmap": + lineage.append(current) + current = graph.nodes[current].parent if current in graph.nodes else None + items: list[tuple[str, str | None]] = [ + ("Book", _published_link(project_page.parent / "README.md", page)), + ("All mathematics", _published_link(project_page, page)), + ] + for node_id in reversed(lineage): + target = scope_pages.get(node_id) + label = graph.nodes[node_id].title if node_id in graph.nodes else node_id + items.append((label, _published_link(target, page) if target and target != page else None)) + if not lineage: + label = graph.nodes[scope].title if scope in graph.nodes else scope.replace("-", " ").title() + items.append((label, None)) + return tuple(items) -__all__ = ["focus_page_path", "write_graph_pages"] +__all__ = ["focus_page_href", "focus_page_path", "write_graph_pages"] diff --git a/autoform_cli/graph_views.py b/autoform_cli/graph_views.py index 305f553b..19cbb623 100644 --- a/autoform_cli/graph_views.py +++ b/autoform_cli/graph_views.py @@ -24,6 +24,7 @@ _ScopedRelation = tuple[str, str, bool, str | None, str | None] _H1 = re.compile(r"^ {0,3}#[ \t]+(.+?)[ \t]*#*[ \t]*$") +INVENTORY_CHECKED_STATUS = "inventory_checked" @dataclass(frozen=True, slots=True) @@ -38,6 +39,11 @@ class ViewNode: declaration: str | None = None status_key: str | None = None focus: bool = False + catalog: str | None = None + summary: str | None = None + lean: str | None = None + area: str | None = None + internal_dependency_count: int = 0 @property def item_count(self) -> int: @@ -69,6 +75,7 @@ class GraphView: scope: str | None = None focus: str | None = None radius: int | None = None + summary: str | None = None @property def member_ids(self) -> tuple[str, ...]: @@ -119,6 +126,7 @@ def group_title(graph: Graph, group: str) -> str: def project_view(graph: Graph, statuses: dict[str, NodeStatus]) -> GraphView: """Collapse every publication chapter to one project-map node.""" children = _containment_children(graph) + internal_counts = _internal_dependency_counts(graph, children) grouped = _group_nodes(graph, children) edges = _project_edges(graph, children) required_scopes = {endpoint.removeprefix("scope:") for edge in edges for endpoint in (edge.source, edge.target)} @@ -129,11 +137,25 @@ def project_view(graph: Graph, statuses: dict[str, NodeStatus]) -> GraphView: title=group_title(graph, group), kind="scope", members=grouped.get(group, ()), - status_counts=_status_counts(grouped.get(group, ()), statuses), + status_counts=_status_counts(graph, grouped.get(group, ()), statuses), + status_key=_rollup_status_key(graph, grouped.get(group, ()), statuses), + summary=graph.nodes[group].summary if group in graph.nodes else None, + area=graph.nodes[group].area if group in graph.nodes else None, + internal_dependency_count=( + internal_counts[group] + if group in internal_counts + else _dependency_count_within(graph, grouped.get(group, ())) + ), ) for group in scopes ) - return GraphView(kind="project", title="Project dependency map", nodes=nodes, edges=edges) + return GraphView( + kind="project", + title="Project dependency map", + nodes=nodes, + edges=edges, + summary=graph.nodes["roadmap"].summary if "roadmap" in graph.nodes else None, + ) def chapter_view(graph: Graph, statuses: dict[str, NodeStatus], group: str) -> GraphView: @@ -173,7 +195,8 @@ def chapter_view(graph: Graph, statuses: dict[str, NodeStatus], group: str) -> G title=group_title(graph, external), kind="boundary", members=tuple(sorted(external_members)), - status_counts=_status_counts(external_members, statuses), + status_counts=_status_counts(graph, external_members, statuses), + status_key=_rollup_status_key(graph, external_members, statuses), ) for external, external_members in sorted(boundaries.items()) ) @@ -183,6 +206,7 @@ def chapter_view(graph: Graph, statuses: dict[str, NodeStatus], group: str) -> G nodes=tuple(nodes), edges=_edges(edge_counts), scope=group, + summary=graph.nodes[group].summary if group in graph.nodes else None, ) @@ -200,6 +224,7 @@ def scope_view( containment hierarchy without creating another graph representation. """ children = _containment_children(graph) + internal_counts = _internal_dependency_counts(graph, children) if scope not in graph.nodes or scope not in children: raise KeyError(f"unknown blueprint scope: {scope}") relations = ( @@ -211,6 +236,7 @@ def scope_view( statuses, scope, children=children, + internal_counts=internal_counts, relations=relations, top_scope=lambda node_id: _top_scope(graph, node_id, children), include_external=include_external, @@ -231,6 +257,7 @@ def scope_views( files each relation under only the containers that enclose an endpoint. """ children = _containment_children(graph) + internal_counts = _internal_dependency_counts(graph, children) enclosing: dict[str, dict[str, str]] = {} top_scopes: dict[str, str] = {} @@ -262,6 +289,7 @@ def top_scope(node_id: str) -> str: statuses, scope, children=children, + internal_counts=internal_counts, relations=relations.get(scope, ()), top_scope=top_scope, include_external=include_external, @@ -277,6 +305,7 @@ def _scope_view( scope: str, *, children: dict[str, tuple[str, ...]], + internal_counts: dict[str, int], relations: Iterable[_ScopedRelation], top_scope: Callable[[str], str], include_external: bool, @@ -293,7 +322,11 @@ def _scope_view( title=article.title, kind="scope", members=members[child], - status_counts=_status_counts(members[child], statuses), + status_counts=_status_counts(graph, members[child], statuses), + status_key=_rollup_status_key(graph, members[child], statuses), + summary=article.summary, + area=article.area, + internal_dependency_count=internal_counts.get(child, 0), ) ) else: @@ -330,7 +363,8 @@ def _scope_view( title=group_title(graph, external), kind="boundary", members=tuple(sorted(external_members)), - status_counts=_status_counts(external_members, statuses), + status_counts=_status_counts(graph, external_members, statuses), + status_key=_rollup_status_key(graph, external_members, statuses), ) ) return GraphView( @@ -339,6 +373,7 @@ def _scope_view( nodes=tuple(nodes), edges=_edges(edge_counts), scope=scope, + summary=graph.nodes[scope].summary, ) @@ -372,10 +407,9 @@ def focus_views( ) -> dict[str, GraphView]: """Build every local view while sharing the graph-wide indexes. - Static publication writes one focus page per theorem. Recomputing adjacency - and topological order for every page becomes quadratic on a large book, so - the bulk path constructs both once and keeps each page proportional to its - local neighborhood. + Programmatic consumers that need all local views can avoid recomputing + adjacency and topological order for every node. Static publication uses the + shared hash-addressable explorer instead of emitting one HTML page per node. """ if radius < 0: raise ValueError("focus radius must be non-negative") @@ -430,8 +464,13 @@ def _focus_view( members=node.members, status_counts=node.status_counts, declaration=node.declaration, + catalog=node.catalog, status_key=node.status_key, focus=node.id == node_id, + summary=node.summary, + lean=node.lean, + area=node.area, + internal_dependency_count=node.internal_dependency_count, ) for node in view.nodes ) @@ -442,13 +481,39 @@ def _focus_view( edges=view.edges, focus=node_id, radius=radius, + summary=graph.nodes[node_id].summary, ) def full_view(graph: Graph, statuses: dict[str, NodeStatus]) -> GraphView: - """Present the complete fine-grained theorem DAG through the view API.""" + """Present every article and dependency, with container status rolled up.""" view = _node_view(graph, statuses, graph.nodes) - return GraphView(kind="full", title="Full theorem dependency graph", nodes=view.nodes, edges=view.edges) + children = _containment_children(graph) + internal_counts = _internal_dependency_counts(graph, children) + descendants = _leaf_descendant_map(graph, children) + nodes = tuple( + ViewNode( + id=node.id, + title=node.title, + kind="scope", + members=(node.id, *descendants[node.id]), + status_counts=_status_counts(graph, descendants[node.id], statuses), + status_key=_rollup_status_key(graph, descendants[node.id], statuses), + summary=graph.nodes[node.id].summary, + area=graph.nodes[node.id].area, + internal_dependency_count=internal_counts.get(node.id, 0), + ) + if node.id in children + else node + for node in view.nodes + ) + return GraphView( + kind="full", + title="Full dependency graph", + nodes=nodes, + edges=view.edges, + summary=graph.nodes["roadmap"].summary if "roadmap" in graph.nodes else None, + ) def _node_view( @@ -516,27 +581,84 @@ def _edges(counts: dict[tuple[str, str], list[int]]) -> tuple[ViewEdge, ...]: def _theorem_node(node: Node, node_status: NodeStatus) -> ViewNode: + display_status = ( + INVENTORY_CHECKED_STATUS + if node.catalog == "module" and node_status.fully_proved + else node_status.key + ) return ViewNode( id=node.id, title=node.title, kind="node", members=(node.id,), - status_counts=((node_status.key, 1),), + status_counts=((display_status, 1),), declaration=node.declaration, - status_key=node_status.key, + catalog=node.catalog, + # A checked inventory is deliberately neutral: it records source + # accounting, not completion of a mathematical target. + status_key="planned" if display_status == INVENTORY_CHECKED_STATUS else display_status, + summary=node.summary, + lean=node.lean, + area=node.area, ) def _status_counts( + graph: Graph, node_ids: Iterable[str], statuses: dict[str, NodeStatus], ) -> tuple[tuple[str, int], ...]: counts = {state.key: 0 for state in STATES} + inventories = 0 for node_id in node_ids: - counts[statuses[node_id].key] += 1 - return tuple((state.key, counts[state.key]) for state in STATES if counts[state.key]) + node_status = statuses[node_id] + if graph.nodes[node_id].catalog == "module" and node_status.fully_proved: + inventories += 1 + else: + counts[node_status.key] += 1 + state_counts = tuple( + (state.key, counts[state.key]) for state in STATES if counts[state.key] + ) + if inventories: + return (*state_counts, (INVENTORY_CHECKED_STATUS, inventories)) + return state_counts +def _internal_dependency_counts( + graph: Graph, + children: dict[str, tuple[str, ...]], +) -> dict[str, int]: + """Count typed relations inside every container in one graph-wide pass.""" + counts = {scope: 0 for scope in children} + enclosing = {node_id: set(_enclosing_scopes(graph, node_id)) for node_id in graph.nodes} + for node_id in children: + enclosing[node_id].add(node_id) + for source, target, _proof_only in _relations(graph): + for scope in enclosing[source].intersection(enclosing[target]): + counts[scope] += 1 + return counts + + +def _dependency_count_within(graph: Graph, node_ids: Iterable[str]) -> int: + selected = frozenset(node_ids) + return sum( + dependency in selected + for node_id in selected + for dependency in graph.nodes[node_id].dependencies + ) + + +def _rollup_status_key( + graph: Graph, + node_ids: Iterable[str], + statuses: dict[str, NodeStatus], +) -> str: + """Use the least-complete descendant as a container's honest status.""" + counts = _status_counts(graph, node_ids, statuses) + target_counts = tuple( + (key, count) for key, count in counts if key != INVENTORY_CHECKED_STATUS + ) + return target_counts[-1][0] if target_counts else "planned" def _scope_node_id(group: str) -> str: return f"scope:{group or 'roadmap'}" @@ -616,6 +738,30 @@ def _containment_children(graph: Graph) -> dict[str, tuple[str, ...]]: return {parent: tuple(node_ids) for parent, node_ids in children.items()} +def _leaf_descendant_map( + graph: Graph, + children: dict[str, tuple[str, ...]], +) -> dict[str, tuple[str, ...]]: + """Compute every containment rollup once for full-graph rendering.""" + descendants: dict[str, tuple[str, ...]] = {} + + def visit(node_id: str) -> tuple[str, ...]: + if node_id in descendants: + return descendants[node_id] + contained = children.get(node_id, ()) + result = ( + tuple(leaf for child in contained for leaf in visit(child)) + if contained + else (node_id,) + ) + descendants[node_id] = result + return result + + for node_id in graph.nodes: + visit(node_id) + return descendants + + __all__ = [ "GraphView", "ViewEdge", diff --git a/autoform_cli/lean.py b/autoform_cli/lean.py index 8fd81fb6..4a500e85 100644 --- a/autoform_cli/lean.py +++ b/autoform_cli/lean.py @@ -38,11 +38,13 @@ ) _NAMESPACE = re.compile(r"^\s*namespace\s+(.+)$") -_SECTION = re.compile(r"^\s*section\b\s*(\S*)") +_SECTION = re.compile( + r"^\s*(?:(?:public|private|noncomputable|unsafe|local)\s+)*section\b\s*(\S*)" +) _END = re.compile(r"^\s*end\b\s*(\S*)") _DECLARATION = re.compile( r"^\s*(?:@\[[^\]]*\]\s*)*" - r"(?:(?:private|protected|noncomputable|partial|unsafe|scoped|local)\s+)*" + r"(?:(?:public|private|protected|noncomputable|partial|unsafe|scoped|local)\s+)*" r"(theorem|lemma|def|abbrev|instance|structure|class|inductive|opaque|axiom|irreducible_def)\s+(.+)$" ) _IGNORED_DIRECTORIES = frozenset( @@ -117,9 +119,18 @@ class BoundProjectSources: tree: BoundDirectoryTree excluded: tuple[PurePosixPath, ...] - def capture(self) -> IndexedSourceSnapshot: + def capture( + self, + *, + names: Iterable[str] | None = None, + ) -> IndexedSourceSnapshot: snapshot = self.tree.capture() - return _indexed_source_snapshot(self.root, snapshot, self.excluded) + return _indexed_source_snapshot( + self.root, + snapshot, + self.excluded, + names=names, + ) def verify(self) -> None: self.tree.verify() @@ -138,8 +149,6 @@ def __init__(self, reason: str) -> None: for character in reason ) ) - - def index_failure_message(error: OSError) -> str: """Describe an indexing failure without exposing host paths.""" @@ -149,7 +158,10 @@ def index_failure_message(error: OSError) -> str: def index_project( - root: str | Path, *, exclude_roots: Iterable[str | Path] = () + root: str | Path, + *, + exclude_roots: Iterable[str | Path] = (), + names: Iterable[str] | None = None, ) -> SourceIndex: """Scan ``*.lean`` beneath *root* and index declarations by full name.""" requested_root = directory_binding.lexical_absolute_path(root) @@ -164,6 +176,7 @@ def index_project( return snapshot_project_sources( root_path, exclude_roots=remapped_exclusions, + names=names, ).index @@ -235,6 +248,7 @@ def snapshot_project_sources( *, exclude_roots: Iterable[str | Path] = (), limits: TreeCaptureLimits = TreeCaptureLimits(), + names: Iterable[str] | None = None, ) -> IndexedSourceSnapshot: """Read each Lean source once and derive its index and revision together. @@ -243,6 +257,7 @@ def snapshot_project_sources( """ exclusions = tuple(exclude_roots) + requested_names = None if names is None else tuple(names) changed: TreeChangedError | None = None for attempt in range(_SNAPSHOT_ATTEMPTS): if attempt: @@ -253,7 +268,7 @@ def snapshot_project_sources( exclude_roots=exclusions, limits=limits, ) as bound: - return bound.capture() + return bound.capture(names=requested_names) except TreeChangedError as error: changed = error except TreeSnapshotError as error: @@ -443,7 +458,9 @@ def _lean_tree_selection( if _is_managed_output_manifest_name(path.name) else None ), - record_omitted=False, + # Omitted marker entries let the immutable snapshot classify nested Git + # checkouts without consulting live pathnames after capture. + record_omitted=True, limits=limits, opaque_markers=( # A nested Git checkout is another source tree. Treat the @@ -511,6 +528,8 @@ def _indexed_source_snapshot( root: Path, snapshot: TreeSnapshot, excluded: tuple[PurePosixPath, ...], + *, + names: Iterable[str] | None = None, ) -> IndexedSourceSnapshot: managed_output_manifests: dict[ PurePosixPath, @@ -539,6 +558,13 @@ def add_manifest(relative: str, kind: str, data: bytes | None = None) -> None: for relative in snapshot.opaque_directories if relative } + ignored_roots.update( + marker.parent + for relative, kind in snapshot.omitted + if kind in {"directory", "file"} + and len((marker := PurePosixPath(relative)).parts) > 1 + and unicodedata.normalize("NFC", marker.name).casefold() == ".git" + ) for parent in sorted( managed_output_manifests, key=lambda path: (len(path.parts), path.as_posix()), @@ -561,8 +587,12 @@ def in_ignored_root(relative_text: str) -> bool: # any other ``.lean`` link, live or dangling, is refused. tolerated_links = frozenset( relative - for relative, _target in snapshot.symlinks - if PurePosixPath(relative).suffix.casefold() == ".lean" + for relative, kind in ( + *((relative, "symlink") for relative, _target in snapshot.symlinks), + *snapshot.omitted, + ) + if kind == "symlink" + and PurePosixPath(relative).suffix.casefold() == ".lean" and not in_ignored_root(relative) and PurePosixPath(relative).name.startswith(".#") ) @@ -581,6 +611,11 @@ def in_ignored_root(relative_text: str) -> bool: line_counts: dict[Path, int] = {} source_files: list[tuple[Path, bytes]] = [] digest = hashlib.sha256(b"autoform-lean-source-index/v1\0") + wanted_short = ( + None + if names is None + else frozenset(_short_name(name) for name in names) + ) for relative_text, data in snapshot.files: relative = PurePosixPath(relative_text) if relative.suffix.casefold() != ".lean" or _lean_path_is_excluded( @@ -598,6 +633,8 @@ def in_ignored_root(relative_text: str) -> bool: except UnicodeError: continue line_counts[relative_path] = len(text.splitlines()) + if wanted_short is not None and not _may_declare(text, wanted_short): + continue for declaration in _scan(text, relative_path): declarations.setdefault(declaration.name, declaration) source_digest = digest.hexdigest() @@ -614,6 +651,29 @@ def in_ignored_root(relative_text: str) -> bool: ) +def _may_declare(text: str, wanted_short: frozenset[str]) -> bool: + """Reject files that cannot contain a requested declaration.""" + + if not wanted_short: + return False + for line in _without_lean_comments(text).splitlines(): + match = _DECLARATION.match(line) + if match is None: + continue + name = _name_token(match.group(2)) + if name is not None and _short_name(name.removesuffix(".")) in wanted_short: + return True + return False + + +def _short_name(name: str) -> str: + """Return the last Lean name component without splitting quoted dots.""" + + if name.endswith("»") and "«" in name: + return name[name.rfind("«") :] + return name.rsplit(".", 1)[-1] + + def _lean_generation_revision( snapshot: TreeSnapshot, ignored_roots: set[PurePosixPath], @@ -636,7 +696,11 @@ def retained_entry(relative_text: str) -> bool: ) special = tuple(entry for entry in snapshot.special if retained_entry(entry[0])) placeholders = tuple(path for path in snapshot.placeholders if retained_entry(path)) - omitted = tuple(entry for entry in snapshot.omitted if retained_entry(entry[0])) + omitted = tuple( + entry + for entry in snapshot.omitted + if retained_entry(entry[0]) and entry[0] not in tolerated_links + ) retained_paths = { PurePosixPath(relative) for relative, _value in (*files, *symlinks, *special, *omitted) @@ -744,6 +808,9 @@ def _scan(text: str, relative: Path) -> list[Declaration]: name = _name_token(declaration_match.group(2)) if name is None: continue + # `_name_token` stops before the `{` in an explicit universe + # binder, leaving the syntactic separator behind. + name = re.sub(r"\.\{[^}\n]+\}$", "", name).removesuffix(".") qualified = ".".join([*namespaces, name]) found.append(Declaration(qualified, relative, number, keyword)) return found @@ -874,11 +941,12 @@ def url(self, name: str) -> str | None: ) ): return None + encoded_ref = quote_from_bytes(os.fsencode(self.ref), safe="") path = "/".join( quote_from_bytes(os.fsencode(part), safe="") for part in declaration.path.parts ) - return f"{self.repository_url}/blob/{self.ref}/{path}#L{declaration.line}" + return f"{self.repository_url}/blob/{encoded_ref}/{path}#L{declaration.line}" def build_linker( @@ -886,6 +954,7 @@ def build_linker( *, repository_url: str | None = None, ref: str | None = None, + names: Iterable[str] | None = None, exclude_roots: Iterable[str | Path] = (), source_index: SourceIndex | None = None, detect_missing: bool = True, @@ -912,6 +981,7 @@ def build_linker( snapshot, detected_url, detected_ref, linkable_paths = _capture_link_state( resolved_root, remapped_exclusions, + names=names, ) index = snapshot.index resolved_repository_url = repository_url or detected_url @@ -920,6 +990,7 @@ def build_linker( index = index_project( resolved_root, exclude_roots=remapped_exclusions, + names=names, ) if detect_missing and resolved_repository_url is None: resolved_repository_url = detect_repository_url(resolved_root) @@ -935,6 +1006,8 @@ def build_linker( def _capture_link_state( root: Path, exclude_roots: Iterable[str | Path], + *, + names: Iterable[str] | None = None, ) -> tuple[ IndexedSourceSnapshot, str | None, @@ -944,6 +1017,7 @@ def _capture_link_state( """Capture source bytes and prove which ones belong to one stable commit.""" exclusions = tuple(exclude_roots) + requested_names = None if names is None else tuple(names) last_snapshot: IndexedSourceSnapshot | None = None last_url: str | None = None for attempt in range(_SNAPSHOT_ATTEMPTS): @@ -951,7 +1025,11 @@ def _capture_link_state( time.sleep(_SNAPSHOT_RETRY_DELAY_SECONDS * attempt) before_url = detect_repository_url(root) before_ref = detect_ref(root) - snapshot = snapshot_project_sources(root, exclude_roots=exclusions) + snapshot = snapshot_project_sources( + root, + exclude_roots=exclusions, + names=requested_names, + ) last_snapshot = snapshot last_url = before_url after_url = detect_repository_url(root) diff --git a/autoform_cli/mermaid.py b/autoform_cli/mermaid.py index f34227e2..cf5fb5fc 100644 --- a/autoform_cli/mermaid.py +++ b/autoform_cli/mermaid.py @@ -11,6 +11,7 @@ import html import os from pathlib import Path +from urllib.parse import quote from typing import TYPE_CHECKING from .status import STATES, is_definition @@ -29,7 +30,7 @@ def node_link(node: Node, output: Path, link_extension: str) -> str: def relative_link(target: Path, output: Path, link_extension: str) -> str: """Relative link from the page at *output* to *target*, with its suffix swapped.""" relative = os.path.relpath(target.resolve(), output.resolve().parent) - return Path(relative).with_suffix(link_extension).as_posix() + return quote(Path(relative).with_suffix(link_extension).as_posix(), safe="/") def source_links(graph: Graph, output: Path, link_extension: str) -> dict[str, str]: @@ -79,7 +80,12 @@ def render_diagram( label = _escape(node.title) # Rectangles introduce data, rounded boxes assert something. shape = f'["{label}"]' if is_definition(node) else f'("{label}")' - lines.append(f" {handle}{shape}:::{statuses[node.id].key}") + state_key = ( + "planned" + if node.catalog == "module" and statuses[node.id].fully_proved + else statuses[node.id].key + ) + lines.append(f" {handle}{shape}:::{state_key}") for node in ordered: for dependency in node.statement_dependencies: @@ -90,7 +96,12 @@ def render_diagram( lines.append(f" {handles[dependency]} -.-> {handles[node.id]}") for node in ordered: - tooltip = _escape(f"{node.title} — {statuses[node.id].label}") + state_label = ( + "inventory checked" + if node.catalog == "module" and statuses[node.id].fully_proved + else statuses[node.id].label + ) + tooltip = _escape(f"{node.title} — {state_label}") lines.append(f' click {handles[node.id]} "{links[node.id]}" "{tooltip}"') if include_classdefs: @@ -273,7 +284,10 @@ def render_legend_tip(statuses: dict[str, NodeStatus]) -> str: "planned": "Described in the blueprint only.", } -_STATE_LABELS = {state.key: state.label for state in STATES} +_STATE_LABELS = { + **{state.key: state.label for state in STATES}, + "inventory_checked": "inventory checked", +} def render_page( @@ -296,7 +310,15 @@ def render_page( links=links, include_classdefs=include_classdefs, ) - legend = render_legend(statuses) + containers = frozenset( + node.parent for node in graph.nodes.values() if node.parent is not None + ) + target_statuses = { + node_id: statuses[node_id] + for node_id, node in graph.nodes.items() + if node_id not in containers and node.formalizable + } + legend = render_legend(target_statuses) sections = [ "---", "kind: graph", diff --git a/autoform_cli/project/_snapshot.py b/autoform_cli/project/_snapshot.py index 96c8cf33..77f868d8 100644 --- a/autoform_cli/project/_snapshot.py +++ b/autoform_cli/project/_snapshot.py @@ -248,11 +248,90 @@ def _cross_interface_identity(identity: tuple[int, ...]) -> tuple[int, ...]: def _directory_generation(path: Path) -> tuple[str, tuple[int, ...] | None]: try: metadata = os.stat(path, follow_symlinks=False) + identity = _node_identity(metadata) + _directory_change_token(path) except FileNotFoundError: return "missing", None except (OSError, TypeError, ValueError): return "unreadable", None - return ("directory" if stat.S_ISDIR(metadata.st_mode) else "other", _node_identity(metadata)) + return ("directory" if stat.S_ISDIR(metadata.st_mode) else "other", identity) + + +def _directory_change_token(path: Path) -> tuple[int, ...]: + """Return the native directory change generation omitted by Windows ``stat``. + + On Windows, pathname ``st_ctime_ns`` is the creation time rather than the + filesystem change time. Querying ``FILE_BASIC_INFO`` through a directory + handle retains the change time needed to detect a child rename-out/rename-in + ABA while the decision files are being captured. + """ + + if os.name != "nt": + return () + + import ctypes + from ctypes import wintypes + + class _FileBasicInfo(ctypes.Structure): + _fields_ = ( + ("creation_time", ctypes.c_longlong), + ("last_access_time", ctypes.c_longlong), + ("last_write_time", ctypes.c_longlong), + ("change_time", ctypes.c_longlong), + ("file_attributes", wintypes.DWORD), + ) + + kernel32 = ctypes.WinDLL("kernel32", use_last_error=True) + create_file = kernel32.CreateFileW + create_file.argtypes = ( + wintypes.LPCWSTR, + wintypes.DWORD, + wintypes.DWORD, + wintypes.LPVOID, + wintypes.DWORD, + wintypes.DWORD, + wintypes.HANDLE, + ) + create_file.restype = wintypes.HANDLE + get_information = kernel32.GetFileInformationByHandleEx + get_information.argtypes = ( + wintypes.HANDLE, + ctypes.c_int, + wintypes.LPVOID, + wintypes.DWORD, + ) + get_information.restype = wintypes.BOOL + close_handle = kernel32.CloseHandle + close_handle.argtypes = (wintypes.HANDLE,) + close_handle.restype = wintypes.BOOL + + share_read_write_delete = 0x00000001 | 0x00000002 | 0x00000004 + open_existing = 3 + backup_semantics = 0x02000000 + open_reparse_point = 0x00200000 + handle = create_file( + str(path), + 0, + share_read_write_delete, + None, + open_existing, + backup_semantics | open_reparse_point, + None, + ) + invalid_handle = ctypes.c_void_p(-1).value + if handle == invalid_handle: + raise ctypes.WinError(ctypes.get_last_error()) + try: + information = _FileBasicInfo() + if not get_information( + handle, + 0, # FILE_INFO_BY_HANDLE_CLASS.FileBasicInfo + ctypes.byref(information), + ctypes.sizeof(information), + ): + raise ctypes.WinError(ctypes.get_last_error()) + return (int(information.change_time),) + finally: + close_handle(handle) def _path_present(path: Path) -> bool: diff --git a/autoform_cli/render.py b/autoform_cli/render.py index 2f4d4cc5..e8e6c98c 100644 --- a/autoform_cli/render.py +++ b/autoform_cli/render.py @@ -12,22 +12,44 @@ import hashlib import html import json +import os import re import shutil -from collections.abc import Iterable +import stat +import tempfile +from collections.abc import Iterable, Iterator, Mapping +from contextlib import contextmanager from dataclasses import dataclass, field from pathlib import Path from urllib.parse import quote, unquote, urlsplit -from . import graph_pages, graph_views, mermaid, status -from .coverage import COVERAGE_DISPOSITIONS, CoverageSummary, load_coverage +from . import dag_viewer, graph_pages, graph_views, mermaid, status +from ._tree_snapshot import ( + BoundDirectoryTree, + TreeSelection, + TreeSnapshot, + TreeSnapshotError, + bind_directory_tree, +) +from .coverage import ( + COVERAGE_DISPOSITIONS, + CoverageSummary, + load_coverage, + validate_coverage_roles, +) from .graph import Graph, Node, load_graph from .lean import SourceLinker, build_linker, declaration_names, index_failure_message from .status import is_definition _HEADING = re.compile(r"^ {0,3}(#{1,6})[ \t]+(.+?)[ \t]*#*[ \t]*$") _FENCE = re.compile(r"^ {0,3}(`{3,}|~{3,})") -_MARKDOWN_LINK = re.compile(r"(?[^\]]*)\]\(\s*(?P[^)\s]+)(?:\s+[^)]*)?\)") +# A link label may itself contain a closing bracket, most commonly inside +# inline mathematical code such as ``[0,1]^n``. Only ``](`` closes the label. +_LINK_LABEL_PART = r"(?:[^\]]|\](?!\())" +_MARKDOWN_LINK = re.compile( + rf"(?{_LINK_LABEL_PART}*)\]" + r"\(\s*(?P[^)\s]+)(?:\s+[^)]*)?\)" +) #: A reference-style link definition, `[label]: target "title"`. Markdown #: resolves `[Paper][paper]` through one of these, so a rewrite that only sees #: inline links leaves the destination behind and publishes a dead link. @@ -36,7 +58,8 @@ r'(?P<[^>\r\n]+>|[^\s]+)(?P[ \t]+.*)?$' ) _ARTICLE_SLOT = re.compile( - r"^(?P[ \t]*)[-*+]\s+\[[^\]]+\]\(\s*(?P[^)\s]+)(?:\s+[^)]*)?\)\s*$" + rf"^(?P[ \t]*)[-*+]\s+\[{_LINK_LABEL_PART}+\]" + r"\(\s*(?P[^)\s]+)(?:\s+[^)]*)?\)\s*$" ) _DEPENDENCY_SECTIONS = frozenset({"depends on", "proof depends on"}) _SKIPPED_DIRECTORIES = frozenset({".obsidian", ".trash", ".git"}) @@ -44,6 +67,10 @@ #: Transcriptions of the paper being formalised. Vault material, not chapters. SOURCES_DIR = "sources" PUBLICATION_MANIFEST = "publication.json" +PUBLICATION_SCHEMA = "autoform-publication/v2" +SUPPORTED_PUBLICATION_SCHEMAS = frozenset( + {"autoform-publication/v1", PUBLICATION_SCHEMA} +) #: Derived views this command rewrites; stale copies must not leak into the site. _GENERATED_FILES = frozenset( { @@ -89,6 +116,7 @@ STYLESHEET = "stylesheets/blueprint.css" MERMAID_SCRIPT = "javascripts/blueprint-mermaid.js" LIVE_SCRIPT = "javascripts/blueprint-live.js" +DAG_SCRIPT = "javascripts/blueprint-dag.js" LOGO = "assets/autoform.svg" _ASSET_DIR = Path(__file__).resolve().parent / "assets" @@ -246,8 +274,8 @@ def render_site( """Write deterministic, read-only projections of the Markdown blueprint. Authored Markdown remains the only graph authority. The output joins three - reader surfaces over it: a book, derived progress, and multiscale dependency - maps. Publication excludes hidden and operational files, rejects symlinks, + reader surfaces over it: a book, derived progress, and a multiscale dependency + explorer. Publication excludes hidden and operational files, rejects symlinks, and never embeds timestamps or machine-specific paths. """ blueprint = Path(blueprint_dir).expanduser().resolve() @@ -259,7 +287,40 @@ def render_site( raise PublicationError( ["blueprint and output directories must be disjoint; refusing destructive render"] ) - _validate_publication_tree(blueprint) + with _captured_blueprint(blueprint) as ( + captured, + source_snapshot, + source_binding, + capture_mode, + ): + return _render_captured_site( + captured, + destination, + authored_blueprint=blueprint, + lean_root=lean_root, + repository_url=repository_url, + ref=ref, + clean=clean, + source_snapshot=source_snapshot, + source_binding=source_binding, + capture_mode=capture_mode, + ) + + +def _render_captured_site( + blueprint: Path, + destination: Path, + *, + authored_blueprint: Path, + lean_root: str | Path | None, + repository_url: str | None, + ref: str | None, + clean: bool, + source_snapshot: TreeSnapshot, + source_binding: BoundDirectoryTree, + capture_mode: str, +) -> RenderReport: + """Render exclusively from one captured blueprint generation.""" graph = load_graph(blueprint) coverage, coverage_issues = load_coverage(blueprint) @@ -274,20 +335,47 @@ def render_site( ) if coverage is None: raise PublicationError(["coverage contract could not be loaded"]) + coverage_role_issues = validate_coverage_roles(graph, coverage) + if coverage_role_issues: + raise PublicationError( + [ + f"coverage contract line {issue.line}: {issue.reason}" + if issue.line + else f"coverage contract: {issue.reason}" + for issue in coverage_role_issues + ] + ) statuses = status.derive(graph) # The repository root, not the vault's parent. A blueprint nested at # /docs/blueprint would otherwise be described as /blueprint, # and every generated permalink would 404. - repo_root = Path(lean_root).expanduser().resolve() if lean_root is not None else blueprint.parent + repo_root = ( + Path(lean_root).expanduser().resolve() + if lean_root is not None + else authored_blueprint.parent + ) + lean_names = tuple( + dict.fromkeys( + name + for node in graph.nodes.values() + for name in declaration_names(node.lean or "") + ) + ) try: - linker = build_linker(repo_root, repository_url=repository_url, ref=ref) + linker = build_linker( + repo_root, + repository_url=repository_url, + ref=ref, + names=lean_names, + ) except OSError as error: raise PublicationError([index_failure_message(error)]) from error numbers = _number_nodes(graph) used_by = _reverse_edges(graph) - sources_base = _sources_base(blueprint, repo_root, linker) + sources_base = _sources_base(authored_blueprint, repo_root, linker) _prepare_destination(destination, clean=clean) + source_revision = _snapshot_source_revision(source_snapshot) _write_publication_manifest( destination, blueprint, @@ -295,6 +383,8 @@ def render_site( linker, coverage=coverage, complete=False, + source_revision=source_revision, + source_capture=capture_mode, ) report = RenderReport(output_dir=destination) @@ -302,8 +392,13 @@ def render_site( # Nodes are published as environments on their milestone page, the way a # blueprint chapter carries many statements in sequence. Each keeps an # anchor so every cross-reference still lands on the statement itself. - groups = _group_nodes(graph) containers = _containers(graph) + groups = _group_nodes(graph) + # An inventory-only chapter still needs its authored landing page decorated + # with the neutral inventory metric, even though it has no theorem + # environments to consolidate. + for node_id in _module_inventories(graph, containers=containers): + groups.setdefault(graph.nodes[node_id].parent or "roadmap", []) anchors = { node_id: _anchor(node_id, group) for group, node_ids in groups.items() @@ -319,7 +414,7 @@ def render_site( { node_id: (destination / node.path.relative_to(blueprint), "") for node_id, node in graph.nodes.items() - if node_id in containers or not node.formalizable + if node_id in containers or (not node.formalizable and node.catalog is None) } ) node_sources = { @@ -344,7 +439,11 @@ def render_site( # Narrative articles remain book pages. Only formalizable leaves are # consolidated into their containing article with stable anchors. article = node_paths.get(source.resolve()) - if article is not None and article.formalizable and article.id not in containers: + if ( + article is not None + and (article.formalizable or article.catalog is not None) + and article.id not in containers + ): continue target.parent.mkdir(parents=True, exist_ok=True) if source.suffix.lower() == ".md": @@ -395,6 +494,7 @@ def render_site( targets=targets, narrative=narrative, blueprint=blueprint, + authored_blueprint=authored_blueprint, repo_root=repo_root, destination=destination, node_sources=node_sources, @@ -438,7 +538,11 @@ def render_site( graph, statuses, destination, - node_links=lambda page: _anchored_links(targets, page), + node_links=lambda page, node_ids: _anchored_links( + targets, + page, + node_ids=node_ids, + ), ) report.pages += len(generated_graph_pages) @@ -446,11 +550,16 @@ def render_site( (STYLESHEET, _stylesheet()), (MERMAID_SCRIPT, _mermaid_script()), (LIVE_SCRIPT, _static_asset("blueprint-live.js")), + (DAG_SCRIPT, dag_viewer.viewer_script()), (LOGO, _logo()), ): asset = destination / relative asset.parent.mkdir(parents=True, exist_ok=True) asset.write_text(contents, encoding="utf-8") + try: + source_binding.verify() + except TreeSnapshotError as error: + raise PublicationError(["blueprint changed during publication; retry the render"]) from error _write_publication_manifest( destination, blueprint, @@ -458,6 +567,8 @@ def render_site( linker, coverage=coverage, complete=True, + source_revision=source_revision, + source_capture=capture_mode, ) return report @@ -482,7 +593,7 @@ def _prepare_destination(destination: Path, *, clean: bool) -> None: if ( manifest.is_symlink() or not isinstance(publication, dict) - or publication.get("schema") != "autoform-publication/v1" + or publication.get("schema") not in SUPPORTED_PUBLICATION_SCHEMAS ): raise PublicationError( [ @@ -495,29 +606,130 @@ def _prepare_destination(destination: Path, *, clean: bool) -> None: destination.mkdir(parents=True) -def _validate_publication_tree(blueprint: Path) -> None: - """Reject inputs that could leak local state through a public artifact.""" - issues: list[str] = [] - if not blueprint.is_dir(): - return - for source in sorted(blueprint.rglob("*")): - relative = source.relative_to(blueprint) - folded_parts = {part.casefold() for part in relative.parts} - name = relative.name.casefold() - if ( - folded_parts.intersection(_LOCAL_ONLY_NAMES) - or name == ".env" - or name.startswith(".env.") - or name.endswith((".key", ".log", ".pem")) - ): - issues.append(f"refusing local or sensitive publication input: {relative.as_posix()}") - continue - if _is_hidden(relative): - continue - if source.is_symlink(): - issues.append(f"refusing symlink in blueprint publication: {relative.as_posix()}") +def _is_sensitive_publication_path(relative: Path) -> bool: + folded_parts = {part.casefold() for part in relative.parts} + name = relative.name.casefold() + return bool( + folded_parts.intersection(_LOCAL_ONLY_NAMES) + or name == ".env" + or name.startswith(".env.") + or name.endswith((".key", ".log", ".pem")) + ) + + +def _publication_path_selected(relative) -> bool: + path = Path(relative.as_posix()) + if _SKIPPED_DIRECTORIES.intersection(path.parts): + return False + if _is_sensitive_publication_path(path): + return True + return not ( + _is_hidden(path) + or path.name in _GENERATED_FILES + ) + + +_PUBLICATION_SELECTION = TreeSelection( + include=lambda path, mode: ( + _publication_path_selected(path) + and not ( + _is_sensitive_publication_path(Path(path.as_posix())) + and stat.S_ISREG(mode) + ) + ), + descend=lambda path: ( + _publication_path_selected(path) + and not _is_sensitive_publication_path(Path(path.as_posix())) + ), + placeholder=lambda path, mode: ( + _is_sensitive_publication_path(Path(path.as_posix())) + and not stat.S_ISDIR(mode) + ), + record_omitted=True, +) + + +def _validate_publication_snapshot(snapshot: TreeSnapshot) -> None: + paths = [ + *snapshot.directories, + *(relative for relative, _data in snapshot.files), + *(relative for relative, _target in snapshot.symlinks), + *(relative for relative, _mode in snapshot.special), + *snapshot.placeholders, + *(relative for relative, _kind in snapshot.omitted), + ] + issues = [ + f"refusing local or sensitive publication input: {relative}" + for relative in paths + if relative and _is_sensitive_publication_path(Path(relative)) + ] + if issues: + raise PublicationError(sorted(set(issues))) + + +def _capture_mode(bound: BoundDirectoryTree) -> str: + try: + bound.descriptor + except TreeSnapshotError: + return "portable-best-effort" + return "retained-descriptor" + + +def _materialize_publication_snapshot( + snapshot: TreeSnapshot, + destination: Path, + *, + capture_mode: str, +) -> None: + issues = snapshot.unsupported_entries() if issues: - raise PublicationError(issues) + relative, reason = issues[0] + if reason == "symbolic links are not supported": + raise PublicationError([f"refusing symlink in blueprint publication: {relative}"]) + raise PublicationError([f"refusing blueprint entry {relative}: {reason}"]) + if capture_mode == "retained-descriptor": + snapshot.materialize(destination, verify_bytes=False) + return + + # The destination is a fresh private temporary directory and every relative + # component has already passed TreeSnapshot's portable-name validation. No + # live source path is reopened while these exact captured bytes are written. + destination.mkdir() + for relative in snapshot.directories: + if relative: + (destination / relative).mkdir(parents=True, exist_ok=True) + for relative, data in snapshot.files: + target = destination / relative + target.parent.mkdir(parents=True, exist_ok=True) + target.write_bytes(data) + + +@contextmanager +def _captured_blueprint( + blueprint: Path, +) -> Iterator[tuple[Path, TreeSnapshot, BoundDirectoryTree, str]]: + """Retain, capture, and materialize one authored blueprint generation.""" + + try: + with bind_directory_tree( + blueprint, + selection=_PUBLICATION_SELECTION, + ) as bound: + snapshot = bound.capture() + _validate_publication_snapshot(snapshot) + capture_mode = _capture_mode(bound) + with tempfile.TemporaryDirectory(prefix="autoform-blueprint-") as temporary: + captured = Path(temporary).resolve() / "blueprint" + _materialize_publication_snapshot( + snapshot, + captured, + capture_mode=capture_mode, + ) + yield captured, snapshot, bound, capture_mode + except PublicationError: + raise + except TreeSnapshotError as error: + raise PublicationError([f"blueprint could not be captured safely: {error}"]) from error def _is_hidden(relative: Path) -> bool: @@ -540,7 +752,7 @@ def _sources_base(blueprint: Path, repo_root: Path, linker: SourceLinker) -> "_S if not linker.repository_url or not linker.ref: return None try: - relative = (blueprint / SOURCES_DIR).resolve().relative_to(repo_root).as_posix() + relative = (blueprint / SOURCES_DIR).relative_to(repo_root).as_posix() except ValueError: # The vault is outside the repository being linked, so no blob URL # describes it. Better no link than one that 404s. @@ -566,7 +778,10 @@ class _SourceBase: def href(self, tail: tuple[str, ...]) -> str: verb = "blob" if tail else "tree" path = "/".join((self.relative, *tail)) - return f"{self.repository_url}/{verb}/{self.ref}/{quote(path, safe='/')}" + return ( + f"{self.repository_url}/{verb}/{quote(self.ref, safe='')}/" + f"{quote(path, safe='/')}" + ) def _source_href(sources_base: _SourceBase, tail: tuple[str, ...]) -> str: @@ -574,23 +789,25 @@ def _source_href(sources_base: _SourceBase, tail: tuple[str, ...]) -> str: return sources_base.href(tail) -def _published_source_files(blueprint: Path): - """Yield the regular authored inputs that contribute to the static site.""" - for source in sorted(blueprint.rglob("*")): - relative = source.relative_to(blueprint) - if _SKIPPED_DIRECTORIES.intersection(relative.parts) or _is_hidden(relative): - continue - if relative.name in _GENERATED_FILES or not source.is_file(): - continue - yield source, relative +def _snapshot_source_revision(snapshot: TreeSnapshot) -> str: + digest = hashlib.sha256(b"autoform-markdown-publication/v2\0") + for relative, data in snapshot.files: + path = os.fsencode(relative) + for chunk in (path, data): + digest.update(len(chunk).to_bytes(8, "big")) + digest.update(chunk) + return digest.hexdigest() def _source_revision(blueprint: Path) -> str: - digest = hashlib.sha256(b"autoform-markdown-publication/v1\0") - for source, relative in _published_source_files(blueprint): - digest.update(relative.as_posix().encode("utf-8") + b"\0") - digest.update(source.read_bytes() + b"\0") - return digest.hexdigest() + try: + with bind_directory_tree( + blueprint, + selection=_PUBLICATION_SELECTION, + ) as bound: + return _snapshot_source_revision(bound.capture()) + except TreeSnapshotError as error: + raise PublicationError([f"blueprint could not be captured safely: {error}"]) from error def publication_source_revision(blueprint_dir: str | Path) -> str: @@ -607,6 +824,8 @@ def _write_publication_manifest( *, coverage: CoverageSummary, complete: bool, + source_revision: str, + source_capture: str, ) -> None: manifest = { "complete": complete, @@ -617,9 +836,10 @@ def _write_publication_manifest( "source_path": coverage.source_path, "source_sha256": coverage.source_sha256, }, - "schema": "autoform-publication/v1", + "schema": PUBLICATION_SCHEMA, "source": "blueprint/roadmap Markdown", - "source_revision": publication_source_revision(blueprint), + "source_capture": source_capture, + "source_revision": source_revision, "git_ref": linker.ref, "nodes": len(graph.nodes), "dependencies": graph.edge_count, @@ -642,7 +862,7 @@ def _group_nodes(graph: Graph) -> dict[str, list[str]]: containers = _containers(graph) for node_id in status.topological_order(graph): node = graph.nodes[node_id] - if not node.formalizable or node_id in containers: + if not (node.formalizable or node.catalog is not None) or node_id in containers: continue group = node.parent or "roadmap" grouped.setdefault(group, []).append(node_id) @@ -672,7 +892,7 @@ def _book_page_order(blueprint: Path, destination: Path, graph: Graph) -> list[P book_sources = { node.path.resolve() for node in graph.nodes.values() - if node.id in containers or not node.formalizable + if node.id in containers or (not node.formalizable and node.catalog is None) } pending = [blueprint / "README.md"] while pending: @@ -833,9 +1053,7 @@ def _next_target( if statement is None and chapter_page is not None: anchor = node.id.split("/", 1)[1].replace("/", "-") if "/" in node.id else node.id statement = f"{mermaid.relative_link(chapter_page, page, '.html')}#{anchor}" - graph_href = mermaid.relative_link( - graph_pages.focus_page_path(destination, node.id), page, ".html" - ) + graph_href = graph_pages.focus_page_href(destination, node.id, page, parent=node.parent) title = html.escape(node.title) heading = ( @@ -955,13 +1173,17 @@ def row( href = links.get(node.id) label = f'{name}' if href else name state = statuses[node.id] + inventory_checked = node.catalog == "module" and state.fully_proved + kind = "module inventory" if node.catalog == "module" else node.declaration or node.kind + state_key = "planned" if inventory_checked else state.key + state_label = "inventory checked" if inventory_checked else state.label rows.append( row( depth, f"{label} {html.escape(node.title)}", - html.escape(node.declaration or node.kind), - f'' - f'{html.escape(state.label)}', + html.escape(kind), + f'' + f'{html.escape(state_label)}', node_id=node.id, ) ) @@ -1007,7 +1229,18 @@ def _render_summary_nav( reads this file instead, so the tabs come from the same page order the book itself uses. """ - lines = [f"- [Home]({overview.relative_to(destination).as_posix()})", "- Book"] + # SUMMARY.md is a navigation manifest, not a searchable content page. A + # repository-wide book can make this one generated page larger than every + # article, so exclude it before Material constructs its transient index. + lines = [ + "---", + "search:", + " exclude: true", + "---", + "", + f"- [Home]({overview.relative_to(destination).as_posix()})", + "- Book", + ] for page in book_pages: if page == overview: continue @@ -1025,8 +1258,7 @@ def _render_summary_nav( lines.extend( [ "- Graph", - " - [Dependency maps](dependencies.md)", - " - [Full theorem DAG](dependencies/full.md)", + " - [Dependency explorer](dependencies.md)", f" - [Vault structure]({STRUCTURE_PAGE})", ] ) @@ -1060,7 +1292,7 @@ def _render_landing_page( # The sidebar lists the open tab's pages, and this tab holds only this # page, so on the landing page it is a column of one word. The tabs # already carry the reader to Book and Graph, so it goes, and the hero - # and map get the width instead. + # and explorer get the width instead. "hide:", " - navigation", " - toc", @@ -1088,51 +1320,41 @@ def _render_landing_page( targets=targets, ), ] - breakdown = mermaid.render_legend(statuses) - project = graph_views.project_view(graph, statuses) - if project.nodes: - # Clicking a chapter on the home page opens that chapter's dependency - # map: the home map is a preview of the Graph tab, not a second index. - # A project-view node is a whole chapter, so its id is namespaced - # `scope:`; the page is named for the group alone. Stripping has - # to precede the empty-group fallback, or the root chapter asks for - # `scope:.html` -- a truthy id, and so never the fallback it needs. - links = { - node.id: mermaid.relative_link( - destination - / "dependencies/chapters" - / f"{node.id.removeprefix('scope:') or 'roadmap'}.md", - page, - ".html", - ) - for node in project.nodes - } - # The map is the subject of this page, not an appendix to it: a reader - # arriving at a blueprint wants the shape of the project first. It runs - # the full width, and the legend rides along as its caption rather than - # as a section of its own further down. - parts.extend( - [ - "", - '
    ', - '
    ', - 'Project map', - 'Select a chapter to open its dependencies', - "
    ", - "", - mermaid.render_view_diagram(project, links=links, include_classdefs=False), - "", - f'
    \n\n{breakdown}\n\n
    ' - if breakdown - else "", - "
    ", - ] - ) - elif breakdown: - parts.extend(["", "## Status breakdown", "", breakdown]) + target_statuses = {node_id: statuses[node_id] for node_id in _countable(graph)} + breakdown = mermaid.render_legend(target_statuses) + # dependencies.json is the project projection written by graph_pages. The + # landing page deliberately mounts that exact payload and host instead of + # maintaining a second, Mermaid-only preview of the same graph. + parts.extend( + [ + "", + '
    ', + '
    ', + 'Mathematics atlas', + 'Explore mathematical regions, topics, and dependencies · ' + 'open full-page', + "
    ", + "", + dag_viewer.render_container( + "dependencies.json", + script_href=mermaid.relative_link(destination / DAG_SCRIPT, page, ".js"), + fallback_links=( + ("Open the dependency explorer", "dependencies.html"), + ), + fallback_total=1, + layout="embedded", + search_href="dependencies/index.json", + ), + "", + f'
    \n\n{breakdown}\n\n
    ' + if breakdown + else "", + "
    ", + ] + ) # The authored body is a contents list and links to the roadmap, coverage # contract and dependency view. The hero retains a compact coverage summary; - # repeating the full list here would only push the map down the page. Its + # repeating the full list here would only push the explorer down the page. Its # opening sentence is already the hero's lead. parts.append("") return "\n".join(part for part in parts if part is not None).rstrip() + "\n" @@ -1151,13 +1373,12 @@ def _render_landing_page( def _is_countable(graph: Graph, node_id: str, containers: frozenset[str]) -> bool: """Whether *node_id* is a formalization target the dashboards should count. - A leaf, and a leaf that declares something. Counting every leaf made a - freshly scaffolded vault report "0 of 1 targets complete, 1 ready now": the - roadmap landing page has no children yet, so it counted as an unstarted - result, and the site claimed work existed before any had been planned. + Declaration leaves are targets. Module catalogs are inventory evidence, + not mathematical formalization targets. Bare navigation and prose leaves + do not count either. """ - - return node_id not in containers and graph.nodes[node_id].formalizable + node = graph.nodes[node_id] + return node_id not in containers and node.formalizable def _countable(graph: Graph) -> list[str]: @@ -1165,6 +1386,22 @@ def _countable(graph: Graph) -> list[str]: return [node_id for node_id in graph.nodes if _is_countable(graph, node_id, containers)] +def _module_inventories( + graph: Graph, + *, + containers: frozenset[str] | None = None, + node_ids: Iterable[str] | None = None, +) -> list[str]: + """Return inventory leaves separately from mathematical targets.""" + containers = _containers(graph) if containers is None else containers + candidates = graph.nodes if node_ids is None else node_ids + return [ + node_id + for node_id in candidates + if node_id not in containers and graph.nodes[node_id].catalog == "module" + ] + + def _completion_percentage(done: int, total: int) -> int: """Round progress while reserving both endpoints for the exact endpoints.""" @@ -1208,23 +1445,38 @@ def _render_hero( # ``proved`` alone covers its own proof, definition body, or authored # Mathlib marker; ``fully_proved`` also closes the dependency chain. done = sum(node_status.fully_proved for node_status in selected.values()) + dispatchable = { + node_id: statuses[node_id] + for node_id in leaves + if graph.nodes[node_id].formalizable + } actionable = sum( - count for state, count in status.summarize(selected) if state.key in _ACTIONABLE_STATES + count + for state, count in status.summarize(dispatchable) + if state.key in _ACTIONABLE_STATES ) total = len(leaves) + inventory_count = len(_module_inventories(graph)) share = _completion_percentage(done, total) target_label = "target" if total == 1 else "targets" figures = [ - ("Scoped roadmap", f"{share}%", f"{done} of {total} {target_label} complete"), - ("Ready now", str(actionable), "unblocked, waiting for an author"), - ("Chapters", str(len(graph_views.group_nodes(graph))), "top-level milestones"), + ("Scoped roadmap", f"{share}%", f"{done} of {total} {target_label} complete", False), + ("Ready now", str(actionable), "unblocked, waiting for an author", False), + ( + "Module inventories", + str(inventory_count), + "existing Lean modules checked", + True, + ), + ("Chapters", str(len(graph_views.group_nodes(graph))), "top-level milestones", False), ] stats = "".join( - f'
    {value}
    ' + f'
    ' + f'
    {value}
    ' f'
    {html.escape(label)}
    ' f'
    {html.escape(note)}
    ' - for label, value, note in figures + for label, value, note, neutral in figures ) coverage_line = ( '
    ' @@ -1279,11 +1531,15 @@ def _render_overview_summary( node_ids: list[str] | None = None, ) -> str: """Render the compact, honest progress strip shown at the start of the book.""" + candidates = list(node_ids if node_ids is not None else graph.nodes) selected_ids = [ node_id - for node_id in (node_ids if node_ids is not None else graph.nodes) + for node_id in candidates if _is_countable(graph, node_id, containers) ] + inventory_count = len( + _module_inventories(graph, containers=containers, node_ids=candidates) + ) definitions = sum(is_definition(graph.nodes[node_id]) for node_id in selected_ids) results = len(selected_ids) - definitions item_parts = [] @@ -1291,6 +1547,11 @@ def _render_overview_summary( item_parts.append(f"{definitions} definition{'s' if definitions != 1 else ''}") if results: item_parts.append(f"{results} result{'s' if results != 1 else ''}") + if inventory_count: + item_parts.append( + f"{inventory_count} module " + f"{'inventory' if inventory_count == 1 else 'inventories'}" + ) item_summary = " · ".join(item_parts) or "No decomposed definitions or results yet" state_parts = [] @@ -1347,43 +1608,82 @@ def _anchor(node_id: str, group: str) -> str: return remainder.replace("/", "-") +class _AnchoredLinks(Mapping[str, str]): + """Resolve published article links on demand for one output page. + + Most article bodies mention no other article, while a repository-wide wiki + can contain tens of thousands of targets. Materializing the complete map + for every body therefore made link rewriting quadratic in the roadmap size. + """ + + def __init__( + self, + targets: Mapping[str, tuple[Path, str]], + page: Path, + *, + extension: str, + node_ids: Iterable[str] | None, + ) -> None: + self._targets = targets + self._page = page + self._resolved_page = page.resolve() + self._node_ids = targets.keys() if node_ids is None else tuple(dict.fromkeys(node_ids)) + self._allowed = None if node_ids is None else frozenset(self._node_ids) + self._extension = extension + self._cache: dict[str, str] = {} + self._hrefs: dict[Path, str] = {} + + def __getitem__(self, node_id: str) -> str: + if self._allowed is not None and node_id not in self._allowed: + raise KeyError(node_id) + cached = self._cache.get(node_id) + if cached is not None: + return cached + target, anchor = self._targets[node_id] + if target in self._hrefs: + href = self._hrefs[target] + elif target.resolve() == self._resolved_page: + href = "" + self._hrefs[target] = href + else: + href = mermaid.relative_link(target, self._page, self._extension) + if self._extension == ".html": + href = _as_published(href) + self._hrefs[target] = href + if href: + anchored = f"{href}#{anchor}" if anchor else href + else: + anchored = f"#{anchor}" if anchor else "#" + self._cache[node_id] = anchored + return anchored + + def __iter__(self): + return iter(self._node_ids) + + def __len__(self) -> int: + return len(self._node_ids) + + def _anchored_links( - targets: dict[str, tuple[Path, str]], + targets: Mapping[str, tuple[Path, str]], page: Path, *, extension: str = ".html", - hrefs: dict[Path, str] | None = None, -) -> dict[str, str]: + node_ids: Iterable[str] | None = None, +) -> Mapping[str, str]: """Link every node to its statement on the published chapter page. Use ``.md`` for links MkDocs will parse -- it validates and rewrites those itself -- and ``.html`` for raw HTML and Mermaid, which it never sees. A - statement on the current page is just a fragment. Calls for the same page - and extension can share *hrefs*, so each target page is linked once across - all of them. + statement on the current page is just a fragment. Link construction is + lazy, and nodes on the same target page share its cached base href. """ - resolved_page = page.resolve() - # Many nodes share a chapter page, and resolving a path walks the disk, so - # each target page is linked once. The current page is cached as "" and - # links as a bare fragment. - if hrefs is None: - hrefs = {} - links: dict[str, str] = {} - for node_id, (target, anchor) in targets.items(): - href = hrefs.get(target) - if href is None: - if target.resolve() == resolved_page: - href = "" - else: - href = mermaid.relative_link(target, page, extension) - if extension == ".html": - href = _as_published(href) - hrefs[target] = href - if href: - links[node_id] = f"{href}#{anchor}" if anchor else href - else: - links[node_id] = f"#{anchor}" if anchor else "#" - return links + return _AnchoredLinks( + targets, + page, + extension=extension, + node_ids=node_ids, + ) def _as_published(href: str) -> str: @@ -1418,9 +1718,9 @@ def _rewrite_links( all when *sources_base* says where to reach them in the repository. """ # Most pages name a few nodes, so each node link is built where it is used. - # A coverage page can name most of the graph, so one cache serves the whole - # text and each target page it reaches is linked once. - page_hrefs: dict[Path, str] = {} + # A coverage page can name most of the graph, so one lazy map serves the + # whole text and each target page it reaches is linked once. + anchored = _anchored_links(targets, page, extension=".md") def moved_target(raw: str) -> str | None: """Where *raw* should point once published, or None to leave it alone.""" @@ -1431,7 +1731,7 @@ def moved_target(raw: str) -> str | None: candidate = (source_dir / unquote(path)).resolve() node_id = node_sources.get(candidate) if node_id is not None: - href = _anchored_links({node_id: targets[node_id]}, page, extension=".md", hrefs=page_hrefs)[node_id] + href = anchored[node_id] if not targets[node_id][1] and separator: href = f"{'' if href == '#' else href}#{fragment}" return href @@ -1501,6 +1801,8 @@ def _number_nodes(graph: Graph) -> dict[str, str]: def _declaration_label(node: Node) -> str: + if node.catalog == "module": + return "Module" return DECLARATION_LABELS.get((node.declaration or "").casefold(), "Node") @@ -1525,6 +1827,7 @@ def _render_chapter( targets: dict[str, tuple[Path, str]], narrative: str | None, blueprint: Path, + authored_blueprint: Path, repo_root: Path, destination: Path, node_sources: dict[Path, str], @@ -1548,6 +1851,7 @@ def _render_chapter( links=links, page=page, blueprint=blueprint, + authored_blueprint=authored_blueprint, repo_root=repo_root, destination=destination, node_sources=node_sources, @@ -1558,11 +1862,23 @@ def _render_chapter( linked += node_linked unresolved.extend(node_unresolved) + summary_node_ids = list( + dict.fromkeys( + ( + *node_ids, + *( + node_id + for node_id, node in graph.nodes.items() + if node.catalog == "module" and (node.parent or "roadmap") == group + ), + ) + ) + ) chapter_summary = _render_overview_summary( graph, statuses, containers=containers, - node_ids=node_ids, + node_ids=summary_node_ids, ) if narrative is None: title = graph.nodes[group].title if group in graph.nodes else group.replace("-", " ").capitalize() @@ -1635,9 +1951,10 @@ def _render_environment( numbers: dict[str, str], used_by: dict[str, list[str]], linker: SourceLinker, - links: dict[str, str], + links: Mapping[str, str], page: Path, blueprint: Path, + authored_blueprint: Path, repo_root: Path, destination: Path, node_sources: dict[Path, str], @@ -1665,7 +1982,13 @@ def _render_environment( code_links, implementation_rows, linked, unresolved = _lean_presentation(node, linker) context_link = _graph_context_link(node, page=page, destination=destination) - source_link = _vault_source_link(node, repo_root=repo_root, linker=linker) + source_link = _vault_source_link( + node, + blueprint=blueprint, + authored_blueprint=authored_blueprint, + repo_root=repo_root, + linker=linker, + ) meta_rows = implementation_rows if node_status.key == "conditional": # A conditional proof must never read as finished, so the open @@ -1688,11 +2011,18 @@ def _render_environment( # amsthm distinguishes the two: a proposition is set in italics, a # definition upright. leanblueprint keeps that distinction on the web. - style = "theorem-style-definition" if is_definition(node) else "theorem-style-plain" - mark = "✓" if node_status.key in {"fully_proved", "mathlib"} else "●" + inventory_checked = node.catalog == "module" and node_status.fully_proved + display_key = "planned" if inventory_checked else node_status.key + display_label = "inventory checked" if inventory_checked else node_status.label + style = ( + "theorem-style-definition" + if node.catalog == "module" or is_definition(node) + else "theorem-style-plain" + ) + mark = "✓" if inventory_checked or node_status.key in {"fully_proved", "mathlib"} else "●" lines = [ - f'
    ', '
    ', @@ -1703,8 +2033,8 @@ def _render_environment( f"{context_link}" f"{source_link}" f'#' - f'' - f'{mark}{html.escape(node_status.label)}', + f'' + f'{mark}{html.escape(display_label)}', "
    ", '
    ', "", @@ -1766,7 +2096,14 @@ def _code_icon() -> str: ) -def _vault_source_link(node: Node, *, repo_root: Path, linker) -> str: +def _vault_source_link( + node: Node, + *, + blueprint: Path, + authored_blueprint: Path, + repo_root: Path, + linker, +) -> str: """Link a statement to the Markdown article it was authored in. The graph view and the published statement are both derived. This is the @@ -1775,10 +2112,14 @@ def _vault_source_link(node: Node, *, repo_root: Path, linker) -> str: if not linker.repository_url or not linker.ref: return "" try: - relative = node.path.resolve().relative_to(repo_root).as_posix() + blueprint_relative = node.path.resolve().relative_to(blueprint) + relative = (authored_blueprint / blueprint_relative).relative_to(repo_root).as_posix() except ValueError: return "" - href = f"{linker.repository_url}/blob/{linker.ref}/{relative}" + href = ( + f"{linker.repository_url}/blob/{quote(linker.ref, safe='')}/" + f"{quote(relative, safe='/')}" + ) label = html.escape(f"Edit the Markdown source for {node.title}", quote=True) icon = ( '
    2 items · 2 fully proved"]:::scope' in document # The vault copy carries its palette inline; Obsidian has no init script. assert f"classDef fully_proved fill:{_state('fully_proved').fill}" in document assert '' in document @@ -103,16 +103,20 @@ def test_the_published_graph_defers_its_palette_to_the_theme(tmp_path: Path) -> def test_proof_only_dependencies_are_dashed(tmp_path: Path) -> None: blueprint = tmp_path / "blueprint" - _write_node(blueprint / "roadmap" / "tool.md", "Tool") - (blueprint / "roadmap" / "result.md").write_text( - "---\n---\n\n# Result\n\n## Proof depends on\n\n- [Tool](tool.md)\n", + _write_node(blueprint / "roadmap" / "tools" / "README.md", "Tools") + _write_node(blueprint / "roadmap" / "tools" / "tool.md", "Tool") + result = blueprint / "roadmap" / "results" / "result.md" + result.parent.mkdir(parents=True) + _write_node(result.parent / "README.md", "Results") + result.write_text( + "---\n---\n\n# Result\n\n## Proof depends on\n\n- [Tool](../tools/tool.md)\n", encoding="utf-8", ) document = export_graph(blueprint).read_text(encoding="utf-8") - assert " n1 -.-> n0" in document - assert " n1 --> n0" not in document + assert "-.->" in document + assert " --> " not in document def test_green_stops_at_an_unproved_prerequisite(tmp_path: Path) -> None: @@ -151,7 +155,9 @@ def test_a_conditional_proof_has_its_own_colour_and_legend_entry(tmp_path: Path) document = export_graph(blueprint).read_text(encoding="utf-8") - assert '("Top"):::conditional' in document + # The bounded vault map collapses fine nodes into their top-level scope, + # but it must keep the conditional state visible in that scope's counts. + assert "1 conditional" in document assert f"classDef conditional fill:{_state('conditional').fill}" in document assert '' in document assert "Proof compiles, but rests on an open statement without a recorded Lean proof." in document @@ -315,6 +321,34 @@ def test_the_vault_gets_a_structure_page_obsidian_can_read(tmp_path: Path) -> No assert "dependencies.md)" not in page +def test_vault_views_label_checked_catalogs_as_module_inventories(tmp_path: Path) -> None: + blueprint = tmp_path / "blueprint" + ledger = blueprint / "sources/catalog.md" + ledger.parent.mkdir(parents=True) + ledger.write_text("# Catalog declarations\n", encoding="utf-8") + catalog = blueprint / "roadmap/catalog.md" + _write_node( + catalog, + "Existing module", + catalog="module", + lean="Existing.module", + statement="formalized", + proof="formalized", + ) + with catalog.open("a", encoding="utf-8") as stream: + stream.write("\n## Sources\n\n- [Ledger](../sources/catalog.md)\n") + + graph_page = export_graph(blueprint).read_text(encoding="utf-8") + structure_page = export_structure(blueprint).read_text(encoding="utf-8") + + assert "1 item · 1 inventory checked" in graph_page + assert "fully proved" not in graph_page + assert ( + "[Existing module](roadmap/catalog.md) · module inventory · inventory checked" + in structure_page + ) + + def test_generated_structure_can_be_refreshed(tmp_path: Path) -> None: blueprint = tmp_path / "blueprint" _write_node(blueprint / "roadmap" / "first.md", "First") diff --git a/uv.lock b/uv.lock index c820d280..6ece141c 100644 --- a/uv.lock +++ b/uv.lock @@ -114,6 +114,9 @@ dependencies = [ ] [package.optional-dependencies] +browser = [ + { name = "playwright" }, +] dev = [ { name = "mkdocs" }, { name = "mkdocs-literate-nav" }, @@ -131,6 +134,7 @@ requires-dist = [ { name = "mkdocs", marker = "extra == 'dev'", specifier = ">=1.6,<2" }, { name = "mkdocs-literate-nav", marker = "extra == 'dev'", specifier = ">=0.6,<1" }, { name = "mkdocs-material", marker = "extra == 'dev'", specifier = ">=9.5,<10" }, + { name = "playwright", marker = "extra == 'browser'", specifier = "==1.62.0" }, { name = "psutil", specifier = ">=5.9" }, { name = "pymdown-extensions", specifier = ">=11.0.1,<12" }, { name = "pymdown-extensions", marker = "extra == 'dev'", specifier = ">=11.0.1,<12" }, @@ -138,7 +142,7 @@ requires-dist = [ { name = "ruff", marker = "extra == 'dev'", specifier = ">=0.4" }, { name = "tomli", specifier = ">=2.3.1,<2.4" }, ] -provides-extras = ["repl", "dev"] +provides-extras = ["repl", "browser", "dev"] [[package]] name = "babel" @@ -665,6 +669,92 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/f7/ec/67fbef5d497f86283db54c22eec6f6140243aae73265799baaaa19cd17fb/ghp_import-2.1.0-py3-none-any.whl", hash = "sha256:8337dd7b50877f163d4c0289bc1f1c7f127550241988d568c1db512c4324a619", size = 11034, upload-time = "2022-05-02T15:47:14.552Z" }, ] +[[package]] +name = "greenlet" +version = "3.5.6" +source = { registry = "https://pypi.org/simple" } +sdist = { url = "https://files.pythonhosted.org/packages/3e/6e/0091f175ccd02b02bc8811bbcbcc6ac2e980be116e3b2f7a736ca322bf84/greenlet-3.5.6.tar.gz", hash = "sha256:8e67c43bdfc88d5fee6db0d3e40175b362fc95fb85f0412d233b9b203c53a575", size = 207653, upload-time = "2026-09-14T15:42:51.806Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/a7/4f/4af258e1ce388eb64be82d6466b7d0b3bc3eede154e14c3360a76a759b71/greenlet-3.5.6-cp310-cp310-macosx_11_0_universal2.whl", hash = "sha256:95e7c44d072db623a1aab04ce488cf9533294a77ed9d072cd503a3596f4106ac", size = 292967, upload-time = "2026-09-14T14:26:34.475Z" }, + { url = "https://files.pythonhosted.org/packages/1d/05/dc0d54e90af2f192724936799cee990687792ff54a4638d3ae0e0a0145c0/greenlet-3.5.6-cp310-cp310-manylinux_2_24_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:b7d501d5eb5d4f67207df364752ad697465b834268744be7581c18d81d35d41d", size = 609284, upload-time = "2026-09-14T15:11:58.49Z" }, + { url = "https://files.pythonhosted.org/packages/c1/51/826b4fe7bc39c3f910c95e889a981c827f72a611fc035f31816a256cf043/greenlet-3.5.6-cp310-cp310-manylinux_2_24_ppc64le.manylinux_2_28_ppc64le.whl", hash = "sha256:a364c1ea75dc51b83a17f52fe0c79cf8bc4ddf740403bebd4581c7666eea017d", size = 622648, upload-time = "2026-09-14T15:20:39.198Z" }, + { url = "https://files.pythonhosted.org/packages/55/3b/f2d36fc38934588dff6d6ec9288934c9611abac7a79c866c2002fc707698/greenlet-3.5.6-cp310-cp310-manylinux_2_24_s390x.manylinux_2_28_s390x.whl", hash = "sha256:5599b380c1f28efeb724e81569eac80cd92f99a85bd9775456caaf3225d40b11", size = 629557, upload-time = "2026-09-14T15:25:03.036Z" }, + { url = "https://files.pythonhosted.org/packages/94/5c/092682ae7ca1aadd44aa36b0bc35c48c9ed55f9ffebb5794980b1e2ae74b/greenlet-3.5.6-cp310-cp310-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:eed88b64a5e5da72d6a71cdc5aaeefaa5ced9b748f8d19f89800b339961dad39", size = 622813, upload-time = "2026-09-14T14:35:54.845Z" }, + { url = "https://files.pythonhosted.org/packages/d6/f6/4167f0e44e795840cbc219b2e5d8f576492192cd9e3e17e827db20287daa/greenlet-3.5.6-cp310-cp310-manylinux_2_39_riscv64.whl", hash = "sha256:5bbda3c70dd35d60671bc33b01916802707a052130d9e50cdb871d34594d35cb", size = 425482, upload-time = "2026-09-14T15:28:34.144Z" }, + { url = "https://files.pythonhosted.org/packages/07/59/9c6b723a559b53bee0980a5dc57577d434891dd454f0fe54ed6e22d4e4ce/greenlet-3.5.6-cp310-cp310-musllinux_1_2_aarch64.whl", hash = "sha256:874cea8bb1ec1ddccbacbd027856f6bf496f6bc18aba97a918c20e067edab236", size = 1585817, upload-time = "2026-09-14T15:10:03.922Z" }, + { url = "https://files.pythonhosted.org/packages/de/d4/2bceaa305ff0ecf99511480da8f0a866eb2469a68da8715008a0d3e8f65f/greenlet-3.5.6-cp310-cp310-musllinux_1_2_x86_64.whl", hash = "sha256:128813fc29f2336a21b4d06eedd5e16bcc7ea46f59e9ff1cb30ea70e48195d88", size = 1650177, upload-time = "2026-09-14T14:35:46.736Z" }, + { url = "https://files.pythonhosted.org/packages/7a/33/c57855a6abada0c7bfb9c6c0f33df1fbed8e5224708478dbcdff6c5db490/greenlet-3.5.6-cp310-cp310-win_amd64.whl", hash = "sha256:dad3d233d441a022c1f7155f0fb9d5aff7b97c1ea8c7dfa02cce586b16ab2d0b", size = 322896, upload-time = "2026-09-14T14:24:52.308Z" }, + { url = "https://files.pythonhosted.org/packages/f1/d7/41511ee2696f14be4200b524d9553dc4295e2bdeb20aa8962c3cb25e71c6/greenlet-3.5.6-cp311-cp311-macosx_11_0_universal2.whl", hash = "sha256:a6a4b98a9132e0f45c9fc245a63894cfd8c45fb7a0d6bffc5eab3ec327cf7324", size = 294075, upload-time = "2026-09-14T14:25:16.922Z" }, + { url = "https://files.pythonhosted.org/packages/f8/7b/b509624970909294cd064ff7346148ca9941c21bec9026d7873dd254e9fa/greenlet-3.5.6-cp311-cp311-manylinux_2_24_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:45bfd2b51e38aaa5f9849f114d9c7c1d75f69187c849b3549cd64c465283abfa", size = 613429, upload-time = "2026-09-14T15:12:00.454Z" }, + { url = "https://files.pythonhosted.org/packages/2b/5c/d2eb503067f9ba20875ef8c87681f29a64f53bbbbe4059a5d7c53179d442/greenlet-3.5.6-cp311-cp311-manylinux_2_24_ppc64le.manylinux_2_28_ppc64le.whl", hash = "sha256:3c6dede9133e1da41d561bc3fb14e92b47e2ce39ae60edefaad145658ea7c5e2", size = 625405, upload-time = "2026-09-14T15:20:41.053Z" }, + { url = "https://files.pythonhosted.org/packages/1b/24/9b071d11c8bb9f5f38cccacc38fcc234d91997a4c395cc2bf43ecae89642/greenlet-3.5.6-cp311-cp311-manylinux_2_24_s390x.manylinux_2_28_s390x.whl", hash = "sha256:4fb8e59f68845d56c23c031dcd79c329f345e4a9d2ffac91c3d1ab366bdc457b", size = 633270, upload-time = "2026-09-14T15:25:04.864Z" }, + { url = "https://files.pythonhosted.org/packages/ec/d3/63d4477ce31dff2fd802a9a20240f6606aac85977e0fb18443aae33de3f6/greenlet-3.5.6-cp311-cp311-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:1c20ea32a73d17b9b60e3371240e17b0068120c98a5ec01a224a7dd8c89733ba", size = 624428, upload-time = "2026-09-14T14:35:56.895Z" }, + { url = "https://files.pythonhosted.org/packages/88/17/ac11883ecc9da19c681c8b763ee39e6f7dca2aa81874eb11a075d3cbeb00/greenlet-3.5.6-cp311-cp311-manylinux_2_39_riscv64.whl", hash = "sha256:d701eab36200c36224833d07dbdb709adb7fd4253429548ddb5e547b8ed40586", size = 428068, upload-time = "2026-09-14T15:28:35.872Z" }, + { url = "https://files.pythonhosted.org/packages/ad/aa/9cde4e00688eaa2a03b91d12e4681439a87e6aad860399e0847af6a014ca/greenlet-3.5.6-cp311-cp311-musllinux_1_2_aarch64.whl", hash = "sha256:5a0b2791239c99992a86c1b635b787fe2a877d9eaaa26f8891ce943832b585ae", size = 1588385, upload-time = "2026-09-14T15:10:05.386Z" }, + { url = "https://files.pythonhosted.org/packages/5c/01/24632b5ec186b64e21e07a8f53ce5e15a7e9cb33eddee99a5fe16379afa5/greenlet-3.5.6-cp311-cp311-musllinux_1_2_x86_64.whl", hash = "sha256:188bf333769b7145e2b0b4a7f09615ec550ed44d3a2a8395fb7b36f0e9901e13", size = 1653119, upload-time = "2026-09-14T14:35:48.275Z" }, + { url = "https://files.pythonhosted.org/packages/ce/6c/019d2ef898f4b9ac845167f1c6f73229e9a4e2439362a5e2ce50205a19b0/greenlet-3.5.6-cp311-cp311-win_amd64.whl", hash = "sha256:a6b4ff33f7e011bbaa148238d131c4fd4f8afbab3c104ddfbdb2b12b74ff7016", size = 323317, upload-time = "2026-09-14T14:22:38.836Z" }, + { url = "https://files.pythonhosted.org/packages/5a/7a/439df999455e3bdf02b1c68f3848d4020385ef0a01f89f706b07bf148a65/greenlet-3.5.6-cp311-cp311-win_arm64.whl", hash = "sha256:59deccd347735a7774223b05a93773fddbb298aba3cea21be4337fb4752dbe32", size = 307739, upload-time = "2026-09-14T14:23:40.469Z" }, + { url = "https://files.pythonhosted.org/packages/72/18/3fc6d951466ae9a2a688edcddde3b2e388da0a8244e0caf7117bbeb0eb95/greenlet-3.5.6-cp312-cp312-macosx_11_0_universal2.whl", hash = "sha256:a5876d0a60355af98d535c47f6cd6eb0f8a432396dab26845d380b92f8412422", size = 295668, upload-time = "2026-09-14T14:22:33.241Z" }, + { url = "https://files.pythonhosted.org/packages/27/89/366d2af5061eeefa5012f510d95a99c8620dcc457609838db4d538820318/greenlet-3.5.6-cp312-cp312-manylinux_2_24_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:e85880b538e59a59f55117b81f208a6660ad5ac328aad9305f812d9b8bc67a0f", size = 611700, upload-time = "2026-09-14T15:12:01.962Z" }, + { url = "https://files.pythonhosted.org/packages/54/1c/07f133f865fd58ae593dd2bbec3144acaee9b04ffe2eb48c6e121747ceef/greenlet-3.5.6-cp312-cp312-manylinux_2_24_ppc64le.manylinux_2_28_ppc64le.whl", hash = "sha256:f0ba7c2a329d650628f4c8572fd1db29f0a59dd70a3e3e0710dcf18a35cce9d8", size = 624223, upload-time = "2026-09-14T15:20:42.459Z" }, + { url = "https://files.pythonhosted.org/packages/a7/f2/844dc823ff2752ad049caa6b59d57e4572f9c445934b02d3518f4c67197c/greenlet-3.5.6-cp312-cp312-manylinux_2_24_s390x.manylinux_2_28_s390x.whl", hash = "sha256:ee7d9da3bf493909cf811a3f038840cb34fab5ae2956b8a263919f6e289ab188", size = 629529, upload-time = "2026-09-14T15:25:06.354Z" }, + { url = "https://files.pythonhosted.org/packages/66/6a/1594f3869c57c149abdb380492529e04d4c0229b5e4d79572c5bd0aaa673/greenlet-3.5.6-cp312-cp312-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:975736b002ed080d124cf81a79cb7e05cb26d6b3f5c7a7b651c0fcce70353aa1", size = 621404, upload-time = "2026-09-14T14:35:59.027Z" }, + { url = "https://files.pythonhosted.org/packages/c0/42/b1f8dbc89a53b9e77859fc1ad1627d106fc361daa3ea4bdf43a91ebb4338/greenlet-3.5.6-cp312-cp312-manylinux_2_39_riscv64.whl", hash = "sha256:71890d5247020c25c21a6b65202782bfc281d4e6e244842419d30e3492bb6dcc", size = 432385, upload-time = "2026-09-14T15:28:37.369Z" }, + { url = "https://files.pythonhosted.org/packages/a2/f5/33e5c9e48178b9259fd000f8f45caa4a65036f65d3d0c06a602f570f025d/greenlet-3.5.6-cp312-cp312-musllinux_1_2_aarch64.whl", hash = "sha256:0616b8f878098c5681fd8f0dc92d887551717402342a70f0abcbfea5f5ad8a44", size = 1584998, upload-time = "2026-09-14T15:10:06.653Z" }, + { url = "https://files.pythonhosted.org/packages/ef/31/9b4e140bc24d0ad7927ebd651f5608b0acc2334d061748c3b6ad19085cfa/greenlet-3.5.6-cp312-cp312-musllinux_1_2_x86_64.whl", hash = "sha256:3dbb4596a6a4e5d47121a33ff20533a81e60f302d9e67b69909a8bc21a43f0a7", size = 1647568, upload-time = "2026-09-14T14:35:49.787Z" }, + { url = "https://files.pythonhosted.org/packages/c3/71/d79f1791f824f8ff15c2978746640467ae932a2365e0201069f7f272395f/greenlet-3.5.6-cp312-cp312-win_amd64.whl", hash = "sha256:7ac4abb3877c43af320392c664774eef6fa2cc063c79a55fc02d844a3cbe7395", size = 324203, upload-time = "2026-09-14T14:22:54.504Z" }, + { url = "https://files.pythonhosted.org/packages/63/af/42aca4d56e8cb321912203069d8d34734cb288222f10ad2ae102718cc577/greenlet-3.5.6-cp312-cp312-win_arm64.whl", hash = "sha256:301102a49120b095e72a7838792b41233975fc1c155daec6d98f81c00c9280e0", size = 308310, upload-time = "2026-09-14T14:24:03.008Z" }, + { url = "https://files.pythonhosted.org/packages/f1/a1/e720a38852366c589e1a46cf570b886507ad2cf591050c203365638baab0/greenlet-3.5.6-cp313-cp313-macosx_11_0_universal2.whl", hash = "sha256:f96f0e30b5a95c7631b12bfe214cbc90ec8fe8cfa36920596c10514a65743519", size = 294627, upload-time = "2026-09-14T14:24:40.102Z" }, + { url = "https://files.pythonhosted.org/packages/eb/c3/58187858df41354a11e6a55b421e7af9059798abdab3a384cc51b8567c38/greenlet-3.5.6-cp313-cp313-manylinux_2_24_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:c75116c9de79949de23006e2d9b35ee82874c594fcf5c0311b439acaa14b8441", size = 614356, upload-time = "2026-09-14T15:12:03.399Z" }, + { url = "https://files.pythonhosted.org/packages/ce/b9/3a7e67d5f05c9760b1ad411fa52264bd69cc08e22a2ebfb4018b90628ced/greenlet-3.5.6-cp313-cp313-manylinux_2_24_ppc64le.manylinux_2_28_ppc64le.whl", hash = "sha256:cad5782f93f7f738b62c6527b6f32a60694d924029f299a8b524758cfa53d815", size = 626756, upload-time = "2026-09-14T15:20:44.269Z" }, + { url = "https://files.pythonhosted.org/packages/c6/7c/40400455f5b5a65bb83e94fde66d1be9e5ec518638113f8083ace746c309/greenlet-3.5.6-cp313-cp313-manylinux_2_24_s390x.manylinux_2_28_s390x.whl", hash = "sha256:a93ee7c6e8fd0f8a83525a51bd777be57ee17787e91d805bd8d6faf9dcada18e", size = 632632, upload-time = "2026-09-14T15:25:07.813Z" }, + { url = "https://files.pythonhosted.org/packages/85/cb/ab0c123c514ed4e94c0dc9ee2e86362633e6b998cfc05de7fc9ac2eb9690/greenlet-3.5.6-cp313-cp313-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:f98e8215e172f567ce80eeaed9107fb4d32b6c44f26983d9b8334658136a205a", size = 623779, upload-time = "2026-09-14T14:36:01.104Z" }, + { url = "https://files.pythonhosted.org/packages/f9/67/1f35cff30a6c51c3f23b63d4afcc7313ab4f97490ba3676fa78178984b27/greenlet-3.5.6-cp313-cp313-manylinux_2_39_riscv64.whl", hash = "sha256:7f731ebac68ea06d628658295cb2d217b10186329fcf9a3b6a149045059bf92e", size = 434933, upload-time = "2026-09-14T15:28:38.858Z" }, + { url = "https://files.pythonhosted.org/packages/a5/26/fda8a5a06e7073333ccb038133c5893b9e0c4fe29d5992a17e83c241bc6e/greenlet-3.5.6-cp313-cp313-musllinux_1_2_aarch64.whl", hash = "sha256:df19e2d0b1620039af5102563fbd96e8938c7f5c3f5828528d641d9fc585525e", size = 1584930, upload-time = "2026-09-14T15:10:08.234Z" }, + { url = "https://files.pythonhosted.org/packages/2f/37/50f8813163148d6234e08b23dcad6a9e37f01d148c8ec976e4c44ea2d918/greenlet-3.5.6-cp313-cp313-musllinux_1_2_x86_64.whl", hash = "sha256:06c0e933290fba8ffe53ead4ae1b8044b0e9754b75cebf381aa2bc3e50d82fac", size = 1647590, upload-time = "2026-09-14T14:35:51.173Z" }, + { url = "https://files.pythonhosted.org/packages/86/da/b7669b09586365654083a62bd0724cf06cb74bd5085a15cdd161271f992f/greenlet-3.5.6-cp313-cp313-win_amd64.whl", hash = "sha256:5b602b4201b965a8354d74e232364a66ff243dd142e350d035f46169bb36e13d", size = 324086, upload-time = "2026-09-14T14:23:48.428Z" }, + { url = "https://files.pythonhosted.org/packages/e5/5d/c9663cfe84a2a9e0aa96f066f5b0594c227ea4c647511e087e2e11d4ac0a/greenlet-3.5.6-cp313-cp313-win_arm64.whl", hash = "sha256:876077e7ebb8c84ed068e2b23d4c62ebb010d60df84b9591af1be2f39010ffb2", size = 308211, upload-time = "2026-09-14T14:28:01.634Z" }, + { url = "https://files.pythonhosted.org/packages/66/c0/d254544ae2b8bdd311aef000fafc02828c2771b17d994b3075620ea7cc6e/greenlet-3.5.6-cp314-cp314-macosx_11_0_universal2.whl", hash = "sha256:8cddea1b8339451c2fb3388e138347b6126744f33b611bdb55b7357361cfef46", size = 295221, upload-time = "2026-09-14T14:25:11.583Z" }, + { url = "https://files.pythonhosted.org/packages/18/18/eb54be16b9cc3971e09ca5b73334e1b8c804a4630d9addaaf218a4fe300f/greenlet-3.5.6-cp314-cp314-manylinux_2_24_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:c59acfa8eb73a1e0d484392dc002bdf001fd4ce73394e0132df3d1ab6093d7cb", size = 660992, upload-time = "2026-09-14T15:12:04.876Z" }, + { url = "https://files.pythonhosted.org/packages/8f/b4/e193efe65671dcf294bc51fcc59efb52d154adf8612c4ea016da0d2c486c/greenlet-3.5.6-cp314-cp314-manylinux_2_24_ppc64le.manylinux_2_28_ppc64le.whl", hash = "sha256:a3b4a01c6da07ef9f80d4fe8933b994bc99747bcea3eab0330a9c34d3c12655b", size = 673428, upload-time = "2026-09-14T15:20:45.756Z" }, + { url = "https://files.pythonhosted.org/packages/fd/21/631bb45fafde1dca782152377c0676d182ec924820064047f533a3627b28/greenlet-3.5.6-cp314-cp314-manylinux_2_24_s390x.manylinux_2_28_s390x.whl", hash = "sha256:dd0b83bed3405b586a3133629f1d1a5bc7bfd64822a3b7ab342bdc68e6dbc61b", size = 677688, upload-time = "2026-09-14T15:25:09.279Z" }, + { url = "https://files.pythonhosted.org/packages/45/ac/28fa7a9e50f2859466214c4ac584d776db52c1604ad4dd158960a5af2a1f/greenlet-3.5.6-cp314-cp314-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:9a09d59bef1db94f384b5bcc2d523694d338f3df6b757aeeaf7baca5d0c0be88", size = 670773, upload-time = "2026-09-14T14:36:02.577Z" }, + { url = "https://files.pythonhosted.org/packages/40/30/2b0a73e68e1e18e30b601d0d183cfdfc2beca4de5a6843c630f0fc9fb90c/greenlet-3.5.6-cp314-cp314-manylinux_2_39_riscv64.whl", hash = "sha256:fdacf26402389bdd89857ad3c045a26fe8f3314f9a8b28226f82f88463a65b77", size = 480475, upload-time = "2026-09-14T15:28:40.741Z" }, + { url = "https://files.pythonhosted.org/packages/c3/cd/fb7d6cdd86ff3427c1494854f0e35437eba05142be91f530f6da75e09e19/greenlet-3.5.6-cp314-cp314-musllinux_1_2_aarch64.whl", hash = "sha256:8b7c73d1cef3d9ae963e9ff03f6222df43efbb9054ffd2f1969c935b7fc84c02", size = 1631900, upload-time = "2026-09-14T15:10:09.745Z" }, + { url = "https://files.pythonhosted.org/packages/f6/40/143bdbb20a516628cb15074ae52ed17d850b450292609c7a6fccac6dbece/greenlet-3.5.6-cp314-cp314-musllinux_1_2_x86_64.whl", hash = "sha256:8b27df301f56e3b3d2298095c8f7d6b68f2521f6b1693e901fa039bdbae34424", size = 1693740, upload-time = "2026-09-14T14:35:52.959Z" }, + { url = "https://files.pythonhosted.org/packages/c9/9e/019642432e6ae283301df1361227d47610709d2dc69a38f95edef266d713/greenlet-3.5.6-cp314-cp314-win_amd64.whl", hash = "sha256:f8f0bd690e1a41294ac87905e8121c81a3761ec2583c768f13467428606c8c7a", size = 327473, upload-time = "2026-09-14T14:28:12.948Z" }, + { url = "https://files.pythonhosted.org/packages/e9/7f/8aafc7bf70c948786dba7221d0dc0838e5329bebc6d434ef2208b4f0e760/greenlet-3.5.6-cp314-cp314-win_arm64.whl", hash = "sha256:8cda13494d86a4f12429641117cb6ac4bbbc9c30a33f711f7d3a2e5fbe4b0b7e", size = 311095, upload-time = "2026-09-14T14:28:00.7Z" }, + { url = "https://files.pythonhosted.org/packages/14/7e/7a205688a5b3074933b18a906608d46d106e9a79d776bdab5a4abf4b4feb/greenlet-3.5.6-cp314-cp314t-macosx_11_0_universal2.whl", hash = "sha256:97c5a53e8c1754df58e73f047a99e287d4da1bdfe64b0072fb25c87000897951", size = 305352, upload-time = "2026-09-14T14:21:31.962Z" }, + { url = "https://files.pythonhosted.org/packages/78/cb/9c4a57a9d9dd0256e20b8f7f4f06554c2c92badebf0ab73ce344321b78b9/greenlet-3.5.6-cp314-cp314t-manylinux_2_24_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:fea4427d1ffdb3b523d7daa6712038428a4c16c450b9777bdd1221cfee0eab49", size = 672671, upload-time = "2026-09-14T15:12:06.347Z" }, + { url = "https://files.pythonhosted.org/packages/97/52/c6729681ebbd298f4decd28746815acc8a0b0a0fde21d2df33776fd4d042/greenlet-3.5.6-cp314-cp314t-manylinux_2_24_ppc64le.manylinux_2_28_ppc64le.whl", hash = "sha256:73a29b5ba642e35433166a03a3e02935e7238c4b3467fbd77523b99edea23e5b", size = 679489, upload-time = "2026-09-14T15:20:47.291Z" }, + { url = "https://files.pythonhosted.org/packages/71/76/3c11c21e0716b1f1dc7c1a4b3d690abb1d3b448c69a9d32049fecb64010a/greenlet-3.5.6-cp314-cp314t-manylinux_2_24_s390x.manylinux_2_28_s390x.whl", hash = "sha256:61a61b4a95a4f97922c3a6f5606d3e360851584bd47e500a5161373c53810e3d", size = 681303, upload-time = "2026-09-14T15:25:11.088Z" }, + { url = "https://files.pythonhosted.org/packages/58/c5/2b6c721ba8b8963da42d5a0f57f25b8aaeb1fe9bdd156875e57f3be648a2/greenlet-3.5.6-cp314-cp314t-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:460e70b033aba8ed47e2ac9b5d0d2157b05a34fbfa30a241400aef4118902cdc", size = 676608, upload-time = "2026-09-14T14:36:03.959Z" }, + { url = "https://files.pythonhosted.org/packages/3f/26/3ae402202452cd5941bbbd483e5a74297e2397e7aa3182c2a5e3ab7d5666/greenlet-3.5.6-cp314-cp314t-manylinux_2_39_riscv64.whl", hash = "sha256:fe3170a69fe039b18ad18171e66faa9a75f6fe9d78f968fd9b54e09fbd714d81", size = 510112, upload-time = "2026-09-14T15:28:42.112Z" }, + { url = "https://files.pythonhosted.org/packages/b2/04/0d018e0d05bcdde19a0fcb907834155f1fc853a9bedd3f3f5e6acadcae19/greenlet-3.5.6-cp314-cp314t-musllinux_1_2_aarch64.whl", hash = "sha256:ca80a49b53ed1d22f7282da7255f7bb2fd1935fd0f623d8613fda38745f18961", size = 1641479, upload-time = "2026-09-14T15:10:11.216Z" }, + { url = "https://files.pythonhosted.org/packages/59/bb/f02ef9073919158f6403fe3701d4ed4403d646720e7201dfc6e9d264bac3/greenlet-3.5.6-cp314-cp314t-musllinux_1_2_x86_64.whl", hash = "sha256:916f92f2a8db10508f739d0b5e00b83defe5d1115a997c54532a6d7cf8c95404", size = 1698758, upload-time = "2026-09-14T14:35:54.336Z" }, + { url = "https://files.pythonhosted.org/packages/08/a5/1f48fe647473a2dcccfd1839b2ff2c78eb57009be776b4da071e901c9bff/greenlet-3.5.6-cp314-cp314t-win_amd64.whl", hash = "sha256:886bcf1870af74c32bc310fd00a6b803445e17e51b7d5a107c7b35c0f362cc16", size = 331574, upload-time = "2026-09-14T14:27:18.451Z" }, + { url = "https://files.pythonhosted.org/packages/cd/72/3882855a75838faeb54a58aeef4fd77d20b2a86d4bad570c70d41b565dcf/greenlet-3.5.6-cp315-cp315-macosx_11_0_universal2.whl", hash = "sha256:3ac3494c381dab876cad7d0b22f3a722f3e0c8deb3a65b9e7f35ad7f58b8fcb3", size = 295926, upload-time = "2026-09-14T14:27:21.16Z" }, + { url = "https://files.pythonhosted.org/packages/10/1f/be4d957d8a9b90bcbe8db206548a42134d96222d43e5ed3fc4708fb6e24b/greenlet-3.5.6-cp315-cp315-manylinux_2_24_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:602024dae6d77e161f4b89491b62ca1d4f19949d79d47b2db057e476d21179d6", size = 666910, upload-time = "2026-09-14T15:12:07.901Z" }, + { url = "https://files.pythonhosted.org/packages/a1/af/60d62571a7d6de961e4ce7625d6c2faf359345659fc782d2cdf517c34577/greenlet-3.5.6-cp315-cp315-manylinux_2_24_ppc64le.manylinux_2_28_ppc64le.whl", hash = "sha256:f8e63209c3e1e828ee6a457529b4a6d8b05d050fe0ae03a7ae49e967c5d312e0", size = 677415, upload-time = "2026-09-14T15:20:48.817Z" }, + { url = "https://files.pythonhosted.org/packages/f5/41/b3114c97c10e796010f00a30f51c81470072bca4b53e396ccca87484fcf7/greenlet-3.5.6-cp315-cp315-manylinux_2_24_s390x.manylinux_2_28_s390x.whl", hash = "sha256:9133d68624b1f2e89ec2f554d56aea8a5b0d7168cd9320200ba58d4d794845a4", size = 681337, upload-time = "2026-09-14T15:25:12.812Z" }, + { url = "https://files.pythonhosted.org/packages/fb/16/ac9e547b611539aaed1870eb1d6ddc57abdd5924b3a99bb9b5f0b44176b8/greenlet-3.5.6-cp315-cp315-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:ccadce0130fd813ec86ebfe969a6c58b42acc1d0fe55a47525375b740e07b605", size = 675927, upload-time = "2026-09-14T14:36:05.34Z" }, + { url = "https://files.pythonhosted.org/packages/48/1b/d41861c2fa00968e39e467a495ca8db9ce9b6310a5d9b57561b3d0dc48fa/greenlet-3.5.6-cp315-cp315-manylinux_2_39_riscv64.whl", hash = "sha256:5adcbbfe78bdc242c71740a02e0991cc1b2f34d33c8bb15ca45eee8fd1140942", size = 487339, upload-time = "2026-09-14T15:28:43.497Z" }, + { url = "https://files.pythonhosted.org/packages/c4/b1/b7ba08d6431121741f1d30be0d5d292e76873325179a63586cd9217b62f6/greenlet-3.5.6-cp315-cp315-musllinux_1_2_aarch64.whl", hash = "sha256:9297fb9c39b9a2c039dbcd306c410bd6906b95244dec3bba4318d36c718c164c", size = 1637236, upload-time = "2026-09-14T15:10:12.442Z" }, + { url = "https://files.pythonhosted.org/packages/af/c5/3b1cbc68f0c082022fc8717f7fe4b8b13b8d583c52352be37f4e9f55bcd2/greenlet-3.5.6-cp315-cp315-musllinux_1_2_x86_64.whl", hash = "sha256:b374e79ffa7511afc11773aef40a4ccea6191fba1c856ea2f9c56738dca69d7a", size = 1698526, upload-time = "2026-09-14T14:35:56.039Z" }, + { url = "https://files.pythonhosted.org/packages/de/56/12941ed2711400451c89d544e10f831800a2770f19dd55eac8f0f7f2003b/greenlet-3.5.6-cp315-cp315-win_amd64.whl", hash = "sha256:7969bffa322c097bd46ae595ada6a931cefda613f18ba64587e9cff4cb320756", size = 327739, upload-time = "2026-09-14T14:23:55.768Z" }, + { url = "https://files.pythonhosted.org/packages/c5/3b/576b9ed5ac929252e340cf60b4bcb6a8515350dc20797064b1922dc4ea75/greenlet-3.5.6-cp315-cp315-win_arm64.whl", hash = "sha256:8dba0129b93e7091dfefaf4cf7000172741bff7f47bf6326fcf17f32fbb54d6b", size = 311715, upload-time = "2026-09-14T14:28:25.154Z" }, + { url = "https://files.pythonhosted.org/packages/16/c2/86cfc5555a98e12b86966ddbd24fd39af32f71f2f785c6595b7feb2db156/greenlet-3.5.6-cp315-cp315t-macosx_11_0_universal2.whl", hash = "sha256:de3de000d459402cda015068fd135aa50c0bf6f2477a80d4da1e646f123b4e78", size = 306244, upload-time = "2026-09-14T14:27:57.565Z" }, + { url = "https://files.pythonhosted.org/packages/14/6d/83ffc9d05a75a80ab3a7595dbb1d9604e5d4fc2996d73a8ae2dbd1284900/greenlet-3.5.6-cp315-cp315t-manylinux_2_24_aarch64.manylinux_2_28_aarch64.whl", hash = "sha256:45663c01a4de48b9a64a2ee1509d92d1dfd3afb02b2ccfc9333029d11aef996a", size = 676578, upload-time = "2026-09-14T15:12:09.468Z" }, + { url = "https://files.pythonhosted.org/packages/5d/d6/c2cf684810e5caded075970aaadea654ecb58b8382b9aecf1d231b936894/greenlet-3.5.6-cp315-cp315t-manylinux_2_24_ppc64le.manylinux_2_28_ppc64le.whl", hash = "sha256:3deccbb57a481e3a408fe61cdfd5c13e0678fc0a30fdd09597917ca87b4be877", size = 684203, upload-time = "2026-09-14T15:20:50.261Z" }, + { url = "https://files.pythonhosted.org/packages/f2/d1/039c353d5593a97a89699e989324c9bc86af499e6c6152fe0180f5742204/greenlet-3.5.6-cp315-cp315t-manylinux_2_24_s390x.manylinux_2_28_s390x.whl", hash = "sha256:63aff70fe5aac59c72215f42ec39fcb59ff46774fa966e717f8ecb6ee2273577", size = 686023, upload-time = "2026-09-14T15:25:14.528Z" }, + { url = "https://files.pythonhosted.org/packages/62/19/00e1bee5d2af890dc8f400b54d0b0f9b489965f92bc12b407ff72cc6f469/greenlet-3.5.6-cp315-cp315t-manylinux_2_24_x86_64.manylinux_2_28_x86_64.whl", hash = "sha256:311018b46472fb26ee85870847fb89eb64cc8aaddb617400789d87076f7cfeec", size = 681253, upload-time = "2026-09-14T14:36:06.742Z" }, + { url = "https://files.pythonhosted.org/packages/8a/62/97ceb8e0b2ea96046cdf8e95b042715020ebb12d83ea0690db80a8f03d23/greenlet-3.5.6-cp315-cp315t-manylinux_2_39_riscv64.whl", hash = "sha256:520648db8fb92eef7b3e6013f5a6f901cdf0d6685f639c2f7a245879f865bef7", size = 517058, upload-time = "2026-09-14T15:28:44.924Z" }, + { url = "https://files.pythonhosted.org/packages/89/58/c9275fd0ca195d1d3402931bcce8cfcc74726ff76efb1883d229e6e1a3d7/greenlet-3.5.6-cp315-cp315t-musllinux_1_2_aarch64.whl", hash = "sha256:7f924a5a9d5890649566f2f6682e0d8ad8ca23028bacffbbac36dbd7fd680176", size = 1645988, upload-time = "2026-09-14T15:10:13.758Z" }, + { url = "https://files.pythonhosted.org/packages/e0/36/b35747582fa4f1a5453f8f3002405dbac788e450cec7674dc2d204b6ccb5/greenlet-3.5.6-cp315-cp315t-musllinux_1_2_x86_64.whl", hash = "sha256:de9923832f2d8c1a5ecd8d7260465a6ca5a86888a0d129e3bd5cf0406d2fc5bf", size = 1702383, upload-time = "2026-09-14T14:35:58.143Z" }, + { url = "https://files.pythonhosted.org/packages/ed/69/6ec22ac9351e474d2a134d0ff9400dc80362d1c20f0721088ffffdfc205b/greenlet-3.5.6-cp315-cp315t-win_amd64.whl", hash = "sha256:2ab5f42ac6c238eb71770715e6e909ad9a1a92b6c681ccb64cd5a0f07edb953f", size = 331845, upload-time = "2026-09-14T14:27:41.723Z" }, + { url = "https://files.pythonhosted.org/packages/30/cf/697c051fd534e223461fb8b523890e21a24eeca229cd50624cff6f02fabd/greenlet-3.5.6-cp315-cp315t-win_arm64.whl", hash = "sha256:f9fe868463ec7e1363733af77e38a5fda3e9b63940337048c945d69e0c80ff24", size = 315070, upload-time = "2026-09-14T14:22:21.476Z" }, +] + [[package]] name = "griffelib" version = "2.1.0" @@ -1212,6 +1302,25 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/7d/68/d8d58938dfb1370b266a1a729e6d77a985be23689a0496498ee17b2cbf90/platformdirs-4.11.0-py3-none-any.whl", hash = "sha256:360ccded2b7fce0af0ff80cc8f5942a1c5d99b0e856033acb030bfc634709e74", size = 23247, upload-time = "2026-07-21T13:09:35.422Z" }, ] +[[package]] +name = "playwright" +version = "1.62.0" +source = { registry = "https://pypi.org/simple" } +dependencies = [ + { name = "greenlet" }, + { name = "pyee" }, +] +wheels = [ + { url = "https://files.pythonhosted.org/packages/6c/5b/ca2abcf3aa69f9fb510215e3064f30b57fe57657c8d04ede45bb966d5606/playwright-1.62.0-py3-none-macosx_10_13_x86_64.whl", hash = "sha256:d8da938f3748841a8754f2e1f0216902c1c8f8ae3720de8b32ccf8e6913a7c4f", size = 43732091, upload-time = "2026-07-31T17:00:44.178Z" }, + { url = "https://files.pythonhosted.org/packages/af/1a/0bfbe9904350961f4dbb713f04342e40d548c5fc26c8157bd13617c81492/playwright-1.62.0-py3-none-macosx_11_0_arm64.whl", hash = "sha256:db755ab27db21a04186f1fe8169888e42356086e439b1059b923ef417f0b6034", size = 42510842, upload-time = "2026-07-31T17:00:48.596Z" }, + { url = "https://files.pythonhosted.org/packages/66/dc/c0486b407ad0699a250f6bbe3066fca95344009a99ca66e88ca175c69dc1/playwright-1.62.0-py3-none-macosx_11_0_universal2.whl", hash = "sha256:5108bd5b3e87169ddf269feee097da5893af7f8aea4634dfc840518d64c1f1da", size = 43732093, upload-time = "2026-07-31T17:00:52.218Z" }, + { url = "https://files.pythonhosted.org/packages/43/6b/b24aebc2b04bffcb342bccf96e287c78b363e1615bed5cea97500cc0393a/playwright-1.62.0-py3-none-manylinux1_x86_64.whl", hash = "sha256:ba33bae6a13b3d9d354c751cb618af357d20fe1d57767cbcce52079bbef17ad3", size = 47748926, upload-time = "2026-07-31T17:00:56.438Z" }, + { url = "https://files.pythonhosted.org/packages/36/43/b4b18bdc87e1949568fffdcde3ff9a0456266b2d0c6d4432cc34d89ea6eb/playwright-1.62.0-py3-none-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:db2d76613a57ad844362ce42f7d0c2fa26b19a4f7a46d4f76b891c631e6e5aff", size = 47441423, upload-time = "2026-07-31T17:01:00.404Z" }, + { url = "https://files.pythonhosted.org/packages/81/22/af5d926fc2c32a339eec00a443644bc40ab9db1dd2dd9017873c59773c0c/playwright-1.62.0-py3-none-win32.whl", hash = "sha256:e5614fa89355d7081457680324bb219f79f69c423c5cb6fa250e30b0d8aebf1c", size = 38164450, upload-time = "2026-07-31T17:01:04.187Z" }, + { url = "https://files.pythonhosted.org/packages/2b/a9/4160c1033c07af98bf841ad079457dd78408a5ee0dd56cbfe50b8b6a1c22/playwright-1.62.0-py3-none-win_amd64.whl", hash = "sha256:92c0d98ed04eb35af557b709875edba415b1f548bdb22ddb5bb3e1e6c835c2f1", size = 38164458, upload-time = "2026-07-31T17:01:08.459Z" }, + { url = "https://files.pythonhosted.org/packages/6c/ec/06b55d619a7082a766aa04f2c6bb31435c87f02930087d8a0517119408fa/playwright-1.62.0-py3-none-win_arm64.whl", hash = "sha256:ea8d3055aa9d5a9f1832ac82517bd8b42c78fac7ebcbebb0107116735c8cb6a1", size = 34208868, upload-time = "2026-07-31T17:01:11.818Z" }, +] + [[package]] name = "pluggy" version = "1.6.0" @@ -1457,6 +1566,18 @@ wheels = [ { url = "https://files.pythonhosted.org/packages/77/c1/6e422f34e569cf8e18df68d1939c81c099d2b61e4f7d9621c8a77560799c/pydantic_settings-2.14.2-py3-none-any.whl", hash = "sha256:a20c97b37910b6550d5ea50fbcc2d4187defe58cd57070b73863d069419c9440", size = 61715, upload-time = "2026-06-19T13:44:55.02Z" }, ] +[[package]] +name = "pyee" +version = "13.0.1" +source = { registry = "https://pypi.org/simple" } +dependencies = [ + { name = "typing-extensions" }, +] +sdist = { url = "https://files.pythonhosted.org/packages/8b/04/e7c1fe4dc78a6fdbfd6c337b1c3732ff543b8a397683ab38378447baa331/pyee-13.0.1.tar.gz", hash = "sha256:0b931f7c14535667ed4c7e0d531716368715e860b988770fc7eb8578d1f67fc8", size = 31655, upload-time = "2026-02-14T21:12:28.044Z" } +wheels = [ + { url = "https://files.pythonhosted.org/packages/a0/c4/b4d4827c93ef43c01f599ef31453ccc1c132b353284fc6c87d535c233129/pyee-13.0.1-py3-none-any.whl", hash = "sha256:af2f8fede4171ef667dfded53f96e2ed0d6e6bd7ee3bb46437f77e3b57689228", size = 15659, upload-time = "2026-02-14T21:12:26.263Z" }, +] + [[package]] name = "pygments" version = "2.20.0"