diff --git a/.github/workflows/docs.yml b/.github/workflows/docs.yml index 7c1dc4537c..efc834ddf4 100644 --- a/.github/workflows/docs.yml +++ b/.github/workflows/docs.yml @@ -80,7 +80,14 @@ jobs: run: ~/.elan/bin/lake build LeanPool - name: Extract declarations - run: ~/.elan/bin/lake env ~/.elan/bin/lean --run scripts/exposition/Extract.lean exposition-dump.jsonl + # Per-project environments (see extract-all.sh); 2-way parallel to + # stay inside the runner's memory. + env: + LEAN_CMD: /home/runner/.elan/bin/lean + EXTRACT_JOBS: "2" + run: >- + ~/.elan/bin/lake env bash scripts/exposition/extract-all.sh + exposition-dump.jsonl exposition-commands.jsonl - name: Install uv uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff @@ -93,6 +100,7 @@ jobs: uv sync --locked uv run python -m lean_pool.exposition \ --dump ../exposition-dump.jsonl \ + --commands ../exposition-commands.jsonl \ --repo-root .. \ --out ../exposition-site \ --commit ${{ github.sha }} @@ -161,7 +169,7 @@ jobs: # deploy matches the fresh artifact exactly (or omits the exposition # entirely on the fail-soft paths) — never a stale mixture. rm -rf docbuild/.lake/build/doc/exposition - deadline=$((SECONDS + 1800)) + deadline=$((SECONDS + 2700)) while [ "$SECONDS" -lt "$deadline" ]; do found=$(gh api "repos/${{ github.repository }}/actions/runs/${{ github.run_id }}/artifacts" \ --jq '[.artifacts[] | select(.name == "exposition-site" and .expired == false)] | length' || echo 0) diff --git a/.github/workflows/exposition-verify.yml b/.github/workflows/exposition-verify.yml new file mode 100644 index 0000000000..b998c61e0f --- /dev/null +++ b/.github/workflows/exposition-verify.yml @@ -0,0 +1,114 @@ +name: Exposition Verify + +# Compiles a minimal Lean file for every project card's main_declarations +# (the exposition's "Minimal Lean file" feature) and fails if any does not +# elaborate. Runs weekly, on demand, and on PRs touching the exposition +# pipeline — not on every content merge (the docs.yml exposition job stays +# fast; this is the correctness gate for the builder itself). + +on: + schedule: + - cron: '40 6 * * 1' + workflow_dispatch: + pull_request: + branches: + - main + paths: + - 'python/lean_pool/exposition/**' + - 'scripts/exposition/**' + - '.github/workflows/exposition-verify.yml' + +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true + +permissions: + contents: read + +jobs: + verify: + runs-on: ubuntu-latest + name: Verify minimal Lean files + steps: + - name: Checkout project + uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd + + - name: Restore caches + uses: actions/cache/restore@27d5ce7f107fe9357f9df03efb73ab90386fccae + with: + path: | + ~/.elan + .lake/packages + .lake/build + docbuild/.lake/build + key: Docs-Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json', 'docbuild/lake-manifest.json', 'LeanPool.lean') }}-${{ github.sha }} + restore-keys: | + Docs-Lake-${{ runner.os }}-${{ hashFiles('lake-manifest.json', 'docbuild/lake-manifest.json', 'LeanPool.lean') }}- + Docs-Lake-${{ runner.os }}- + + - name: Install Lean + uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 + with: + auto-config: false + use-github-cache: false + use-mathlib-cache: false + + - name: Install Mathlib cache + run: | + if [ ! -d ".lake/packages/mathlib" ]; then + ~/.elan/bin/lake exe cache get + else + echo "Mathlib already present from cache" + fi + + - name: Build pool + run: ~/.elan/bin/lake build LeanPool + + - name: Extract declarations + env: + LEAN_CMD: /home/runner/.elan/bin/lean + EXTRACT_JOBS: "2" + run: >- + ~/.elan/bin/lake env bash scripts/exposition/extract-all.sh + exposition-dump.jsonl exposition-commands.jsonl + + - name: Install uv + uses: astral-sh/setup-uv@d0d8abe699bfb85fec6de9f7adb5ae17292296ff + with: + enable-cache: true + + - name: Generate site data + run: | + cd python + uv sync --locked + uv run python -m lean_pool.exposition \ + --dump ../exposition-dump.jsonl \ + --commands ../exposition-commands.jsonl \ + --repo-root .. \ + --out ../exposition-site \ + --commit ${{ github.sha }} + + - name: Verify minimal files + run: | + # `lake env` must run from the workspace root; from python/ it + # resolves no workspace and hands `lean` an empty LEAN_PATH, which + # fails every target at `import Mathlib`. + LEAN_PATH="$(~/.elan/bin/lake env printenv LEAN_PATH)" + export LEAN_PATH + cd python + uv run python -m lean_pool.exposition.verify \ + --site ../exposition-site \ + --repo-root .. \ + --out ../exposition-verify \ + --jobs 2 \ + --lean /home/runner/.elan/bin/lean \ + --baseline 207 + + - name: Upload verification report + if: always() + uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02 + with: + name: exposition-verify-report + path: | + exposition-verify/report.json + retention-days: 30 diff --git a/.gitignore b/.gitignore index ade4808901..836a0b9621 100644 --- a/.gitignore +++ b/.gitignore @@ -4,6 +4,7 @@ # Exposition build outputs (see python/lean_pool/exposition/) /exposition-dump.jsonl +/exposition-commands.jsonl /exposition-site/ # Python diff --git a/python/lean_pool/exposition/SCHEMA.md b/python/lean_pool/exposition/SCHEMA.md index 31760d6f14..c88f30ab55 100644 --- a/python/lean_pool/exposition/SCHEMA.md +++ b/python/lean_pool/exposition/SCHEMA.md @@ -114,41 +114,48 @@ Link recipes: `doi` → `https://doi.org/`, `arxiv` → `https://arxiv.org/abs/`, `url` as-is, `github_repo` → `https://github.com/`. -### Minimal-Lean-file fields (schema 1.2, additive) +### Minimal-Lean-file fields (schema 1.3) -The shard gains `commit` (the exact commit its data was extracted from — -raw-source fetches for the minimal-file builder pin to it) and a +The minimal-file pipeline follows LMLExposition's methodology (Rémy +Degenne, github.com/LeanMachineLearning/exposition): the extractor +re-elaborates every module against the loaded environment and classifies +each top-level command from its real `Syntax`, so the builder replays +byte-exact source with pre-computed surgery edits instead of textual +heuristics. + +The shard carries `commit` (raw-source fetches pin to it) and a `moduleData` array parallel to `modules`: ```json -"moduleData": [{"imports": ["Mathlib.Order.Basic", …], // external imports - "uses": [3, 7], // same-project imports (module indices) - "contexts": [[20, "namespace Foo"], …]}, // (line, text) of replayable top-level - …] // context commands +"moduleData": [{"imports": ["Mathlib.Order.Basic", …], // external imports + "uses": [3, 7], // same-project imports (module indices) + "commands": [ … ]}, // classified top-level commands + …] ``` -`modules` may list more entries than declarations reference: modules pulled -in only through `uses` (notation-/attribute-only files) are appended so -their contexts can be replayed. - -Per-declaration additions: +All command positions are **UTF-8 byte offsets** into the module source +(the builder fetches sources as bytes and slices before decoding): ```json -"stmtEnd": [436, 69], // theorem/lemma only: statement/body boundary (line, col) -"tdeps": [124, 164], // theorem/lemma only: statement-only dependencies ⊆ deps -"span": [15, 18], // mutual members: the whole block's line span -"host": 12, // generated decls: the source declaration containing them -"prefix": "open Classical in" // bare `… in` prefix excluded from Lean's range +{"t": "d", "s": 100, "e": 420, "d": [12, 13], // declaration command: shard ids it defines + "ed": [[380, 420, ":= sorry"]], // surgery edits (theorem proof → sorry, + "un": ["LMF.termℍ"]} // by-blocks in def values → sorry) +{"t": "c", "s": 0, "e": 14, "k": "ns", // context command; k ∈ ns|end|open|var| + "ns": "Foo", "q": "Bar.Foo"} // sec|opt|univ|nota +{"t": "c", "k": "var", "b": [[s, e, ["Γ", "h"]], …]} // variable: per-binder ranges + idents +{"t": "c", "k": "nota", "kn": ["…"], "nd": [4]} // notation: kinds defined, expansion deps ``` -The minimal-file builder (`static/assets/minimal.js`, shared verbatim with -the node validation harness) follows `tdeps` through theorems (proofs become -`:= sorry`) and full `deps` elsewhere, replays module contexts in import -order, prunes `variable`/`attribute`/`export` contexts that reference -declarations outside the cone, and grows the cone with lemmas named in -`simp only [...]`-style tactic lists (invisible to term-level dependency -extraction). `build()` may return `{pending: [moduleIndex…]}` when that -closure needs sources not yet fetched; callers fetch and retry (≤ 4 rounds). +Non-exposed declarations have no entry. `tdeps` (statement-only deps ⊆ +`deps`) remains per proof-kind declaration; `"alias": true` marks alias +commands whose bodies stay verbatim (closure follows `deps`). + +The builder (`static/assets/minimal.js`, shared verbatim with the node +validation harness) is a port of LML's `assembleTarget`: dependency cone + +notation-usage closure, module replay in import order with per-binder +`variable` pruning, `open NS (…)` trimming, namespace stubs, and +empty-scope stripping. `build()` returns `{pending: [moduleIndex…]}` when +it needs module sources not yet fetched; callers fetch and retry. ## `data/index.json` diff --git a/python/lean_pool/exposition/__main__.py b/python/lean_pool/exposition/__main__.py index dd4c835c77..d00ae05ab9 100644 --- a/python/lean_pool/exposition/__main__.py +++ b/python/lean_pool/exposition/__main__.py @@ -40,11 +40,28 @@ show_default=True, help="Commit SHA recorded in index.json and used for GitHub link metadata.", ) -def cli(dump_path: Path, repo_root: Path, out_dir: Path, commit: str) -> None: +@click.option( + "--commands", + "commands_path", + type=click.Path(exists=True, dir_okay=False, path_type=Path), + default=None, + help="Extractor per-module command tables (JSONL) for the minimal-file builder.", +) +def cli( + dump_path: Path, + repo_root: Path, + out_dir: Path, + commit: str, + commands_path: Path | None, +) -> None: """Generate the static exposition site from an extractor dump.""" logging.basicConfig(level=logging.INFO, format="%(levelname)s %(message)s") summary = generate_site( - dump_path=dump_path, repo_root=repo_root, out_dir=out_dir, commit=commit + dump_path=dump_path, + repo_root=repo_root, + out_dir=out_dir, + commit=commit, + commands_path=commands_path, ) click.echo( f"Wrote {summary.projects} projects ({summary.decls} declarations, " diff --git a/python/lean_pool/exposition/generate.py b/python/lean_pool/exposition/generate.py index 8fa85a0575..4bb42e00ab 100644 --- a/python/lean_pool/exposition/generate.py +++ b/python/lean_pool/exposition/generate.py @@ -238,76 +238,71 @@ def _refined_kind_and_statement( PROOF_KINDS = frozenset({"theorem", "lemma"}) -def _attach_minimal_file_fields( - nodes: list[dict], - skeletons: dict[int, ModuleSkeleton | None], -) -> None: - """Add per-node minimal-file fields: ``span`` and ``host`` (schema 1.2). +def read_command_tables(commands_path: Path | None) -> dict[str, list[dict]]: + """Parse the extractor's per-module command tables (JSONL). - ``span`` widens a node's verbatim slice to its enclosing top-level - ``mutual`` block. ``host`` points a generated declaration (mid-line - range, blanked statement) at the human-written declaration whose source - contains it, so the builder can emit the host instead. + Returns a mapping from module name to its command entry list; empty when + no command file was provided (the minimal-file builder then has no + replay data and the frontend hides the feature). """ - by_module: dict[int, list[int]] = {} - for node_id, node in enumerate(nodes): - by_module.setdefault(node["module"], []).append(node_id) - for module_index, node_ids in by_module.items(): - skeleton = skeletons.get(module_index) - if skeleton is not None: - for start_line, end_line in skeleton.mutual_spans: - for node_id in node_ids: - node = nodes[node_id] - if start_line <= node["line"] and node["endLine"] <= end_line: - node["span"] = [start_line, end_line] - if skeleton is not None and skeleton.prefix_blocks: - # Lean's declaration range excludes a bare `open/set_option/ - # attribute … in` prefix on the preceding lines; reattach it. - # The prefix's following command may start inside the node's - # range at a later line than node["line"] when a doc comment - # sits between them, hence the range check. Chains supported. - prefix_by_next_line = { - next_line: (line, text) - for line, next_line, text in skeleton.prefix_blocks - } - for node_id in node_ids: - node = nodes[node_id] - chain_end = None - for line, next_line, text in skeleton.prefix_blocks: - if node["line"] <= next_line <= node["endLine"]: - chain_end = (line, text) - break - if chain_end is None: - continue - parts = [chain_end[1]] - cursor = chain_end[0] - while cursor in prefix_by_next_line: - line, text = prefix_by_next_line[cursor] - parts.append(text) - cursor = line - node["prefix"] = "\n".join(reversed(parts)) - for node_id in node_ids: - node = nodes[node_id] - generated = node["statement"] == "" and "stmtEnd" not in node - if not generated: + if commands_path is None: + return {} + tables: dict[str, list[dict]] = {} + with Path(commands_path).open(encoding="utf-8") as command_file: + for line in command_file: + stripped = line.strip() + if not stripped: continue - host = None - for other_id in node_ids: - other = nodes[other_id] - if other_id == node_id or other["statement"] == "": - continue - if other["line"] <= node["line"] <= other["endLine"]: - if host is None or other["line"] >= nodes[host]["line"]: - host = other_id - if host is not None: - node["host"] = host + record = json.loads(stripped) + tables[record["m"]] = record["c"] + return tables + + +def _remap_command_entries( + entries: list[dict], id_by_name: dict[str, int] +) -> list[dict]: + """Remap a module's command entries to shard-local declaration ids. + + Declaration entries whose names are all unknown (non-exposed) are + dropped — the builder skips those command spans entirely, like + LMLExposition's `skip` class. Notation expansion deps are remapped the + same way. + """ + remapped: list[dict] = [] + for entry in entries: + if entry.get("t") == "d": + ids = sorted( + {id_by_name[name] for name in entry.get("n", []) if name in id_by_name} + ) + if not ids: + continue + new_entry = { + key: value for key, value in entry.items() if key not in ("n", "sd") + } + new_entry["d"] = ids + if entry.get("sd"): + new_entry["sd"] = sorted( + { + id_by_name[name] + for name in entry["sd"] + if name in id_by_name and id_by_name[name] not in ids + } + ) + remapped.append(new_entry) + else: + new_entry = dict(entry) + if "nd" in new_entry: + new_entry["nd"] = sorted( + {id_by_name[name] for name in new_entry["nd"] if name in id_by_name} + ) + remapped.append(new_entry) + return remapped def _build_node( record: dict, kind: str, statement: str, - statement_end: tuple[int, int] | None, module_index: int, dependencies: list[int], type_dependencies: list[int] | None, @@ -325,8 +320,10 @@ def _build_node( if "d" in record: node["doc"] = record["d"] node["statement"] = statement - if statement_end is not None and kind in PROOF_KINDS: - node["stmtEnd"] = list(statement_end) + if statement.startswith("alias"): + # An `alias` keeps its body verbatim in the minimal file, so its + # closure must follow value dependencies despite the theorem kind. + node["alias"] = True if record.get("p"): node["private"] = True node["deps"] = dependencies @@ -354,22 +351,57 @@ def _closed_module_list( their skeletons too; they are appended after the declaration-bearing modules. """ - modules = list(project_modules) - known = set(modules) project_prefix = f"LeanPool.{slug}." - skeletons: dict[int, ModuleSkeleton | None] = {} - index = 0 - while index < len(modules): - source = source_cache.get(modules[index]) - skeleton = module_skeleton(source) if source else None - skeletons[index] = skeleton - if skeleton is not None: - for imported in skeleton.local_imports: - if imported.startswith(project_prefix) and imported not in known: - known.add(imported) - modules.append(imported) - index += 1 - return modules, skeletons + scanned: dict[str, ModuleSkeleton | None] = {} + + def imports_of(module: str) -> list[str]: + """Same-project imports of one module, in source order.""" + if module not in scanned: + source = source_cache.get(module) + scanned[module] = module_skeleton(source) if source else None + skeleton = scanned[module] + if skeleton is None: + return [] + return [ + imported + for imported in skeleton.local_imports + if imported.startswith(project_prefix) + ] + + def visit(root: str, placed: set[str], order: list[str]) -> None: + """Append ``root``'s import closure, each module after its imports.""" + stack = [(root, False)] + while stack: + module, expanded = stack.pop() + if module in placed: + continue + if expanded: + placed.add(module) + order.append(module) + continue + stack.append((module, True)) + for imported in reversed(imports_of(module)): + if imported not in placed: + stack.append((imported, False)) + + # The set: declaration-bearing modules closed under same-project imports. + included: set[str] = set() + for module in project_modules: + visit(module, included, []) + + # The order: Lean's own, taken by walking the project's entry module and + # emitting each module after the ones it imports. Ordering alphabetically + # instead puts unrelated modules in an order Lean never elaborates, which + # changes which instances and notations are in scope at a given point and + # can silently break assembled files. + placed: set[str] = set() + order: list[str] = [] + visit(f"LeanPool.{slug}", placed, order) + for module in project_modules: + visit(module, placed, order) + + modules = [module for module in order if module in included] + return modules, {index: scanned.get(module) for index, module in enumerate(modules)} def build_project_shard( @@ -378,8 +410,10 @@ def build_project_shard( card: ProjectCard | None, source_cache: SourceCache, commit: str = "main", + command_tables: dict[str, list[dict]] | None = None, ) -> dict: """Build one ``data/projects/.json`` payload per SCHEMA.md.""" + command_tables = command_tables or {} ordered = _sorted_records(records) declaration_modules = sorted({record["m"] for record in ordered}) modules, skeletons = _closed_module_list(slug, declaration_modules, source_cache) @@ -390,13 +424,12 @@ def build_project_shard( nodes = [] for index, record in enumerate(ordered): source = source_cache.get(record["m"]) - kind, statement, statement_end = _refined_kind_and_statement(record, source) + kind, statement, _ = _refined_kind_and_statement(record, source) nodes.append( _build_node( record, kind, statement, - statement_end, module_indices[record["m"]], dependency_lists[index], type_dependency_lists[index] if "tdeps" in record else None, @@ -404,7 +437,6 @@ def build_project_shard( layout.node_orders[index], ) ) - _attach_minimal_file_fields(nodes, skeletons) node_count = len(nodes) average = sum(layout.node_layers) / node_count if node_count else 0.0 stats = { @@ -415,6 +447,9 @@ def build_project_shard( "kinds": _kind_counts([node["kind"] for node in nodes]), } main_results = _resolve_main_results(card, nodes) + id_by_name: dict[str, int] = {} + for node_id, node in enumerate(nodes): + id_by_name.setdefault(node.get("full", node["name"]), node_id) module_data = [] for index in range(len(modules)): skeleton = skeletons[index] @@ -427,9 +462,9 @@ def build_project_shard( { "imports": skeleton.external_imports if skeleton else [], "uses": uses, - "contexts": [list(entry) for entry in skeleton.contexts] - if skeleton - else [], + "commands": _remap_command_entries( + command_tables.get(modules[index], []), id_by_name + ), } ) return { @@ -535,6 +570,7 @@ def generate_site( repo_root: Path, out_dir: Path, commit: str = "main", + commands_path: Path | None = None, static_dir: Path | None = None, templates_dir: Path | None = None, ) -> SiteSummary: @@ -555,8 +591,11 @@ def generate_site( grouped = group_records_by_project(read_dump(dump_path)) cards = load_project_cards(Path(repo_root) / "LeanPool" / "projects.yml") source_cache = SourceCache(Path(repo_root)) + command_tables = read_command_tables(commands_path) shards = { - slug: build_project_shard(slug, records, cards.get(slug), source_cache, commit) + slug: build_project_shard( + slug, records, cards.get(slug), source_cache, commit, command_tables + ) for slug, records in grouped.items() } index = build_index(shards, commit) diff --git a/python/lean_pool/exposition/source_text.py b/python/lean_pool/exposition/source_text.py index a13195ee93..e41a15cfd4 100644 --- a/python/lean_pool/exposition/source_text.py +++ b/python/lean_pool/exposition/source_text.py @@ -323,210 +323,40 @@ def _boundary_scan_start( return name_end -# Top-level commands replayed verbatim as scoping/notation context by the -# minimal-file builder. Anything else at top level is either a declaration -# (sliced through its own range) or intentionally dropped (`example`, -# `#eval`, module docstrings, ...). -CONTEXT_KEYWORDS = frozenset( - { - "namespace", - "section", - "end", - "open", - "variable", - "universe", - "set_option", - "attribute", - "export", - "deriving", - "notation", - "notation3", - "macro", - "macro_rules", - "syntax", - "elab", - "elab_rules", - "declare_syntax_cat", - "binder_predicate", - "infix", - "infixl", - "infixr", - "prefix", - "postfix", - } +# Lean's module system allows `public`/`private`/`meta` modifiers and +# `import all`. Missing them leaves a module with no recorded imports, which +# silently collapses the module ordering used to assemble minimal files. +_IMPORT_RE = re.compile( + r"^(?:(?:public|private|meta)\s+)*import\s+(?:all\s+)?([\w.«»]+)", re.MULTILINE ) -_IMPORT_RE = re.compile(r"^import\s+([\w.«»]+)", re.MULTILINE) - @dataclass class ModuleSkeleton: - """Per-module facts the minimal-file builder needs. + """Per-module import facts. + Context replay now uses the extractor's syntax-classified command + tables (SCHEMA.md schema 1.3), so only imports are scanned here. ``external_imports`` — the module's non-pool imports (Mathlib etc.). ``local_imports`` — the module's pool-internal imports (full names). - ``contexts`` — ``(line, text)`` of top-level context commands, in order. - ``mutual_spans`` — ``(start_line, end_line)`` of top-level ``mutual`` - blocks; members must be emitted as one verbatim block. - ``prefix_blocks`` — ``(line, next_line, text)`` of bare - ``open/set_option … in`` blocks whose declaration starts at - ``next_line`` (Lean's declaration range excludes such prefixes). """ external_imports: list[str] local_imports: list[str] - contexts: list[tuple[int, str]] - mutual_spans: list[tuple[int, int]] - prefix_blocks: list[tuple[int, int, str]] - - -def _block_starts(code: str) -> list[int]: - """Offsets of top-level command starts (column-0 non-blank characters).""" - starts = [0] if code and not code[0].isspace() else [] - for i in range(1, len(code)): - if code[i - 1] == "\n" and not code[i].isspace() and code[i] != "\n": - starts.append(i) - return starts - - -def _is_context_block(code: str, start: int, end: int) -> bool: - """Classify a top-level block as a replayable context command. - - ``open``/``set_option`` (and modifier-prefixed forms) can also prefix a - declaration via ``... in``; those blocks belong to the declaration and - are excluded by checking where :func:`_strip_prefixes` lands. - """ - token = _read_token(code, start, end) - if token in ("scoped", "local", "noncomputable"): - # `noncomputable section` opens a scope; `scoped notation` etc. - after = start + len(token) - while after < end and code[after] in " \t": - after += 1 - token = _read_token(code, after, end) - if token == "deriving": - # `deriving instance Foo for Bar` is a standalone command, but a - # column-0 `deriving Foo` continuation of an inductive belongs to - # that declaration's range. - after = start + len(token) - while after < end and code[after] in " \t": - after += 1 - return _read_token(code, after, end) == "instance" - if token in ("attribute", "variable") and _ends_with_in(code, start, end): - # `attribute [...] X in` / `variable … in` prefix the next declaration. - return False - if token not in CONTEXT_KEYWORDS: - return False - if token in ("open", "set_option"): - after_prefixes = _strip_prefixes(code, start, end) - keyword = _read_token(code, after_prefixes, end) - if keyword in DECLARATION_KEYWORDS: - return False - if after_prefixes >= end or not keyword: - # A bare `open … in` / `set_option … in` block is the prefix of a - # declaration starting at column 0 on the next line; the - # declaration's own range covers it. - return False - return True - - -def _ends_with_in(code: str, start: int, end: int) -> bool: - """Does this block's code end with a top-level ``in`` token?""" - j = end - while j > start and code[j - 1] in " \t\r\n": - j -= 1 - return ( - j - start >= 2 - and code[j - 2 : j] == "in" - and (j - 2 == start or not _ident_char(code[j - 3])) - ) - - -def _is_prefix_only_block(code: str, start: int, end: int) -> bool: - """Is this a bare ``open/set_option/attribute/variable … in`` prefix?""" - token = _read_token(code, start, end) - if token in ("attribute", "variable"): - return _ends_with_in(code, start, end) - if token not in ("open", "set_option"): - return False - after_prefixes = _strip_prefixes(code, start, end) - keyword = _read_token(code, after_prefixes, end) - return (after_prefixes >= end or not keyword) and _IN_RE.search( - code, start, end - ) is not None def module_skeleton(source: SourceFile) -> ModuleSkeleton: - """Scan a module for imports, context commands, and mutual blocks.""" - code = source.code - # Comments blanked but strings kept: used to trim trailing comments off a - # command without eating a final string literal (e.g. an `elab` command - # ending in an error message). - comment_view = code_view(source.text, blank_strings=False) - starts = _block_starts(code) - all_imports = _IMPORT_RE.findall(code) - external_imports = [ - module - for module in all_imports - if not (module == "LeanPool" or module.startswith("LeanPool.")) - ] - local_imports = [module for module in all_imports if module.startswith("LeanPool.")] - contexts: list[tuple[int, str]] = [] - mutual_spans: list[tuple[int, int]] = [] - prefix_blocks: list[tuple[int, int, str]] = [] - skip_until = -1 - for index, start in enumerate(starts): - end = starts[index + 1] if index + 1 < len(starts) else len(code) - if start < skip_until: - continue - first = _read_token(code, start, end) - if first == "import": - continue - if _is_prefix_only_block(code, start, end): - line, _ = source.position(start) - next_line = ( - source.position(starts[index + 1])[0] - if index + 1 < len(starts) - else line + 1 - ) - code_end = end - while code_end > start and comment_view[code_end - 1] in " \t\r\n": - code_end -= 1 - prefix_blocks.append( - (line, next_line, source.text[start:code_end].rstrip()) - ) - continue - if first == "mutual": - # The block ends at the next column-0 command, which is the - # matching bare `end`; fold it into the span and skip it. - close_end = end - if index + 1 < len(starts): - next_start = starts[index + 1] - next_end = starts[index + 2] if index + 2 < len(starts) else len(code) - if _read_token(code, next_start, next_end) == "end": - close_end = next_end - skip_until = next_end - start_line, _ = source.position(start) - last = close_end - while last > start and comment_view[last - 1] in " \t\r\n": - last -= 1 - end_line, _ = source.position(max(last - 1, start)) - mutual_spans.append((start_line, end_line)) - continue - if _is_context_block(code, start, end): - line, _ = source.position(start) - # Cut at the last code character: the raw block otherwise runs to - # the next command and swallows a following declaration's doc - # comment (blanked in the comment view, so invisible to the scan). - code_end = end - while code_end > start and comment_view[code_end - 1] in " \t\r\n": - code_end -= 1 - contexts.append((line, source.text[start:code_end].rstrip())) + """Scan a module's header for its imports.""" + all_imports = _IMPORT_RE.findall(source.code) return ModuleSkeleton( - external_imports=external_imports, - local_imports=local_imports, - contexts=contexts, - mutual_spans=mutual_spans, - prefix_blocks=prefix_blocks, + external_imports=[ + module + for module in all_imports + if not (module == "LeanPool" or module.startswith("LeanPool.")) + ], + local_imports=[ + module for module in all_imports if module.startswith("LeanPool.") + ], ) diff --git a/python/lean_pool/exposition/static/assets/graph.js b/python/lean_pool/exposition/static/assets/graph.js index 81debd56d5..aa060fa43d 100644 --- a/python/lean_pool/exposition/static/assets/graph.js +++ b/python/lean_pool/exposition/static/assets/graph.js @@ -124,7 +124,7 @@ let mainIds = []; // node ids flagged as main results (card metadata) let mainInformal = {}; // node id -> informal statement from the card let rawShard = null; // full shard JSON (minimal-file builder input) - const moduleSources = {}; // module index -> fetched raw source text + const moduleSources = {}; // module index -> raw source bytes (Uint8Array) let fullView = null; let coneView = null; @@ -1436,11 +1436,13 @@ return fetch(RAW_BASE + encodeURIComponent(commit) + '/' + path) .then((response) => { if (!response.ok) throw new Error('HTTP ' + response.status); - return response.text(); + // The shard's command tables use UTF-8 byte offsets, so sources are + // kept as raw bytes; minimal.js decodes slices with TextDecoder. + return response.arrayBuffer(); }) - .then((text) => { - moduleSources[moduleIndex] = text; - return text; + .then((buffer) => { + moduleSources[moduleIndex] = new Uint8Array(buffer); + return moduleSources[moduleIndex]; }); } @@ -1620,14 +1622,14 @@ button.disabled = true; button.textContent = 'Building…'; const cone = window.ExpoMinimal.coneIds(rawShard, id); - const needed = new Set(); + // coneIds reports every involved module (declaration modules plus + // notation-only ones); build returns {pending} as a safety net. + const needed = new Set(cone.modules || []); for (const nodeId of cone.ids) needed.add(decls[nodeId].module); const buildOnceFetched = (attempt) => Promise.all(Array.from(needed).map(fetchModuleSource)).then(() => { const result = window.ExpoMinimal.build(rawShard, moduleSources, id); if (result.pending && attempt < 4) { - // The tactic-reference closure pulled in declarations from - // modules we have not fetched yet. for (const moduleIndex of result.pending) needed.add(moduleIndex); return buildOnceFetched(attempt + 1); } diff --git a/python/lean_pool/exposition/static/assets/minimal.js b/python/lean_pool/exposition/static/assets/minimal.js index 63b00c293d..1a4d2dcdb7 100644 --- a/python/lean_pool/exposition/static/assets/minimal.js +++ b/python/lean_pool/exposition/static/assets/minimal.js @@ -3,18 +3,41 @@ * Pure logic, no DOM: exposed as window.ExpoMinimal so graph.js (browser) * and the validation harness (node) share the exact same code paths. * - * Given a project shard, the raw text of the involved modules, and a target - * declaration id, `build` assembles a standalone .lean file: the union of - * the involved modules' external imports, then each module replayed in - * original order — top-level context commands (namespace/section/open/ - * variable/notation/...) kept verbatim, needed definitions copied verbatim, - * needed theorems cut at their statement boundary with `:= sorry` — the - * whole module wrapped in a `section` so its `variable`s stay local. + * Port of LMLExposition's assembly phases (Extract.lean, Rémy Degenne, + * after Matthew Ballard's EmitStandalone.lean): external-import closure + * (`externalImports`), scope-tagged emission with empty-scope stripping + * (`ScopeTag` / `stripEmptyScopes`), blank-line collapsing + * (`collapseBlankRuns`), namespace stubs (`nsStubs`), open-only trimming + * (`restrictToTarget`). The per-command classification (LML's phase 1) + * happens ahead of time in the extractor; each shard module carries a + * `commands` table whose positions are UTF-8 BYTE offsets into the raw + * module source, so `sources` maps module index -> byte array + * (Uint8Array in the browser, Buffer in node) and every slice is decoded + * with TextDecoder after byte-slicing. * - * The dependency cone follows statement-only deps (`tdeps`) through - * theorems (their proofs become `sorry`) and full deps through everything - * else (bodies are kept). Generated declarations (deriving/@[simps]/...) - * are represented by their host declaration's source. + * Two deliberate departures from LML, driven by whole-pool validation: + * + * - `variable` commands are never pruned (LML's `pruneVariable`): dropping + * a binder silently changes every later signature. Instead binder + * references to exposed declarations outside the cone PULL those + * declarations in, and assembly runs again (at most three extra passes). + * - Notation/syntax machinery replays wholesale: every `nota` entry of an + * involved module is emitted, and any same-project import-closure module + * that defines syntax is included wholesale (all its declarations join + * the cone) — macro_rules/elab implementations only work together with + * the syntax they serve, which no per-declaration signal captures. + * + * Command-table entries (see SCHEMA.md): + * decl {t:"d", s, e, d:[declIds], ed:[[s,e,repl],…]?, un:[kind…]?, + * sd:[declIds]?} + * context {t:"c", s, e, k:"ns"|"end"|"open"|"var"|"sec"|"opt"|"univ"| + * "nota", ns?, q?, b:[[s,e,[ident…]],…]?, on:[ns,[ident…]]?, + * kn:[kind…]?, nd:[declIds]?} + * Non-exposed declarations have no entry (holes, like LML's `skip`). + * `sd` lists syntactic references from the command's kept source text + * (simp lists, reducible-inlined constants) that never surface in the + * elaborated dependencies; they are followed only when the body is + * actually emitted. */ (function (root) { "use strict"; @@ -25,441 +48,854 @@ return PROOF_KINDS[kind] === true; } - /* Walk the dependency closure from `seeds`, accumulating into - * `state = {seen, included, missingHost}`; generated declarations are - * replaced by their hosts. */ - function walkCone(shard, seeds, state) { + /* ----- byte slicing ------------------------------------------------------------ */ + + var utf8Decoder = new TextDecoder("utf-8"); + + /* Decode the byte range [start, end) of a module source. Accepts a + * Uint8Array (browser) or a node Buffer (a Uint8Array subclass); both + * support subarray and TextDecoder. */ + function decodeSlice(bytes, start, end) { + return utf8Decoder.decode(bytes.subarray(start, end)); + } + + /* Port of LML's `applyEdits`: the source bytes [start, end) with each + * edit [s, e, replacement] applied (a zero-width range is an insertion). + * Edits are non-overlapping byte ranges computed by the extractor + * (theorem proofs -> ":= sorry", by-blocks in def values -> "sorry"). */ + function applyEdits(bytes, start, end, edits) { + if (!edits || edits.length === 0) return decodeSlice(bytes, start, end); + var sorted = edits.slice().sort(function (a, b) { return a[0] - b[0]; }); + var out = ""; + var cursor = start; + for (var i = 0; i < sorted.length; i++) { + out += decodeSlice(bytes, cursor, sorted[i][0]) + sorted[i][2]; + cursor = sorted[i][1]; + } + return out + decodeSlice(bytes, cursor, end); + } + + /* Identifier-ish tokens of a piece of Lean source text. */ + function identTokens(text) { + return text.match(/[A-Za-z_À-￿][\w.'À-￿]*/g) || []; + } + + /* ----- shard indexes ----------------------------------------------------------- */ + + /* True when a node's body (value/proof) is emitted verbatim: an `alias` + * keeps its body despite its theorem kind (LML's isAlias rule), and every + * non-theorem keeps its body; theorem/lemma proofs become `sorry`. */ + function bodyEmitted(node) { + return node.alias === true || !isProofKind(node.kind); + } + + /* Dependencies to follow for a node: statement-only deps (`tdeps`) when + * the proof is sorried, full deps when the body is emitted. */ + function declDeps(node) { + if (bodyEmitted(node)) return node.deps; + return node.tdeps || node.deps; + } + + /* Index the shard's command tables: + * declToKinds[declId] -> notation kind names its command's source + * uses (LML's `declUsedNotations`); + * kindEntries[kind] -> the notation context entries defining that + * kind (matched via `kn`); + * declToSyntactic[declId] -> its command's `sd` ids: syntactic + * references from the kept source text (simp + * lists, reducible-inlined constants) that + * elaborated deps miss — followed only for + * nodes whose body is emitted. */ + function commandIndex(shard) { + var declToKinds = {}; + var kindEntries = {}; + var declToSyntactic = {}; + var moduleData = shard.moduleData || []; + for (var m = 0; m < moduleData.length; m++) { + var commands = moduleData[m].commands || []; + for (var c = 0; c < commands.length; c++) { + var entry = commands[c]; + if (entry.t === "d") { + for (var i = 0; i < entry.d.length; i++) { + if (entry.un) declToKinds[entry.d[i]] = entry.un; + if (entry.sd) declToSyntactic[entry.d[i]] = entry.sd; + } + } else if (entry.t === "c" && entry.k === "nota" && entry.kn) { + for (var k = 0; k < entry.kn.length; k++) { + (kindEntries[entry.kn[k]] = kindEntries[entry.kn[k]] || []) + .push({ module: m, entry: entry }); + } + } + } + } + return { + declToKinds: declToKinds, + kindEntries: kindEntries, + declToSyntactic: declToSyntactic, + }; + } + + /* Name-resolution index over the shard's exposed declaration names + * (the pre-port "strict matcher" semantics): + * exact[name] -> ids with exactly that (display) name; + * strict[token] -> ids whose name the token denotes: the full name, or + * a dotted suffix at a component boundary + * (`DeMorgan.verum` ~ `LO.DeMorgan.verum`); bare + * single-component tokens only match single-component + * names, since matching them against last components + * would misfire on Mathlib homonyms. Over-matching + * only grows the cone. */ + function nameIndex(shard) { + var exact = {}; + var strict = {}; + function record(map, key, id) { + (map[key] = map[key] || []).push(id); + } + for (var d = 0; d < shard.decls.length; d++) { + var parts = shard.decls[d].name.split("."); + record(exact, shard.decls[d].name, d); + for (var p = 0; p < parts.length; p++) { + if (p === 0 || p < parts.length - 1) { + record(strict, parts.slice(p).join("."), d); + } + } + } + return { exact: exact, strict: strict }; + } + + /* Shard ids an identifier token may refer to: strict-matcher hits plus + * exact hits after qualifying with each active namespace prefix. */ + function resolveToken(token, names, activePrefixes) { + var ids = matchToken(token, names, activePrefixes); + if (ids.length > 0) return ids; + // `Class.field` names a member of a declaration that is itself in the + // shard (a class projection, a structure field). The index only records + // suffixes, never a name plus an extra component, so drop trailing + // components until something resolves and pull in the owner. + var parts = token.split("."); + for (var cut = parts.length - 1; cut > 0; cut--) { + var owner = matchToken(parts.slice(0, cut).join("."), names, activePrefixes); + if (owner.length > 0) return owner; + } + return ids; + } + + function matchToken(token, names, activePrefixes) { + var ids = (names.strict[token] || []).slice(); + for (var p = 0; p < activePrefixes.length; p++) { + if (activePrefixes[p] === "") continue; + var qualified = names.exact[activePrefixes[p] + "." + token]; + if (qualified) ids = ids.concat(qualified); + } + return ids; + } + + /* Reverse instance index: declId -> instances whose dependencies include + * it. Ordinary cone members carry the instances they use inside their + * elaborated deps, but a declaration pulled in for a *source-only* + * reference (a variable binder's type, a notation body) never got + * elaborated, so the instances its type application needs (e.g. + * `PartialOrder Hollom` for a binder `{C : Set Hollom}`) must be pulled + * by association: every project instance mentioning the declaration. */ + function instanceIndex(shard) { + var instancesOf = {}; + for (var d = 0; d < shard.decls.length; d++) { + if (shard.decls[d].kind !== "instance") continue; + var deps = shard.decls[d].deps || []; + for (var i = 0; i < deps.length; i++) { + (instancesOf[deps[i]] = instancesOf[deps[i]] || []).push(d); + } + } + return instancesOf; + } + + /* ----- dependency cone --------------------------------------------------------- */ + + /* Walk the dependency closure from `seeds` into `state`; returns the ids + * newly added by this walk. Nodes whose body is emitted additionally pull + * their command's syntactic references (`sd`) — sorried theorems do not, + * since the text that mentioned them is replaced by `sorry`. */ + function walkCone(shard, seeds, state, index) { var decls = shard.decls; + var added = []; var stack = seeds.slice(); while (stack.length > 0) { var id = stack.pop(); var node = decls[id]; - if (!node) continue; - if (typeof node.host === "number") { - id = node.host; - node = decls[id]; - if (!node) continue; - } else if (node.statement === "" && node.stmtEnd === undefined) { - // Generated declaration without a source host: cannot be emitted. - if (!state.seen["m" + id]) { - state.seen["m" + id] = true; - state.missingHost.push(id); - } - continue; - } - if (state.seen[id]) continue; + if (!node || state.seen[id]) continue; state.seen[id] = true; state.included.push(id); - var deps = declDeps(node); - for (var i = 0; i < deps.length; i++) stack.push(deps[i]); + added.push(id); + var deps = declDeps(node) || []; + var i; + for (i = 0; i < deps.length; i++) stack.push(deps[i]); + if (bodyEmitted(node)) { + var syntactic = index.declToSyntactic[id] || []; + for (i = 0; i < syntactic.length; i++) stack.push(syntactic[i]); + } } + return added; } - /* Dependency cone for the minimal file. Returns shard-local ids, with - * generated declarations replaced by their hosts. */ - function coneIds(shard, targetId) { - var state = { seen: {}, included: [], missingHost: [] }; - walkCone(shard, [targetId], state); - state.included.sort(function (a, b) { return a - b; }); - return { ids: state.included, missingHost: state.missingHost }; + /* Seeds for a wholesale-included module: every declaration it exposes + * plus its notations' expansion deps. */ + function wholesaleSeeds(commands) { + var seeds = []; + for (var c = 0; c < commands.length; c++) { + var entry = commands[c]; + if (entry.t === "d") seeds = seeds.concat(entry.d); + else if (entry.k === "nota" && entry.nd) seeds = seeds.concat(entry.nd); + } + return seeds; } - /* Dependencies to follow for a node. Theorems contribute statement-only - * deps (their proofs become `sorry`) — EXCEPT mutual-block members - * (span): the whole block is emitted verbatim, proofs included, so their - * full dependencies are needed. */ - function declDeps(node) { - if (node.span) return node.deps; - return isProofKind(node.kind) && node.tdeps ? node.tdeps : node.deps; + function hasNotationEntry(commands) { + for (var c = 0; c < commands.length; c++) { + if (commands[c].t === "c" && commands[c].k === "nota") return true; + } + return false; } - /* Involved modules in emission order: the cone's modules closed under - * same-project imports (`moduleData.uses` — pulls in notation-only files - * whose context commands the cone's statements may rely on), ordered - * dependencies-first along the import DAG; ties keep module index order. */ - function moduleOrder(shard, ids) { + /* The target's transitive closure (from the target plus `extraSeeds`, + * the binder/notation references discovered by earlier assembly passes) + * plus two source-level closures: + * + * 1. Notation usage (port of the frontier loop at the end of LML's + * `writeAllExtractions`): a kept declaration whose source uses a + * notation (`un`) pulls that notation's module and expansion deps + * (`nd`) into the cone, iterated to fixpoint. + * 2. Wholesale syntax-module inclusion: any module in the involved + * modules' same-project import closure that defines syntax machinery + * (`nota` entries: notation, syntax, declare_syntax_cat, macro/elab + * rules, register_simp_attr, …) but is not yet involved is included + * wholesale — all its declarations join the cone. Tactic + * implementations and registrations only work together with the + * syntax they serve, which no per-declaration signal captures. */ + function coneInfo(shard, targetId, extraSeeds) { + var index = commandIndex(shard); var decls = shard.decls; var moduleData = shard.moduleData || []; - var involved = {}; - var queue = []; - var i; - for (i = 0; i < ids.length; i++) { - var moduleIndex = decls[ids[i]].module; - if (!involved[moduleIndex]) { - involved[moduleIndex] = true; - queue.push(moduleIndex); + var state = { seen: {}, included: [] }; + var seenKinds = {}; + var notationModules = {}; + var wholesale = {}; + var pendingIds = walkCone( + shard, [targetId].concat(extraSeeds || []), state, index); + for (;;) { + // Notation-usage fixpoint over the newly added declarations. + while (pendingIds.length > 0) { + var next = []; + for (var f = 0; f < pendingIds.length; f++) { + var kinds = index.declToKinds[pendingIds[f]] || []; + for (var k = 0; k < kinds.length; k++) { + if (seenKinds[kinds[k]]) continue; + seenKinds[kinds[k]] = true; + var defs = index.kindEntries[kinds[k]] || []; + for (var d = 0; d < defs.length; d++) { + notationModules[defs[d].module] = true; + var expansionDeps = defs[d].entry.nd || []; + next = next.concat(walkCone(shard, expansionDeps, state, index)); + } + } + } + pendingIds = next; + } + // Involved modules so far: kept declaration commands, used-notation + // modules, and previously wholesale-included modules. + var moduleSet = {}; + var i; + for (i = 0; i < state.included.length; i++) { + moduleSet[decls[state.included[i]].module] = true; + } + for (var nm in notationModules) moduleSet[nm] = true; + for (var wm in wholesale) moduleSet[wm] = true; + // Wholesale scan over the same-project import closure. + var closed = usesClosure(shard, moduleSet); + var seeds = []; + for (var cm in closed) { + // Deliberately keyed on `moduleSet`, not on a separate "already + // expanded" set. Making the rule monotone (expanding every + // syntax-defining module in the closure, even once it is involved + // for another reason) sounds more correct and measurably is not: + // it pulls in enough extra instances to break elaboration elsewhere + // — 7 targets regressed against 2 fixed when that was tried. + if (moduleSet[cm]) continue; + var commands = (moduleData[cm] || {}).commands || []; + if (!hasNotationEntry(commands)) continue; + wholesale[cm] = true; + // A syntax-only module contributes no seeds; record it as involved + // now or the zero-seed return below drops it from the emit order. + moduleSet[cm] = true; + seeds = seeds.concat(wholesaleSeeds(commands)); } + if (seeds.length === 0) { + return { + ids: state.included.slice().sort(function (a, b) { return a - b; }), + seen: state.seen, + moduleSet: moduleSet, + }; + } + pendingIds = walkCone(shard, seeds, state, index); + } + } + + /* Dependency cone for the minimal file: shard-local ids plus the module + * indices whose raw sources `build` will need (callers prefetch these; + * later assembly passes may still request more via {pending}). + * `missingHost` is retained for API compatibility; hosts are gone from + * the data (generated declarations share their command's entry). */ + function coneIds(shard, targetId) { + var info = coneInfo(shard, targetId, []); + return { + ids: info.ids, + modules: Object.keys(info.moduleSet).map(Number), + missingHost: [], + }; + } + + /* ----- module ordering and imports ---------------------------------------------- */ + + /* Project modules reachable from `moduleSet` through `moduleData.uses` + * (same-project imports), as a set. */ + function usesClosure(shard, moduleSet) { + var moduleData = shard.moduleData || []; + var closed = {}; + var queue = []; + for (var m in moduleSet) { + if (moduleSet[m]) { closed[m] = true; queue.push(Number(m)); } } while (queue.length > 0) { var current = queue.pop(); var uses = (moduleData[current] || {}).uses || []; - for (var j = 0; j < uses.length; j++) { - if (!involved[uses[j]]) { - involved[uses[j]] = true; - queue.push(uses[j]); + for (var i = 0; i < uses.length; i++) { + if (!closed[uses[i]]) { + closed[uses[i]] = true; + queue.push(uses[i]); } } } - var moduleList = Object.keys(involved).map(Number).sort(function (a, b) { + return closed; + } + + /* Emission order for the involved modules: dependencies-first along the + * import DAG, so wholesale syntax modules replay before the modules that + * use them. The topological walk runs over the full same-project import + * closure (so two involved modules connected only through a non-involved + * intermediary still order correctly — LML gets this for free from + * `env.header.moduleNames`), then keeps the involved ones. */ + function orderInvolvedModules(shard, involvedSet) { + var moduleData = shard.moduleData || []; + var closed = usesClosure(shard, involvedSet); + var closedList = Object.keys(closed).map(Number).sort(function (a, b) { return a - b; }); var placed = {}; var order = []; function place(moduleIndex, depth) { - if (placed[moduleIndex] || depth > moduleList.length) return; + if (placed[moduleIndex] || depth > closedList.length) return; placed[moduleIndex] = true; // pre-mark: cycles fall back to index order - var needs = ((moduleData[moduleIndex] || {}).uses || []) - .filter(function (m) { return involved[m]; }); + var needs = (moduleData[moduleIndex] || {}).uses || []; for (var k = 0; k < needs.length; k++) place(needs[k], depth + 1); order.push(moduleIndex); } - for (i = 0; i < moduleList.length; i++) place(moduleList[i], 0); - return order; + for (var i = 0; i < closedList.length; i++) place(closedList[i], 0); + return order.filter(function (m) { return involvedSet[m]; }); } - /* Slice a UTF-16 string prefix of `codepoints` Unicode code points. */ - function codePointPrefix(line, codepoints) { - var index = 0; - var count = 0; - while (index < line.length && count < codepoints) { - var code = line.codePointAt(index); - index += code > 0xffff ? 2 : 1; - count += 1; + /* Involved-module emission order for a cone (exported helper): the ids' + * modules, the modules defining notations they use, and — matching + * coneInfo's wholesale rule — syntax-defining modules reachable through + * same-project imports. */ + function moduleOrder(shard, ids) { + var index = commandIndex(shard); + var moduleData = shard.moduleData || []; + var involved = {}; + var kinds = {}; + var i; + for (i = 0; i < ids.length; i++) { + involved[shard.decls[ids[i]].module] = true; + var used = index.declToKinds[ids[i]] || []; + for (var k = 0; k < used.length; k++) kinds[used[k]] = true; + } + for (var kind in kinds) { + var defs = index.kindEntries[kind] || []; + for (var d = 0; d < defs.length; d++) involved[defs[d].module] = true; + } + for (;;) { + var closed = usesClosure(shard, involved); + var grew = false; + for (var cm in closed) { + if (involved[cm]) continue; + if (hasNotationEntry((moduleData[cm] || {}).commands || [])) { + involved[cm] = true; + grew = true; + } + } + if (!grew) break; } - return line.slice(0, index); + return orderInvolvedModules(shard, involved); } - function declText(node, lines) { - var startLine = node.line; - var endLine = node.endLine; - var prefix = ""; - if (node.prefix) { - // Drop `attribute [custom] X in` prefix lines whose attribute cannot - // be replayed; keep open/set_option/variable prefixes. - var prefixLines = node.prefix.split("\n").filter(function (line) { - var attr = line.match(/^\s*attribute\s*\[([^\]]*)\]/); - return !(attr && hasUnknownAttribute(attr[1])); - }); - if (prefixLines.length > 0) prefix = prefixLines.join("\n") + "\n"; - } - if (node.span) { - startLine = node.span[0]; - endLine = node.span[1]; - prefix = ""; - } else if (isProofKind(node.kind) && node.stmtEnd) { - var upto = lines.slice(startLine - 1, node.stmtEnd[0] - 1); - var boundaryLine = lines[node.stmtEnd[0] - 1] || ""; - upto.push(codePointPrefix(boundaryLine, node.stmtEnd[1])); - var statement = upto.join("\n").replace(/\s+$/, ""); - return sanitizeAttributes(prefix + statement) + " := sorry"; + /* Port of LML's `externalImports`: because project modules are emitted + * inline rather than imported, an external (Mathlib) dependency may only + * be reachable *through* a project module, so walk the same-project + * import graph transitively and union the external imports of every + * reachable module (`moduleData.imports` holds exactly each module's + * external frontier). */ + function externalImports(shard, involvedSet) { + var moduleData = shard.moduleData || []; + var closed = usesClosure(shard, involvedSet); + var seen = {}; + var result = []; + for (var m in closed) { + var imports = (moduleData[m] || {}).imports || []; + for (var i = 0; i < imports.length; i++) { + if (!seen[imports[i]]) { + seen[imports[i]] = true; + result.push(imports[i]); + } + } } - return sanitizeAttributes( - prefix + lines.slice(startLine - 1, endLine).join("\n").replace(/\s+$/, "")); + result.sort(); + return result.length > 0 ? result : ["Mathlib"]; } - /* Identifier-ish tokens of a command text (used for context pruning). */ - function identTokens(text) { - return text.match(/[A-Za-z_À-￿][\w.'À-￿]*/g) || []; + /* ----- variable binders ---------------------------------------------------------- */ + + /* The local names a `variable` binder introduces, parsed from its source + * text (port of LML's `binderBoundNames`): the identifiers before the + * first `:` (so `(a b : T)` / `{a b : T}` / `[inst : T]` give `a b` / + * `inst`), or — when there is no `:` and it is not an instance binder — + * every identifier (so `{a b}` gives `a b`). */ + function binderBoundNames(binderSrc) { + var s = binderSrc.replace(/^\s+/, ""); + var isInstance = s.charAt(0) === "["; + var colon = s.indexOf(":"); + var beforeColon = colon === -1 ? (isInstance ? "" : s) : s.slice(0, colon); + return beforeColon + .split(/[\s(){}[\],⦃⦄]+/) + .filter(function (w) { return w.length > 0; }); } - /* Attributes whose registrations ship with Lean/Mathlib. An `attribute` - * context using anything else (a project-registered attribute) cannot be - * replayed, since the registering command is not a context. */ - var KNOWN_ATTRIBUTES = { - simp: 1, instance: 1, ext: 1, norm_cast: 1, push_cast: 1, coe: 1, - reducible: 1, semireducible: 1, irreducible: 1, inline: 1, specialize: 1, - simps: 1, mono: 1, positivity: 1, gcongr: 1, fun_prop: 1, - measurability: 1, continuity: 1, aesop: 1, refl: 1, symm: 1, trans: 1, - congr: 1, to_additive: 1, default_instance: 1, match_pattern: 1, - class: 1, induction_eliminator: 1, cases_eliminator: 1, elab_as_elim: 1, - pp_nodot: 1, grind: 1, norm_num: 1, local: 1, scoped: 1, nolint: 1, - deprecated: 1, simp_nf: 1, higher_order: 1, - }; + /* ----- open-only trimming (port of restrictToTarget's openOnly logic) ----------- */ - /* Index the project's declaration names for token matching. - * `strict` — full names plus dotted suffixes at component boundaries - * (`DeMorgan.verum` ~ `LO.DeMorgan.verum`); bare single-component tokens - * only match single-component names, since matching them against last - * components would misfire on Mathlib homonyms. Used for pruning. - * `loose` — additionally last components (`coprodTree_node` ~ - * `CK.coprodTree_node`). Used for tactic-reference closure, where the - * bracket list is known to name lemmas. */ - function makeNameMatcher(shard) { - var strict = {}; // token -> [decl ids] - var loose = {}; - function record(map, key, id) { - (map[key] = map[key] || []).push(id); - } - for (var d = 0; d < shard.decls.length; d++) { - var parts = shard.decls[d].name.split("."); - for (var p = 0; p < parts.length; p++) { - var suffix = parts.slice(p).join("."); - if (p === 0 || p < parts.length - 1) record(strict, suffix, d); - record(loose, suffix, d); + /* Effective text of an `open` context entry: an `open NS (a b c)` is + * trimmed to the listed identifiers that are the short name of a kept + * declaration (or dropped entirely — null — when none are); keeping a + * name unconditionally would otherwise reference a declaration this + * target dropped. Matching by short name only can under-drop, never + * wrongly drop. Every other `open` form is kept verbatim. */ + function openEntryText(entry, bytes, keepShortNames) { + var src = decodeSlice(bytes, entry.s, entry.e); + if (!entry.on) return src; + var idents = entry.on[1] || []; + var kept = idents.filter(function (ident) { + return keepShortNames[ident] === true; + }); + if (kept.length === 0) return null; + if (kept.length === idents.length) return src; + return "open " + entry.on[0] + " (" + kept.join(" ") + ")"; + } + + /* ----- registration machinery stripping ------------------------------------------ */ + + var REGISTRATION_PATTERN = + /^\s*(register_simp_attr|register_label_attr|declare_aesop_rule_sets)\b\s*(?:\[([^\]]*)\]|([A-Za-z_À-￿][\w'À-￿]*))?/m; + + /* Attribute names registered by import-time-only commands found in the + * given module sources (`register_simp_attr foo`, `register_label_attr`, + * `declare_aesop_rule_sets [Bar]`). Such registrations run in + * initializers, so replaying them in a single file can never make the + * name usable — the commands are dropped and references to the names + * stripped instead. Scans whole sources because rule-set declarations + * often live in modules without any command-table entry. */ + function collectRegisteredNames(order, sources) { + var names = {}; + var pattern = new RegExp(REGISTRATION_PATTERN.source, "gm"); + for (var i = 0; i < order.length; i++) { + var text = decodeSlice(sources[order[i]], 0, sources[order[i]].length); + var match; + while ((match = pattern.exec(text)) !== null) { + if (match[3]) names[match[3]] = true; + if (match[2]) { + identTokens(match[2]).forEach(function (n) { names[n] = true; }); + } } } - return { strict: strict, loose: loose }; + return names; } - /* Decide whether a context command survives into the minimal file. - * - `variable`/`attribute` commands mentioning project declarations - * outside the cone are dropped (safe: a section variable actually used - * by an emitted declaration only mentions cone declarations — they - * appear in its statement's dependencies). - * - `attribute` commands using non-builtin attribute names are dropped - * (their registration command cannot be replayed). - * - `export NS (a b …)` is dropped when `NS.a` … resolve outside the - * cone. */ - /* Does an `@[...]` entry list contain a non-builtin attribute name? */ - function hasUnknownAttribute(inner) { + /* Attribute entries of a bracket group with the registered ones dropped: + * null when nothing survives, the joined entry list otherwise. */ + function filterAttributeEntries(inner, registeredNames) { var entries = inner.split(","); - for (var e = 0; e < entries.length; e++) { - var words = identTokens(entries[e].replace(/^[\s\-↓↑]+/, "")); - var attrName = words[0] === "local" || words[0] === "scoped" + var kept = entries.filter(function (entry) { + var words = identTokens(entry.replace(/^[\s←↓↑\-!]+/, "")); + var attr = words[0] === "local" || words[0] === "scoped" ? words[1] : words[0]; - if (attrName && !KNOWN_ATTRIBUTES[attrName]) return true; - } - return false; + return !(attr && registeredNames[attr] === true); + }); + if (kept.length === entries.length) return inner; + if (kept.length === 0) return null; + return kept.join(",").trim(); } - /* Drop non-builtin attributes from emitted declaration text: their - * registering command cannot be replayed, so `@[simp_isPosition]` would - * fail with "unknown attribute". */ - function sanitizeAttributes(text) { - return text.replace(/@\[([^[\]]*)\]\s*/g, function (whole, inner) { - var kept = inner.split(",").filter(function (entry) { - return !hasUnknownAttribute(entry); + /* Strip references to import-time registrations from emitted text: + * `(rule_sets := [...])` groups are removed wholesale (a project rule + * set can never exist in a single file; a Mathlib built-in one is merely + * no longer pinned, which still elaborates), `@[...]` entries naming a + * collected registered attribute are dropped (the whole group disappears + * when empty), and bare occurrences of registered names inside bracket + * lists (`simp only [simp_fixing, foo]`) are removed. */ + function stripRegistrations(text, registeredNames) { + text = text.replace(/[ \t]*\(\s*rule_sets\s*:=\s*\[[^\]]*\]\s*\)/g, ""); + text = text.replace(/@\[([^[\]]*)\][ \t]*\n?/g, function (whole, inner) { + var kept = filterAttributeEntries(inner, registeredNames); + if (kept === inner) return whole; + if (kept === null) return ""; + return "@[" + kept + "] "; + }); + return text.replace(/\[([^[\]]*)\]/g, function (whole, inner) { + if (inner.indexOf(",") === -1 && !registeredNames[inner.trim()]) { + return whole; + } + var parts = inner.split(","); + var kept = parts.filter(function (part) { + return registeredNames[part.trim()] !== true; }); - if (kept.length === 0) return ""; - if (kept.length === inner.split(",").length) return whole; - return "@[" + kept.join(",").trim() + "] "; + if (kept.length === parts.length) return whole; + return "[" + kept.join(",") + "]"; }); } - function makeContextPruner(matcher, seen) { - function outOnlyIds(ids) { - if (!ids) return false; - for (var k = 0; k < ids.length; k++) { - if (seen[ids[k]]) return false; + /* ----- synthetic context recovery ------------------------------------------------- + * + * The extractor's classifier skips some context-relevant commands + * entirely (`attribute [...] targets`, `export NS (names)`, parser + * aliases `syntax name := ...`); dropping them loses local instances + * (`attribute [local instance] Classical.propDecidable`), + * `match_pattern` attributes, exported short names, and named syntax + * parsers. The raw module bytes are available here, so recover them: + * scan for column-0 lines starting one of those commands, outside every + * known command range, extending over unbalanced brackets. */ + + var SYNTHETIC_LINE = + /^(?:attribute[ \t]*\[|export[ \t]+[A-Za-z_À-￿]|syntax[ \t]+[A-Za-z_À-￿][\w'À-￿]*[ \t]*:=|initialize_simps_projections[ \t])/; + var OPEN_IN_LINE = /^(?:scoped[ \t]+|local[ \t]+)?open[ \t].*[ \t]in[ \t]*$/; + var MACHINERY_LINE = + /^(?:syntax|notation3?|macro_rules|macro|elab_rules|elab|declare_syntax_cat|binder_predicate|attribute|export)\b/; + + function bracketBalance(text) { + var depth = 0; + for (var i = 0; i < text.length; i++) { + var ch = text.charAt(i); + if (ch === "(" || ch === "[") depth += 1; + else if (ch === ")" || ch === "]") depth -= 1; + } + return depth; + } + + function syntheticCommands(bytes, commands) { + // Split into lines with byte offsets. + var lines = []; + var start = 0; + for (var i = 0; i <= bytes.length; i++) { + if (i === bytes.length || bytes[i] === 10) { + lines.push({ s: start, e: i, text: decodeSlice(bytes, start, i) }); + start = i + 1; } - return true; } - /* nsPrefixes: enclosing namespace joins, innermost last. parentFallback: - * for reference lists (attribute/export args) a dotted token whose full - * name is unknown may be a structure/class projection — resolve its - * parent instead. */ - function mentionsOutOnly(tokens, nsPrefixes, parentFallback) { - for (var t = 0; t < tokens.length; t++) { - var token = tokens[t]; - var ids = matcher.strict[token]; - if (!ids && nsPrefixes) { - for (var p = nsPrefixes.length - 1; p >= 0 && !ids; p--) { - ids = matcher.strict[nsPrefixes[p] + "." + token]; + var sorted = commands.slice().sort(function (a, b) { return a.s - b.s; }); + var cmdIdx = 0; + var synth = []; + // Consume the command starting at line `at`: its line, unbalanced + // brackets, and indented continuation lines. Returns the end line idx. + function commandBlockEnd(at) { + var depth = bracketBalance(lines[at].text); + var last = at; + while (last + 1 < lines.length) { + var next = lines[last + 1].text; + if (depth > 0 || /^[ \t]+\S/.test(next)) { + depth += bracketBalance(next); + last += 1; + } else break; + } + return last; + } + for (var l = 0; l < lines.length; l++) { + var line = lines[l]; + if (line.text === "") continue; + while (cmdIdx < sorted.length && sorted[cmdIdx].e <= line.s) cmdIdx++; + if (cmdIdx < sorted.length && sorted[cmdIdx].s <= line.s + && line.s < sorted[cmdIdx].e) continue; // inside a known command + if (SYNTHETIC_LINE.test(line.text)) { + var last = commandBlockEnd(l); + synth.push({ t: "c", k: "synth", s: line.s, e: lines[last].e }); + l = last; + } else if (OPEN_IN_LINE.test(line.text)) { + // `open X in` wrapping a syntax-machinery command is classified as + // neither context nor declaration by the extractor — recover the + // whole block (wrapper, optional doc comment, command). + var probe = l + 1; + if (probe < lines.length && /^\/--/.test(lines[probe].text)) { + while (probe < lines.length && lines[probe].text.indexOf("-/") === -1) { + probe += 1; } + probe += 1; } - if (!ids && parentFallback && token.indexOf(".") >= 0) { - var parent = token.slice(0, token.lastIndexOf(".")); - ids = matcher.loose[parent]; + if (probe < lines.length && MACHINERY_LINE.test(lines[probe].text)) { + var blockEnd = commandBlockEnd(probe); + synth.push({ t: "c", k: "synth", s: line.s, e: lines[blockEnd].e }); + l = blockEnd; } - if (ids && outOnlyIds(ids)) return true; - } - return false; - } - return function keepContext(text, nsPrefixes) { - var exportMatch = text.match( - /^\s*export\s+([\w.'À-￿]+)\s*\(([^)]*)\)/); - if (exportMatch) { - var namespacePath = exportMatch[1]; - var members = identTokens(exportMatch[2]); - var qualified = members.map(function (member) { - return namespacePath + "." + member; - }); - // The namespace itself resolving out-of-cone also prunes (it may - // not even exist in the file without its declarations). - qualified.push(namespacePath); - return !mentionsOutOnly(qualified, nsPrefixes, true); - } - var attributeMatch = text.match( - /^\s*(?:scoped\s+|local\s+)?attribute\s*\[([^\]]*)\]/); - if (attributeMatch) { - if (hasUnknownAttribute(attributeMatch[1])) return false; - return !mentionsOutOnly(identTokens(text), nsPrefixes, true); } - if (/^\s*(?:scoped\s+|local\s+)?variable\b/.test(text)) { - return !mentionsOutOnly(identTokens(text), nsPrefixes, false); - } - return true; - }; + } + return synth; } - /* Track `namespace`/`section`/`end` context commands to know the - * enclosing namespace path at each point of a module replay. */ - function updateNamespaceStack(stack, text) { - var ns = text.match(/^\s*namespace\s+([\w.'À-￿]+)/); - if (ns) { - stack.push(ns[1]); - return; + /* ----- scope stripping and whitespace (ports of ScopeTag machinery) ------------- */ + + /* Chunk tags, port of LML's `ScopeTag`: + * openSection opens a strippable scope (`section`); + * openNamespace opens a `namespace X` scope (also strippable when it + * ends up empty — the namespace stubs already declare it); + * close `end` / `end X`; + * soft `variable` / `open` lines: content that does not, on + * its own, justify keeping its scope; + * hard declarations and any other context command. + * Chunks are {tag, text, refs?}; `refs` are candidate shard ids the + * chunk's source references (variable binders, notation bodies). */ + + /* Port of LML's `stripEmptyScopes`: drops `section` / `namespace` scopes + * whose content is only `soft` chunks (which are scoped to the dropped + * block, hence safe to remove with it). A scope is kept iff it + * transitively contains a `hard` chunk. Returns the rendered text plus + * the union of `refs` on every chunk that actually rendered — the + * inclusion pass only chases references that survived stripping. */ + function stripEmptyScopes(items) { + var stack = []; // {open, chunks[], keep} + var top = []; + for (var i = 0; i < items.length; i++) { + var item = items[i]; + if (item.tag === "openSection" || item.tag === "openNamespace") { + stack.push({ open: item, chunks: [], keep: false }); + } else if (item.tag === "close") { + if (stack.length === 0) { + top.push(item); // unbalanced (shouldn't happen): emit verbatim + } else { + var scope = stack.pop(); + if (scope.keep) { + var rendered = [scope.open].concat(scope.chunks, [item]); + if (stack.length === 0) { + top = top.concat(rendered); + } else { + var parent = stack[stack.length - 1]; + parent.chunks = parent.chunks.concat(rendered); + parent.keep = true; + } + } + // else: drop the scope (open, soft chunks, and close) entirely. + } + } else if (stack.length === 0) { + top.push(item); + } else { + stack[stack.length - 1].chunks.push(item); + if (item.tag === "hard") stack[stack.length - 1].keep = true; + } + } + // Flush any unclosed scopes verbatim (shouldn't happen). + for (var s = 0; s < stack.length; s++) { + top.push(stack[s].open); + top = top.concat(stack[s].chunks); } - if (/^\s*(?:noncomputable\s+)?section\b/.test(text)) { - stack.push(null); // section: no namespace component - return; + var text = ""; + var refs = []; + for (var t = 0; t < top.length; t++) { + text += top[t].text; + if (top[t].refs) refs = refs.concat(top[t].refs); } - if (/^\s*end\b/.test(text)) stack.pop(); + return { text: text, refs: refs }; } - function namespacePrefixes(stack) { - var prefixes = []; - var current = ""; - for (var i = 0; i < stack.length; i++) { - if (stack[i] === null) continue; - current = current ? current + "." + stack[i] : stack[i]; - prefixes.push(current); + /* Port of LML's `collapseBlankRuns`: collapse runs of two or more + * consecutive blank lines into a single blank line. */ + function collapseBlankRuns(text) { + var lines = text.split("\n"); + var out = []; + for (var i = 0; i < lines.length; i++) { + var blank = /^\s*$/.test(lines[i]); + if (blank && out.length > 0 && /^\s*$/.test(out[out.length - 1])) continue; + out.push(lines[i]); } - return prefixes; + return out.join("\n"); } - /* Namespaces mentioned by kept `open` commands; stubbed up front so the - * opens resolve even when nothing from that namespace is emitted. */ - function openedNamespaces(contextTexts) { - var found = []; - var seen = {}; - for (var i = 0; i < contextTexts.length; i++) { - var text = contextTexts[i]; - if (!/^\s*(?:scoped\s+|local\s+)?open\b/.test(text)) continue; - var body = text.replace(/^\s*(?:scoped\s+|local\s+)?open\b/, "") - .replace(/\([^)]*\)/g, " "); - var tokens = body.split(/\s+/); - for (var j = 0; j < tokens.length; j++) { - var token = tokens[j]; - if (!token || token === "scoped" || token === "hiding" - || token === "renaming" || token === "in") continue; - // Namespaces open with a capitalized or dotted path; anything else - // (prose, keywords, operators) must not become a stub. - if (!/^[A-Z\u00c0-\uffff][\w.'\u00c0-\uffff]*$/.test(token) - && token.indexOf(".") === -1) continue; - if (!/^[A-Za-z_\u00c0-\uffff][\w.'\u00c0-\uffff]*$/.test(token)) continue; - if (!seen[token]) { - seen[token] = true; - found.push(token); - } - } + /* ----- namespace stubs ------------------------------------------------------------ */ + + /* Lean keywords that must be guillemet-quoted when a namespace component + * collides with them (`namespace «Prop»`). Quoting a name that did not + * need it is always valid, so the list errs on the large side. */ + var LEAN_KEYWORDS = { + Prop: 1, Type: 1, Sort: 1, in: 1, at: 1, do: 1, by: 1, fun: 1, let: 1, + end: 1, open: 1, section: 1, namespace: 1, theorem: 1, def: 1, + instance: 1, example: 1, variable: 1, universe: 1, axiom: 1, + structure: 1, class: 1, inductive: 1, abbrev: 1, mutual: 1, match: 1, + with: 1, deriving: 1, where: 1, extends: 1, if: 1, then: 1, else: 1, + from: 1, import: 1, export: 1, notation: 1, macro: 1, syntax: 1, + attribute: 1, include: 1, omit: 1, calc: 1, show: 1, have: 1, + suffices: 1, set_option: 1, + }; + + function escapeNamespaceComponent(component) { + if (component.charAt(0) === "«") return component; + if (LEAN_KEYWORDS[component] === 1 + || !/^[A-Za-z_À-￿][\w'!?À-￿]*$/.test(component)) { + return "«" + component + "»"; } - return found; + return component; } - /* Lemma references named in tactic bracket lists of an emitted body. - * `simp only [foo]` applies rfl-lemmas definitionally, leaving no - * constant in the proof term, so the recorded dependencies miss them; - * the bracket list is the only trace. */ - function tacticReferences(text) { - var refs = []; - var pattern = - /\b(?:simp_all|simp_rw|simp|rw|rewrite|unfold|dsimp)\s+(?:only\s+)?\[([^\]]*)\]/g; - var match; - while ((match = pattern.exec(text)) !== null) { - var tokens = identTokens(match[1]); - for (var i = 0; i < tokens.length; i++) refs.push(tokens[i]); - } - return refs; + function escapeNamespacePath(path) { + return path.split(".").map(escapeNamespaceComponent).join("."); } - var TACTIC_MATCH_CAP = 5; // ambiguous tokens (many homonyms) are skipped + var OPEN_KEYWORDS = { scoped: true, hiding: true, renaming: true, in: true }; - /* Grow the cone with declarations named in emitted bodies' tactic lists. - * Mutates `state`; returns module indices whose sources are still needed - * (the caller fetches them and calls build again). */ - function expandTacticReferences(shard, sources, state, matcher, linesFor) { - var decls = shard.decls; - var pending = {}; - for (var round = 0; round < 4; round++) { - var changed = false; - var idsNow = state.included.slice(); - for (var i = 0; i < idsNow.length; i++) { - var node = decls[idsNow[i]]; - if (isProofKind(node.kind) && !node.span) continue; // body sorried - if (sources[node.module] === undefined) { - pending[node.module] = true; - continue; - } - var refs = tacticReferences(declText(node, linesFor(node.module))); - for (var r = 0; r < refs.length; r++) { - var candidates = matcher.loose[refs[r]]; - if (!candidates || candidates.length > TACTIC_MATCH_CAP) continue; - var anyCone = false; - var c; - for (c = 0; c < candidates.length; c++) { - if (state.seen[candidates[c]]) { anyCone = true; break; } - } - if (anyCone) continue; - for (c = 0; c < candidates.length; c++) { - walkCone(shard, [candidates[c]], state); - changed = true; - } - } + /* Every project namespace, taken as the proper dotted prefixes of the + * exposed declaration names (as in LML): needed to recognize lowercase + * project namespaces (`open fromModuleCatOverMatrix`) that the + * capitalized/dotted heuristic below misses. */ + function projectNamespaces(shard) { + var namespaces = {}; + for (var d = 0; d < shard.decls.length; d++) { + var parts = shard.decls[d].name.split("."); + var prefix = ""; + for (var p = 0; p < parts.length - 1; p++) { + prefix = prefix === "" ? parts[p] : prefix + "." + parts[p]; + namespaces[prefix] = true; } - if (!changed) break; } - for (var j = 0; j < state.included.length; j++) { - var moduleIndex = decls[state.included[j]].module; - if (sources[moduleIndex] === undefined) pending[moduleIndex] = true; + return namespaces; + } + + /* Namespace-looking tokens of an `open` command's text: capitalized or + * dotted identifiers (or known project namespaces of any case), with + * parenthesized short-name lists stripped. Stubbing an already-existing + * namespace (Mathlib's, or a structure's) is a no-op, so over-stubbing + * is safe — under-stubbing leaves an `open` of a namespace nothing + * re-creates, which is an error. */ + function namespaceTokens(openText, knownNamespaces) { + var body = openText.replace(/\n/g, " ").replace(/\([^)]*\)/g, " ") + .replace(/^\s*(?:scoped\s+|local\s+)?open\b/, ""); + var found = []; + var tokens = body.split(/\s+/); + for (var i = 0; i < tokens.length; i++) { + var token = tokens[i]; + if (!token || OPEN_KEYWORDS[token] === true) continue; + if (!/^[A-Za-z_À-￿][\w.'À-￿]*$/.test(token)) continue; + if (!/^[A-ZÀ-￿]/.test(token) && token.indexOf(".") === -1 + && knownNamespaces[token] !== true) continue; + found.push(token); } - return Object.keys(pending).map(Number); + return found; } - /* Assemble the minimal file. - * shard: the project shard JSON. - * sources: object mapping module index -> raw module text. - * targetId: shard-local declaration id. - * Returns {pending: [moduleIndex…]} when more sources are required. - */ - function build(shard, sources, targetId) { + /* ----- assembly ------------------------------------------------------------------- */ + + /* One assembly pass. Returns {pending} when required sources are + * missing, else {text, declarationCount, moduleCount, newIds} where + * `newIds` are exposed declarations referenced by surviving variable + * binders / notation bodies but absent from the cone — the caller + * extends the cone with them and reassembles. */ + function assemblePass(shard, sources, targetId, extraSeeds, names) { var decls = shard.decls; - var linesCache = {}; - function linesFor(moduleIndex) { - if (!linesCache[moduleIndex]) { - linesCache[moduleIndex] = (sources[moduleIndex] || "").split("\n"); + var moduleData = shard.moduleData || []; + var info = coneInfo(shard, targetId, extraSeeds); + var order = orderInvolvedModules(shard, info.moduleSet); + + var pending = order.filter(function (m) { return sources[m] === undefined; }); + if (pending.length > 0) return { pending: pending }; + + // Kept declarations' short (last-component) names, for open-only + // trimming (LML's keepShortNames in restrictToTarget). + var keepShortNames = {}; + var i; + for (i = 0; i < info.ids.length; i++) { + var parts = decls[info.ids[i]].name.split("."); + keepShortNames[parts[parts.length - 1]] = true; + } + // All names bound by `variable` binders across the involved modules: + // an identifier matching one is a local, not a reference to a + // same-named global declaration (LML's boundVars). + var boundVars = {}; + for (i = 0; i < order.length; i++) { + var commandsScan = moduleData[order[i]].commands || []; + for (var c = 0; c < commandsScan.length; c++) { + var scanEntry = commandsScan[c]; + if (scanEntry.t !== "c" || scanEntry.k !== "var") continue; + var binders = scanEntry.b || []; + for (var b = 0; b < binders.length; b++) { + var text = decodeSlice( + sources[order[i]], binders[b][0], binders[b][1]); + var bound = binderBoundNames(text); + for (var n = 0; n < bound.length; n++) boundVars[bound[n]] = true; + } } - return linesCache[moduleIndex]; - } - var state = { seen: {}, included: [], missingHost: [] }; - walkCone(shard, [targetId], state); - var matcher = makeNameMatcher(shard); - var stillNeeded = expandTacticReferences( - shard, sources, state, matcher, linesFor); - if (stillNeeded.length > 0) return { pending: stillNeeded }; - var ids = state.included.slice().sort(function (a, b) { return a - b; }); - var cone = { ids: ids, missingHost: state.missingHost }; + } + // Import-time-only registrations across the involved modules. + var registeredNames = collectRegisteredNames(order, sources); + var target = decls[targetId]; - var byModule = {}; - var i; - for (i = 0; i < ids.length; i++) { - var node = decls[ids[i]]; - (byModule[node.module] = byModule[node.module] || []).push(ids[i]); + var importList = externalImports(shard, info.moduleSet); + + // Candidate reference ids for a list of identifier tokens. + function referenceIds(tokens, activePrefixes) { + var refs = []; + for (var t = 0; t < tokens.length; t++) { + if (boundVars[tokens[t]]) continue; + refs = refs.concat(resolveToken(tokens[t], names, activePrefixes)); + } + return refs; } - var order = moduleOrder(shard, ids); - var keepContext = makeContextPruner(matcher, state.seen); - var imports = {}; - var allContexts = []; - var keptContextsByModule = {}; + // ----- namespace stubs (port of assembleTarget's nsStubs, broadened) ----- + // Entered namespaces (fully qualified `q`) plus every namespace-looking + // token of kept `open` commands and of `open … in` declaration prefix + // lines. + var knownNamespaces = projectNamespaces(shard); + var stubSeen = {}; + var stubs = []; + function addStub(namespaceName) { + if (!stubSeen[namespaceName]) { + stubSeen[namespaceName] = true; + stubs.push(namespaceName); + } + } for (i = 0; i < order.length; i++) { - var moduleData = (shard.moduleData || [])[order[i]] || {}; - (moduleData.imports || []).forEach(function (name) { - imports[name] = true; - }); - var nsStack = []; - var kept = []; - (moduleData.contexts || []).forEach(function (entry) { - if (keepContext(entry[1], namespacePrefixes(nsStack))) { - kept.push(entry); - allContexts.push(entry[1]); + var stubCommands = moduleData[order[i]].commands || []; + for (var sc = 0; sc < stubCommands.length; sc++) { + var stubEntry = stubCommands[sc]; + if (stubEntry.t === "d") { + // `open Foo in` prefix lines inside declaration commands. + var declSlice = decodeSlice( + sources[order[i]], stubEntry.s, stubEntry.e); + var prefixLines = declSlice.match( + /^[ \t]*(?:scoped\s+|local\s+)?open\s[^\n]*\sin[ \t]*$/gm) || []; + for (var pm = 0; pm < prefixLines.length; pm++) { + namespaceTokens(prefixLines[pm].replace(/\sin[ \t]*$/, ""), + knownNamespaces).forEach(addStub); + } + } else if (stubEntry.k === "ns" && stubEntry.q) { + addStub(stubEntry.q); + } else if (stubEntry.k === "open") { + var openText = openEntryText( + stubEntry, sources[order[i]], keepShortNames); + if (openText !== null) { + namespaceTokens(openText, knownNamespaces).forEach(addStub); + } } - updateNamespaceStack(nsStack, entry[1]); - }); - keptContextsByModule[order[i]] = kept; + } } - var importList = Object.keys(imports).sort(); - if (importList.length === 0) importList = ["Mathlib"]; var out = []; out.push("/- Minimal Lean file for `" + target.name + "`."); @@ -472,65 +908,268 @@ out.push(""); for (i = 0; i < importList.length; i++) out.push("import " + importList[i]); out.push(""); + // Replayed notation/macro commands may mention declarations that appear + // later in the file; defer their right-hand-side resolution to use + // sites (as in LML), and silence linters on the sorried bodies. out.push("set_option quotPrecheck false"); out.push("set_option linter.all false"); out.push(""); - - var stubs = openedNamespaces(allContexts); if (stubs.length > 0) { - out.push("-- Namespace stubs so later `open`s resolve."); + out.push("-- Namespace stubs (so later `open`s resolve)."); for (i = 0; i < stubs.length; i++) { - out.push("namespace " + stubs[i]); - out.push("end " + stubs[i]); + out.push("namespace " + escapeNamespacePath(stubs[i])); + out.push("end " + escapeNamespacePath(stubs[i])); } out.push(""); } + var header = out.join("\n") + "\n"; + // Per-module tagged chunks (port of assembleTarget's items loop). + // activePrefixes accumulates across modules and is never popped — an + // over-approximation of scope used only for name resolution ("" is + // LML's Name.anonymous root). + var items = []; + var activePrefixes = [""]; + var emittedModules = 0; for (i = 0; i < order.length; i++) { var moduleIndex = order[i]; - var moduleName = shard.modules[moduleIndex]; - var needed = (byModule[moduleIndex] || []).slice(); - var keptContexts = keptContextsByModule[moduleIndex] || []; - // Context-only modules (no cone declarations) are replayed for their - // notation/attribute commands; skip them when nothing survives. - if (needed.length === 0 && keptContexts.length === 0) continue; - var source = sources[moduleIndex]; - if (needed.length > 0 && source === undefined) continue; - var lines = source === undefined ? [] : source.split("\n"); - var events = []; - var k; - for (k = 0; k < keptContexts.length; k++) { - events.push({ line: keptContexts[k][0], text: keptContexts[k][1] }); + var bytes = sources[moduleIndex]; + var commands = (moduleData[moduleIndex].commands || []) + .concat(syntheticCommands(bytes, moduleData[moduleIndex].commands || [])) + .sort(function (a, b) { return a.s - b.s; }); + emittedModules += 1; + items.push({ tag: "hard", + text: "\n-- ═══ " + shard.modules[moduleIndex] + " ═══\n" }); + // Wrap each module's replayed content in its own `section` so its + // `open`s stay local to it (as in the original project) instead of + // piling up across modules — repeated `open Foo`s can make an + // unqualified name ambiguous through redundant open-paths. + items.push({ tag: "openSection", text: "section\n" }); + // Typed scope stack for `end` synthesis: one frame per open scope — + // section frames (with the section name when present), one frame per + // dotted namespace component. Reset per module. + var scopeStack = []; + for (c = 0; c < commands.length; c++) { + var entry = commands[c]; + if (entry.t === "d") { + // restrictToTarget: emit iff the command defines a kept + // declaration (any of its ids — mutual blocks and generated + // instances share one command). + var keep = false; + for (var kd = 0; kd < entry.d.length; kd++) { + if (info.seen[entry.d[kd]]) { keep = true; break; } + } + if (!keep) continue; + var declBody = stripRegistrations( + applyEdits(bytes, entry.s, entry.e, entry.ed), registeredNames); + items.push({ tag: "hard", text: "\n" + declBody + "\n\n" }); + } else if (entry.k === "ns") { + // Track the namespace for name resolution — as spelled, fully + // qualified (`q`), and as the current nesting join (so a short + // name inside `namespace A` + `namespace B` resolves against + // `A.B.`) — then open one synthesized scope per dotted + // component so every scope has a self-contained open/close pair + // no matter which inner scopes stripEmptyScopes later drops. + if (entry.ns) { + activePrefixes.push(entry.ns); + if (entry.q && entry.q !== entry.ns) activePrefixes.push(entry.q); + var nsComponents = entry.ns.split("."); + for (var nc = 0; nc < nsComponents.length; nc++) { + scopeStack.push({ section: false, name: nsComponents[nc] }); + items.push({ tag: "openNamespace", + text: "namespace " + + escapeNamespaceComponent(nsComponents[nc]) + "\n" }); + } + var nestingJoin = scopeStack + .filter(function (fr) { return !fr.section && fr.name; }) + .map(function (fr) { return fr.name; }) + .join("."); + if (nestingJoin !== entry.ns) activePrefixes.push(nestingJoin); + } else { + scopeStack.push({ section: false, name: null }); + items.push({ tag: "openNamespace", + text: decodeSlice(bytes, entry.s, entry.e) + "\n" }); + } + } else if (entry.k === "sec") { + var secText = decodeSlice(bytes, entry.s, entry.e); + // Module-system scaffolding cannot appear in a plain single file: + // reduce `@[expose] public section` / `public section` to a plain + // `section` (keeps the scope balanced). + if (/(?:^|\s)public\s+section/.test(secText) + || /^\s*@\[expose\]/.test(secText)) { + secText = "section"; + } + // A named `section Foo` must close with `end Foo`: remember the + // name for the synthesized close. A dotted `section A.B` opens one + // scope per component just like `namespace A.B` does, so split it — + // otherwise the matching `end A.B` pops two frames while only one + // was pushed, stealing the enclosing namespace's frame. + var secMatch = secText.match(/section\s+([^\s]+)\s*$/); + var secName = secMatch ? secMatch[1] : null; + if (secName && secName.indexOf(".") !== -1) { + var secComponents = secName.split("."); + var secPrefix = secText.slice(0, secMatch.index); + for (var sc = 0; sc < secComponents.length; sc++) { + scopeStack.push({ section: true, name: secComponents[sc] }); + items.push({ tag: "openSection", + text: (sc === 0 ? secPrefix : "") + "section " + + escapeNamespaceComponent(secComponents[sc]) + "\n" }); + } + } else { + scopeStack.push({ section: true, name: secName }); + items.push({ tag: "openSection", text: secText + "\n" }); + } + } else if (entry.k === "end") { + // Never slice `end` text from the source: pop one typed frame per + // dotted component (a bare `end` pops one) and synthesize each + // frame's own close line, innermost first — `end A.B` becomes + // `end B` + `end A`. Per-frame lines keep every open/close pair + // intact when stripEmptyScopes drops an inner scope but keeps an + // outer one. + var popCount = entry.ns ? entry.ns.split(".").length : 1; + for (var ec = 0; ec < popCount && scopeStack.length > 0; ec++) { + var frame = scopeStack.pop(); + items.push({ tag: "close", + text: frame.name + ? "end " + escapeNamespaceComponent(frame.name) + "\n" + : "end\n" }); + } + } else if (entry.k === "open") { + var effective = openEntryText(entry, bytes, keepShortNames); + if (effective === null) continue; // open-only with nothing kept + // Every token may name a namespace brought into scope (an + // over-approximation, as in LML: only exact-name matches use it). + var tokens = effective.replace(/\n/g, " ").split(" "); + for (var t = 0; t < tokens.length; t++) { + if (tokens[t] !== "") activePrefixes.push(tokens[t]); + } + // `open NS hiding a b` / `renaming a -> b` name declarations that + // must exist: resolve and pull them like binder references. + items.push({ + tag: "soft", + text: effective + "\n", + refs: referenceIds(identTokens(effective), activePrefixes), + }); + } else if (entry.k === "var") { + // Never prune binders (dropping one silently changes every later + // signature); references to out-of-cone declarations are pulled + // into the cone by the multi-pass caller instead (via refs). + var varIdents = []; + var varBinders = entry.b || []; + for (var vb = 0; vb < varBinders.length; vb++) { + varIdents = varIdents.concat(varBinders[vb][2] || []); + } + items.push({ + tag: "soft", + text: decodeSlice(bytes, entry.s, entry.e) + "\n", + refs: referenceIds(varIdents, activePrefixes), + }); + } else if (entry.k === "nota") { + var notaText = decodeSlice(bytes, entry.s, entry.e); + // Import-time-only registrations can never take effect inside a + // single file: drop them (references are stripped instead). + if (REGISTRATION_PATTERN.test(notaText)) continue; + // Extractor quirk: a `declare_syntax_cat` slice can end right + // after the keyword; recover the category name from `kn`. + if (/declare_syntax_cat\s*$/.test(notaText) + && entry.kn && entry.kn.length === 1) { + notaText += " " + + entry.kn[0].replace(/\.quot$/, "").split(".").pop(); + } + notaText = stripRegistrations(notaText, registeredNames); + // Replay ALL syntax machinery of involved modules: macro_rules / + // elab_rules only work together with the syntax/categories they + // extend, and quotPrecheck false defers unused right-hand sides. + // Identifier tokens feed the inclusion pass so expansions' + // helpers exist when the notation is actually used. + items.push({ + tag: "hard", + text: "\n" + notaText + "\n\n", + refs: referenceIds(identTokens(notaText), activePrefixes), + }); + } else if (entry.k === "synth") { + // Recovered commands the extractor's classifier skipped: + // `attribute [...] targets`, `export NS (names)`, + // `syntax name := ...` (see syntheticCommands). + // Remove `(rule_sets := [...])` groups FIRST so the attribute + // bracket group has no nested brackets left to confuse parsing. + var synthText = decodeSlice(bytes, entry.s, entry.e) + .replace(/[ \t]*\(\s*rule_sets\s*:=\s*\[[^\]]*\]\s*\)/g, ""); + var attrMatch = synthText.match(/^attribute[ \t]*\[([^\]]*)\]([\s\S]*)$/); + if (attrMatch) { + var keptEntries = filterAttributeEntries(attrMatch[1], registeredNames); + if (keptEntries === null) continue; // only registered attrs + synthText = "attribute [" + keptEntries + "]" + attrMatch[2]; + } + items.push({ + tag: "hard", + text: synthText + "\n", + refs: referenceIds(identTokens(synthText), activePrefixes), + }); + } else { + // "opt", "univ" (and anything future): hard context, verbatim. + items.push({ tag: "hard", + text: decodeSlice(bytes, entry.s, entry.e) + "\n" }); + } } - var emittedSpans = {}; - for (k = 0; k < needed.length; k++) { - var entry = decls[needed[k]]; - var spanKey = entry.span ? entry.span.join(":") : "d" + needed[k]; - if (emittedSpans[spanKey]) continue; - emittedSpans[spanKey] = true; - events.push({ - line: entry.span ? entry.span[0] : entry.line, - text: declText(entry, lines), - }); + // Close any scopes the source left open (defensive: module sources + // are balanced) so the module wrapper's `end` pairs correctly. + while (scopeStack.length > 0) { + var leftover = scopeStack.pop(); + items.push({ tag: "close", + text: leftover.name ? "end " + leftover.name + "\n" : "end\n" }); } - events.sort(function (a, b) { return a.line - b.line; }); - out.push("-- ═══ " + moduleName + " ═══"); - out.push("section"); - for (k = 0; k < events.length; k++) { - out.push(events[k].text); - out.push(""); + items.push({ tag: "close", text: "end\n" }); + } + + var body = stripEmptyScopes(items); + var newIds = []; + var newSeen = {}; + for (i = 0; i < body.refs.length; i++) { + var ref = body.refs[i]; + if (!info.seen[ref] && !newSeen[ref]) { + newSeen[ref] = true; + newIds.push(ref); } - out.push("end"); - out.push(""); } + return { + text: collapseBlankRuns(header + body.text).replace(/\s+$/, "") + "\n", + declarationCount: info.ids.length, + moduleCount: emittedModules, + newIds: newIds, + }; + } + /* Assemble the minimal file. + * shard: the project shard JSON. + * sources: module index -> raw source bytes (Uint8Array or Buffer). + * targetId: shard-local declaration id. + * Returns {pending: [moduleIndex…]} when required sources are missing. + * Runs up to three extra passes: references from surviving variable + * binders / notation bodies extend the cone, then assembly reruns. */ + function build(shard, sources, targetId) { + var names = nameIndex(shard); + var instancesOf = instanceIndex(shard); + var extraSeeds = []; + var result = null; + for (var pass = 0; pass < 8; pass++) { + result = assemblePass(shard, sources, targetId, extraSeeds, names); + if (result.pending) return { pending: result.pending }; + if (result.newIds.length === 0) break; + // Source-only references never got elaborated, so pull the project + // instances mentioning them along (their types need those to + // re-elaborate here). + var expanded = result.newIds.slice(); + for (var n = 0; n < result.newIds.length; n++) { + expanded = expanded.concat(instancesOf[result.newIds[n]] || []); + } + extraSeeds = extraSeeds.concat(expanded); + } return { - text: out.join("\n"), - declarationCount: ids.length, - moduleCount: order.length, - missingHost: cone.missingHost.map(function (id) { - return decls[id] ? decls[id].name : String(id); - }), + text: result.text, + declarationCount: result.declarationCount, + moduleCount: result.moduleCount, + missingHost: [], // hosts are gone from the data; kept for callers }; } diff --git a/python/lean_pool/exposition/verify.py b/python/lean_pool/exposition/verify.py new file mode 100644 index 0000000000..33254df1dd --- /dev/null +++ b/python/lean_pool/exposition/verify.py @@ -0,0 +1,258 @@ +"""Verify that minimal Lean files really compile. + +Assembles a minimal file for every target (default: each project card's +``main_declarations``) with the same builder module the browser uses +(``scripts/exposition/build-minimal.mjs``), then compiles each with +``lean`` against the built pool/Mathlib. A file passes when ``lean`` exits +zero and reports nothing beyond ``declaration uses 'sorry'`` warnings. + +Run from ``python/`` with a generated site and LEAN_PATH set (or via +``lake env``):: + + uv run python -m lean_pool.exposition.verify \ + --site --repo-root .. --out [--jobs 3] +""" + +from __future__ import annotations + +import json +import logging +import subprocess +import sys +from concurrent.futures import ThreadPoolExecutor +from dataclasses import dataclass +from pathlib import Path + +import click +import yaml + +logger = logging.getLogger(__name__) + +COMPILE_TIMEOUT_SECONDS = 600 + + +@dataclass +class Target: + """One declaration to verify.""" + + project: str + name: str + + +@dataclass +class Outcome: + """Build + compile result for one target.""" + + target: Target + stage: str # "pass" | "resolve" | "build" | "compile" | "timeout" + detail: str = "" + + +def main_declaration_targets(repo_root: Path, site_dir: Path) -> list[Target]: + """Every project card ``main_declarations`` entry with a generated shard.""" + registry = yaml.safe_load( + (repo_root / "LeanPool" / "projects.yml").read_text(encoding="utf-8") + ) + targets: list[Target] = [] + for entry in registry.get("projects", []): + entry_module = entry.get("entry_module") or "" + if not entry_module: + continue + slug = entry_module.split(".")[-1] + if not (site_dir / "data" / "projects" / f"{slug}.json").is_file(): + logger.warning("no shard for project %s; skipping its targets", slug) + continue + for name in entry.get("main_declarations") or []: + targets.append(Target(project=slug, name=name)) + return targets + + +def _build_one( + repo_root: Path, site_dir: Path, out_dir: Path, index: int, target: Target +) -> tuple[Path | None, Outcome | None]: + """Assemble one minimal file; return (path, failure-outcome).""" + out_file = ( + out_dir / f"{index:03d}-{target.project}-{target.name.replace('.', '_')}.lean" + ) + result = subprocess.run( + [ + "node", + str(repo_root / "scripts" / "exposition" / "build-minimal.mjs"), + str(site_dir), + str(repo_root), + target.project, + target.name, + str(out_file), + ], + capture_output=True, + text=True, + check=False, + ) + if result.returncode == 2: + return None, Outcome(target, "resolve", result.stderr.strip()[:200]) + if result.returncode != 0: + return None, Outcome(target, "build", result.stderr.strip()[:200]) + return out_file, None + + +def _compile_one(lean_command: str, target: Target, path: Path) -> Outcome: + """Compile one assembled file; only sorry warnings may remain.""" + try: + result = subprocess.run( + [lean_command, str(path)], + capture_output=True, + text=True, + timeout=COMPILE_TIMEOUT_SECONDS, + check=False, + ) + except subprocess.TimeoutExpired: + return Outcome(target, "timeout") + output = (result.stdout + result.stderr).strip() + real_lines = [ + line + for line in output.splitlines() + if line.strip() + and "declaration uses `sorry`" not in line + and "declaration uses 'sorry'" not in line + ] + if result.returncode == 0 and not real_lines: + return Outcome(target, "pass") + return Outcome(target, "compile", "\n".join(real_lines[:6])[:500]) + + +def preflight(lean_command: str, out_dir: Path) -> str | None: + """Check that ``lean`` can see Mathlib; return an error message if it cannot. + + Without this, a missing LEAN_PATH makes every single target fail at + ``import Mathlib`` and the report reads as a pipeline regression rather + than a broken environment. + """ + probe = out_dir / "_preflight.lean" + probe.write_text("import Mathlib\n") + try: + result = subprocess.run( + [lean_command, str(probe)], + capture_output=True, + text=True, + timeout=COMPILE_TIMEOUT_SECONDS, + check=False, + ) + except (subprocess.TimeoutExpired, OSError) as error: + return f"could not run `{lean_command}`: {error}" + finally: + probe.unlink(missing_ok=True) + if result.returncode != 0: + return ( + "`lean` cannot import Mathlib — LEAN_PATH is unset or wrong.\n" + "Run under `lake env` from the repository root, e.g.\n" + ' export LEAN_PATH="$(lake env printenv LEAN_PATH)"\n' + f"lean said: {(result.stdout + result.stderr).strip()[:300]}" + ) + return None + + +@click.command() +@click.option( + "--site", + "site_dir", + type=click.Path(exists=True, file_okay=False, path_type=Path), + required=True, + help="Generated exposition site directory (with data/projects/).", +) +@click.option( + "--repo-root", + "repo_root", + type=click.Path(exists=True, file_okay=False, path_type=Path), + required=True, + help="Repository root (sources + scripts/exposition/).", +) +@click.option( + "--out", + "out_dir", + type=click.Path(file_okay=False, path_type=Path), + required=True, + help="Work directory for assembled files and the report.", +) +@click.option("--jobs", default=3, show_default=True, help="Concurrent lean compiles.") +@click.option( + "--lean", "lean_command", default="lean", show_default=True, help="lean binary." +) +@click.option( + "--limit", default=0, show_default=True, help="Verify only the first N targets." +) +@click.option( + "--baseline", + default=0, + show_default=True, + help="Minimum passing count to accept; 0 requires every target to pass.", +) +def cli( + site_dir: Path, + repo_root: Path, + out_dir: Path, + jobs: int, + lean_command: str, + limit: int, + baseline: int, +) -> None: + """Assemble and compile minimal files for every main declaration.""" + logging.basicConfig(level=logging.INFO, format="%(levelname)s %(message)s") + out_dir.mkdir(parents=True, exist_ok=True) + environment_error = preflight(lean_command, out_dir) + if environment_error: + raise click.ClickException(environment_error) + targets = main_declaration_targets(repo_root, site_dir) + if limit: + targets = targets[:limit] + click.echo(f"verifying {len(targets)} minimal files") + + outcomes: list[Outcome] = [] + compile_queue: list[tuple[Target, Path]] = [] + for index, target in enumerate(targets): + path, failure = _build_one(repo_root, site_dir, out_dir, index, target) + if failure: + outcomes.append(failure) + elif path: + compile_queue.append((target, path)) + + with ThreadPoolExecutor(max_workers=jobs) as pool: + outcomes.extend( + pool.map(lambda item: _compile_one(lean_command, *item), compile_queue) + ) + + passed = sum(1 for outcome in outcomes if outcome.stage == "pass") + report = { + "total": len(targets), + "passed": passed, + "failures": [ + { + "project": outcome.target.project, + "name": outcome.target.name, + "stage": outcome.stage, + "detail": outcome.detail, + } + for outcome in outcomes + if outcome.stage != "pass" + ], + } + (out_dir / "report.json").write_text(json.dumps(report, indent=2)) + for failure in report["failures"]: + click.echo(f"FAIL [{failure['stage']}] {failure['project']}/{failure['name']}") + click.echo(f"passed {passed}/{len(targets)} (report: {out_dir / 'report.json'})") + if passed == len(targets): + return + if baseline and passed >= baseline: + click.echo( + f"at or above the {baseline} baseline; {len(targets) - passed} still " + "fail — see report.json" + ) + if passed > baseline: + click.echo(f"raise --baseline to {passed} to lock in the gain") + return + if baseline: + click.echo(f"REGRESSION: {passed} passing is below the {baseline} baseline") + sys.exit(1) + + +if __name__ == "__main__": + cli() diff --git a/python/tests/test_exposition_generate.py b/python/tests/test_exposition_generate.py index 7281a91f84..74f88719c6 100644 --- a/python/tests/test_exposition_generate.py +++ b/python/tests/test_exposition_generate.py @@ -143,8 +143,8 @@ def a3 : Nat := ] -def _write_inputs(tmp_path: Path) -> tuple[Path, Path, Path, Path]: - """Create the fake repo, static, templates, and dump under tmp_path.""" +def _write_inputs(tmp_path: Path) -> tuple[Path, Path, Path, Path, Path]: + """Create the fake repo, static, templates, dump, and commands files.""" repo = tmp_path / "repo" (repo / "LeanPool" / "Alpha").mkdir(parents=True) (repo / "LeanPool" / "Alpha" / "One.lean").write_text(ALPHA_ONE) @@ -162,19 +162,48 @@ def _write_inputs(tmp_path: Path) -> tuple[Path, Path, Path, Path]: (templates / "project.html").write_text(TEMPLATE) dump = tmp_path / "dump.jsonl" dump.write_text("\n".join(json.dumps(record) for record in RECORDS) + "\n") - return repo, static, templates, dump + commands = tmp_path / "commands.jsonl" + commands.write_text( + json.dumps( + { + "m": "LeanPool.Alpha.One", + "c": [ + {"t": "c", "s": 0, "e": 10, "k": "ns", "ns": "A", "q": "A"}, + { + "t": "d", + "s": 0, + "e": 26, + "n": ["a1"], + "ed": [[17, 26, ":= sorry"]], + }, + {"t": "d", "s": 30, "e": 40, "n": ["NotExposed.x"]}, + { + "t": "c", + "s": 50, + "e": 60, + "k": "nota", + "kn": ["Alpha.termX"], + "nd": ["a3", "Unknown.y"], + }, + ], + } + ) + + "\n" + ) + return repo, static, templates, dump, commands @pytest.fixture def site(tmp_path: Path) -> tuple[Path, SiteSummary]: """Generate the site from the synthetic dump; return (out_dir, summary).""" - repo, static, templates, dump = _write_inputs(tmp_path) + repo, static, templates, dump, commands = _write_inputs(tmp_path) out = tmp_path / "out" summary = generate_site( dump, repo, out, commit="deadbeef", + commands_path=commands, static_dir=static, templates_dir=templates, ) @@ -234,6 +263,29 @@ def test_project_shard_schema_and_stats(site: tuple[Path, SiteSummary]) -> None: assert shard["decls"][1]["deps"] == [0] +def test_command_tables_remapped(site: tuple[Path, SiteSummary]) -> None: + """ModuleData carries command entries with names remapped to shard ids.""" + out, _ = site + shard = _load(out, "data/projects/Alpha.json") + module_data = shard["moduleData"] + assert [set(row) for row in module_data] == [ + {"imports", "uses", "commands"} for _ in module_data + ] + one = module_data[0]["commands"] + # The a1 decl command: names remapped to ids, unknown names dropped. + decl_entries = [entry for entry in one if entry["t"] == "d"] + assert decl_entries[0]["d"] == [0] + assert "n" not in decl_entries[0] + assert decl_entries[0]["ed"] == [[17, 26, ":= sorry"]] + # The non-exposed decl command was dropped entirely. + assert all(entry["d"] for entry in decl_entries) + # Context entry passes through; notation deps are remapped. + context_entries = [entry for entry in one if entry["t"] == "c"] + assert context_entries[0]["k"] == "ns" + nota = [entry for entry in one if entry.get("k") == "nota"][0] + assert nota["nd"] == [2] + + def test_card_and_main_results(site: tuple[Path, SiteSummary]) -> None: """Shards carry the registry card and resolved main results (schema 1.1).""" out, _ = site @@ -292,10 +344,8 @@ def test_declaration_nodes(site: tuple[Path, SiteSummary]) -> None: "order", "main", # a3 is one of the card's main declarations ] - # a1 is a lemma: it carries the statement boundary and type-only deps. - assert alpha[0]["stmtEnd"] == [1, 16] # the `:=` in `lemma a1 : True := …` + # a1 is a lemma: it carries statement-only deps for the minimal builder. assert alpha[0]["tdeps"] == [] - assert "stmtEnd" not in alpha[2] # defs keep their bodies — no boundary field beta = _load(out, "data/projects/Beta.json")["decls"] b3 = beta[2] assert b3["full"] == "_private.LeanPool.Beta.0.b3" @@ -309,7 +359,6 @@ def test_declaration_nodes(site: tuple[Path, SiteSummary]) -> None: "line", "endLine", "statement", - "stmtEnd", "private", "deps", "ext", @@ -390,7 +439,7 @@ def test_static_copy_and_project_pages(site: tuple[Path, SiteSummary]) -> None: def test_missing_static_directory_raises(tmp_path: Path) -> None: """A missing static directory fails loudly instead of emitting a site.""" - repo, _, templates, dump = _write_inputs(tmp_path) + repo, _, templates, dump, _commands = _write_inputs(tmp_path) with pytest.raises(FileNotFoundError, match="static asset directory"): generate_site( dump, @@ -399,3 +448,23 @@ def test_missing_static_directory_raises(tmp_path: Path) -> None: static_dir=tmp_path / "no-such-static", templates_dir=templates, ) + + +def test_module_order_follows_imports_not_alphabet(tmp_path: Path) -> None: + """Modules are emitted after the modules they import, in source order. + + Ordering alphabetically instead puts unrelated modules in an order Lean + never elaborates, which changes which instances and notations are in + scope and can silently break the assembled minimal file. + """ + from lean_pool.exposition.generate import SourceCache, _closed_module_list + + repo = tmp_path / "repo" + (repo / "LeanPool" / "Zeta").mkdir(parents=True) + # Alphabetically Apex < Zulu, but Zulu is imported by Apex. + (repo / "LeanPool" / "Zeta" / "Zulu.lean").write_text("def z : Nat := 0\n") + (repo / "LeanPool" / "Zeta" / "Apex.lean").write_text( + "public import LeanPool.Zeta.Zulu\ndef a : Nat := z\n" + ) + modules, _ = _closed_module_list("Zeta", ["LeanPool.Zeta.Apex"], SourceCache(repo)) + assert modules == ["LeanPool.Zeta.Zulu", "LeanPool.Zeta.Apex"] diff --git a/python/tests/test_exposition_source_text.py b/python/tests/test_exposition_source_text.py index 19b48a2f99..44cbf42a7b 100644 --- a/python/tests/test_exposition_source_text.py +++ b/python/tests/test_exposition_source_text.py @@ -48,8 +48,8 @@ def test_theorem_with_assignment_boundary() -> None: assert statement_end == (4, 14) -def test_module_skeleton_contexts_imports_and_mutual() -> None: - """module_skeleton collects imports, context commands, and mutual spans.""" +def test_module_skeleton_imports() -> None: + """module_skeleton splits external and pool-internal imports.""" text = ( "import Mathlib.Order.Basic\n" "import LeanPool.Other.Module\n" @@ -57,43 +57,32 @@ def test_module_skeleton_contexts_imports_and_mutual() -> None: "/-! Module doc: skipped. -/\n" "\n" "namespace Demo\n" - "\n" - "open Finset in\n" - "theorem uses_prefix : True := trivial\n" - "\n" - "variable {n : Nat}\n" - "open Nat\n" - 'notation "⟪" x "⟫" => id x\n' - "\n" - "mutual\n" - " def even : Nat → Bool | 0 => true | n + 1 => odd n\n" - " def odd : Nat → Bool | 0 => false | n + 1 => even n\n" - "end\n" - "\n" + "def x : Nat := 1\n" "end Demo\n" ) skeleton = module_skeleton(SourceFile.from_text(text)) assert skeleton.external_imports == ["Mathlib.Order.Basic"] - assert all("skipped" not in t for _, t in skeleton.contexts) - context_texts = [entry[1] for entry in skeleton.contexts] - assert context_texts == [ - "namespace Demo", - "variable {n : Nat}", - "open Nat", - 'notation "⟪" x "⟫" => id x', - "end Demo", - ] - assert skeleton.contexts[0][0] == 6 # namespace Demo sits on line 6 - assert skeleton.mutual_spans == [(15, 18)] + assert skeleton.local_imports == ["LeanPool.Other.Module"] + +def test_module_skeleton_reads_module_system_imports() -> None: + """`public`/`meta` modifiers and `import all` are still imports. -def test_context_block_does_not_swallow_following_doc_comment() -> None: - """A doc comment after a context command belongs to the next declaration.""" + Missing these leaves a module with no recorded imports, which collapses + the module ordering the minimal-file builder relies on. + """ text = ( - "namespace Demo\n\n/-- Doc of the next declaration. -/\ndef next : Nat := 1\n" + "public import Mathlib.Order.Basic\n" + "public meta import Lean.Elab.Command\n" + "import all LeanPool.Other.Module\n" + "public import LeanPool.Second.Module\n" ) skeleton = module_skeleton(SourceFile.from_text(text)) - assert skeleton.contexts == [(1, "namespace Demo")] + assert skeleton.external_imports == ["Mathlib.Order.Basic", "Lean.Elab.Command"] + assert skeleton.local_imports == [ + "LeanPool.Other.Module", + "LeanPool.Second.Module", + ] def test_lemma_keyword_refines_theorem_kind() -> None: diff --git a/scripts/exposition/Extract.lean b/scripts/exposition/Extract.lean index 62dda4e582..97391c189d 100644 --- a/scripts/exposition/Extract.lean +++ b/scripts/exposition/Extract.lean @@ -51,6 +51,16 @@ def kindOf (env : Environment) (name : Name) (info : ConstantInfo) : Option Stri | .inductInfo _ => if isStructure env name then some "structure" else some "inductive" | _ => none +/-- Is `name` a notation/syntax parser descriptor? Notation commands are +replayed as *context* by the minimal-file builder (following LMLExposition), +so parser declarations are not exposition nodes. -/ +def isParserDescr (env : Environment) (name : Name) : Bool := + match env.find? name with + | some info => + info.type.isConstOf ``Lean.ParserDescr + || info.type.isConstOf ``Lean.TrailingParserDescr + | none => false + /-- Mirrors the doc-gen4 / import-graph blacklist for generated declarations. -/ def isGenerated (env : Environment) (name : Name) : CoreM Bool := do let display := privateToUserName name @@ -58,13 +68,7 @@ def isGenerated (env : Environment) (name : Name) : CoreM Bool := do if isAuxRecursor env name || isNoConfusion env name then return true if (← isRec name) || (← Meta.isMatcher name) then return true if (env.getProjectionFnInfo? name).isSome then return true - -- `declare_syntax_cat` generates a quotation parser `.quot`; the type - -- guard keeps genuine user definitions that happen to be named `quot`. - if let .str _ "quot" := display then - if let some info := env.find? name then - if info.type.isConstOf ``Lean.ParserDescr - || info.type.isConstOf ``Lean.TrailingParserDescr then - return true + if isParserDescr env name then return true return false /-- Should `name` appear as a node of the exposition? -/ @@ -80,13 +84,92 @@ inductives/structures (field types live in the constructor's type). -/ def directUses (env : Environment) (info : ConstantInfo) : Array Name := match info with | .inductInfo v => - v.ctors.foldl (init := info.getUsedConstantsAsSet) + let base := v.ctors.foldl (init := info.getUsedConstantsAsSet) (fun acc c => match env.find? c with | some ci => acc.insertMany ci.getUsedConstantsAsSet | none => acc) - |>.toArray + -- Structure field defaults live in generated `.._default` + -- functions; seeding them lets the resolver tunnel through their bodies. + let withDefaults := + if (getStructureInfo? env v.name).isSome then + (getStructureFields env v.name).foldl (init := base) fun acc field => + match getDefaultFnForField? env v.name field with + | some defaultFn => acc.insert defaultFn + | none => acc + else base + withDefaults.toArray | _ => info.getUsedConstantsAsSet.toArray +/-! The three dependency-recovery mechanisms below are ported from +LMLExposition's `Collect.lean` (Rémy Degenne, +https://github.com/LeanMachineLearning/exposition): coercion instances and +notation expansions leave no constant in elaborated terms, so +`getUsedConstants` alone misses them. -/ + +/-- Coercion type classes whose instances Lean unfolds at use sites; the +instance must still be present for the source's `↑`/`⇑` to elaborate. -/ +def coercionClasses : List Name := + [``CoeFun, ``CoeSort, ``Coe, ``CoeTC, ``CoeHead, ``CoeTail, ``CoeHTCT, + ``CoeOut, ``CoeDep] + +/-- If `type` is, under binders, a coercion-class application `Cls Src …`, +the head constant of `Src` (the type coerced *from*). -/ +partial def coercionSourceType? (type : Expr) : Option Name := + match type with + | .forallE _ _ b _ => coercionSourceType? b + | _ => + let (fn, args) := type.getAppFnArgs + if coercionClasses.contains fn && args.size ≥ 1 then + args[0]!.getAppFn.constName? + else none + +/-- The `String` a string-literal `Expr` holds, if `e` is one. -/ +def exprStrLit? (e : Expr) : Option String := + match e with + | .lit (.strVal s) => some s + | _ => none + +/-- Reconstructs the `Name` value `e` builds (notation/macro definitions +store the constants they expand to as pre-resolved `Name` data, invisible +to `getUsedConstants`). -/ +partial def evalNameExpr? (e : Expr) : Option Name := do + match e.getAppFnArgs with + | (``Lean.Name.anonymous, _) => some .anonymous + | (``Lean.Name.mkStr1, #[a]) => some (.str .anonymous (← exprStrLit? a)) + | (``Lean.Name.mkStr2, #[a, b]) => + some (.str (.str .anonymous (← exprStrLit? a)) (← exprStrLit? b)) + | (``Lean.Name.mkStr3, #[a, b, c]) => + some (.str (.str (.str .anonymous (← exprStrLit? a)) (← exprStrLit? b)) + (← exprStrLit? c)) + | (``Lean.Name.mkStr4, #[a, b, c, d]) => + some (.str (.str (.str (.str .anonymous (← exprStrLit? a)) + (← exprStrLit? b)) (← exprStrLit? c)) (← exprStrLit? d)) + | (``Lean.Name.str, #[p, s]) => some (.str (← evalNameExpr? p) (← exprStrLit? s)) + | (``Lean.Name.num, #[p, n]) => + match n with + | .lit (.natVal k) => some (.num (← evalNameExpr? p) k) + | _ => none + | (``Lean.Name.mkNum, #[p, n]) => + match n with + | .lit (.natVal k) => some (.num (← evalNameExpr? p) k) + | _ => none + | _ => none + +/-- Every `Name` value embedded anywhere in `e`. -/ +partial def collectEmbeddedNames (e : Expr) : Array Name := Id.run do + let mut acc : Array Name := #[] + if let some n := evalNameExpr? e then acc := acc.push n + match e with + | .app f a => return acc ++ collectEmbeddedNames f ++ collectEmbeddedNames a + | .lam _ t b _ => return acc ++ collectEmbeddedNames t ++ collectEmbeddedNames b + | .forallE _ t b _ => return acc ++ collectEmbeddedNames t ++ collectEmbeddedNames b + | .letE _ t v b _ => + return acc ++ collectEmbeddedNames t ++ collectEmbeddedNames v + ++ collectEmbeddedNames b + | .mdata _ b => return acc ++ collectEmbeddedNames b + | .proj _ _ b => return acc ++ collectEmbeddedNames b + | _ => return acc + /-- Expand a seed set of used constants, tunnelling through generated pool auxiliaries, until exposed pool declarations (edges) or non-pool constants (externals) are reached. -/ @@ -116,20 +199,83 @@ def resolveSeeds (env : Environment) (self : Name) (seeds : Array Name) def escapeName (n : Name) : String := n.toString +/-- Pool constants whose type is a coercion-class application, keyed by the +head constant of the type coerced *from*. Ported from LMLExposition +(`coercionInstancesByType`); membership in the instance table is not +consulted (extension states are not loaded), the type shape suffices. -/ +def coercionInstancesByType (env : Environment) (exposed : NameSet) : + Std.HashMap Name (Array Name) := Id.run do + let mut m : Std.HashMap Name (Array Name) := {} + for name in exposed.toArray do + if let some info := env.find? name then + if let some src := coercionSourceType? info.type then + m := m.insert src ((m.getD src #[]).push name) + return m + +/-- Normalized notation-kind name: re-elaborated local notations get fresh +private prefixes, so kinds are matched modulo `privateToUserName` on both +the environment side and the parsed-syntax side. -/ +def normalizeKind (n : Name) : Name := privateToUserName n + +/-- All pool parser-descriptor constants (notation kinds, normalized), with +their defining module and range-start position. -/ +def poolNotationKinds (env : Environment) : CoreM (Array (Name × Name × Position)) := do + let mut acc : Array (Name × Name × Position) := #[] + for moduleIdx in [0:env.header.moduleNames.size] do + let moduleName := env.header.moduleNames[moduleIdx]! + unless isPoolModule moduleName do continue + let moduleData : ModuleData := env.header.moduleData[moduleIdx]! + for name in moduleData.constNames do + if isParserDescr env name then + if let some ranges ← findDeclarationRanges? name then + acc := acc.push (normalizeKind name, moduleName, ranges.range.pos) + return acc + +/-- Maps each pool notation kind to the *exposed* constants its expansion +references (ported from LMLExposition's `notationExpansionDeps`): notation +macro definitions embed both the parser kind and the abbreviated constants +as pre-resolved `Name` data. -/ +def notationExpansionDeps (env : Environment) (exposed : NameSet) : + Std.HashMap Name (Array Name) := Id.run do + let mut m : Std.HashMap Name (Array Name) := {} + for moduleIdx in [0:env.header.moduleNames.size] do + unless isPoolModule env.header.moduleNames[moduleIdx]! do continue + let moduleData : ModuleData := env.header.moduleData[moduleIdx]! + for name in moduleData.constNames do + if let some (.defnInfo v) := env.find? name then + let names := collectEmbeddedNames v.value + let kinds := names.filter (isParserDescr env ·) + unless kinds.isEmpty do + let realDeps := names.filter (fun n => exposed.contains n) + for k in kinds do + let key := normalizeKind k + m := m.insert key ((m.getD key #[]) ++ realDeps) + return m + def declJson (env : Environment) (name : Name) (info : ConstantInfo) - (exposed : NameSet) : CoreM (Option Json) := do + (exposed : NameSet) (coercionInsts : Std.HashMap Name (Array Name)) : + CoreM (Option Json) := do let some ranges ← findDeclarationRanges? name | return none let some kind := kindOf env name info | return none let some moduleIdx := env.getModuleIdxFor? name | return none let module := env.header.moduleNames[moduleIdx.toNat]! let display := privateToUserName name let doc ← findDocString? env name - let (edges, extCount) := resolveSeeds env name (directUses env info) exposed + -- Coercion instances are unfolded out of elaborated terms; re-attach the + -- instances coercing *from* any referenced type (LMLExposition's + -- `addCoercionInsts`). + let addCoercion (edges : NameSet) : NameSet := + edges.toArray.foldl (init := edges) fun acc dep => + (coercionInsts.getD dep #[]).foldl (init := acc) fun acc2 inst => + if inst == name then acc2 else acc2.insert inst + let (rawEdges, extCount) := resolveSeeds env name (directUses env info) exposed + let edges := addCoercion rawEdges -- Statement-only dependencies for proof-carrying declarations: the minimal -- Lean file replaces their proofs by `sorry`, so only the type's -- dependencies must be present for it to elaborate. let typeEdges : Option NameSet := match info with - | .thmInfo v => some (resolveSeeds env name v.type.getUsedConstants exposed).1 + | .thmInfo v => + some (addCoercion (resolveSeeds env name v.type.getUsedConstants exposed).1) | _ => none let r := ranges.range let s := ranges.selectionRange @@ -148,9 +294,8 @@ def declJson (env : Environment) (name : Name) (info : ConstantInfo) ++ (if isPrivateName name then [("p", Json.bool true)] else []) ++ (match doc with | some d => [("d", Json.str d)] | none => []) -def extract (outPath : System.FilePath) : CoreM Unit := do - let env ← getEnv - -- Pass 1: collect the exposed node set. +/-- Pass 1: the exposed node set, in module order. -/ +def exposedDecls (env : Environment) : CoreM (NameSet × Array Name) := do let mut exposed : NameSet := {} let mut names : Array Name := #[] for moduleIdx in [0:env.header.moduleNames.size] do @@ -164,31 +309,447 @@ def extract (outPath : System.FilePath) : CoreM Unit := do if ← isExposed env name info then exposed := exposed.insert name names := names.push name - -- Pass 2: emit one JSON line per exposed declaration. + return (exposed, names) + +def extract (outPath : System.FilePath) (exposed : NameSet) (names : Array Name) : + CoreM Unit := do + let env ← getEnv + let coercionInsts := coercionInstancesByType env exposed IO.FS.createDirAll (outPath.parent.getD ".") let handle ← IO.FS.Handle.mk outPath .write for name in names do let some info := env.find? name | continue - if let some json ← declJson env name info exposed then + if let some json ← declJson env name info exposed coercionInsts then handle.putStrLn json.compress handle.flush IO.println s!"exposition: wrote {names.size} declarations to {outPath}" end Exposition -def main (args : List String) : IO UInt32 := do +namespace Exposition.Commands + +/-! +Per-module command classification for the minimal-file builder, ported from +LMLExposition's `Extract.lean` (Rémy Degenne, after Matthew Ballard's +`EmitStandalone.lean`). Each source file is re-elaborated against the loaded +environment (`IO.processCommands`; declarations fail fast with "already +declared", which is expected and ignored) to recover per-command `Syntax` +and byte ranges. The output is one JSON line per module describing every +declaration command (with byte-exact `sorry`-surgery edits) and every +context command (`namespace`/`open`/`variable`/notation/...), which the +client-side builder assembles into standalone files. +-/ + +open Lean.Elab + +/-- The `declVal` syntax node of a declaration, if present. -/ +partial def findDeclValStx? (root : Syntax) : Option Syntax := Id.run do + let mut worklist : Array Syntax := #[root] + while !worklist.isEmpty do + let stx := worklist.back! + worklist := worklist.pop + let k := stx.getKind + if k == ``Parser.Command.declValSimple || k == ``Parser.Command.declValEqns + || k == ``Parser.Command.whereStructInst then + return some stx + for arg in stx.getArgs do + worklist := worklist.push arg + return none + +/-- True if `stx` declares a `theorem` or `lemma` (proof replaced by +`sorry`); sees through `open … in` wrapper commands. -/ +partial def isTheoremDecl (stx : Syntax) : Bool := Id.run do + let mut worklist : Array Syntax := #[stx] + while !worklist.isEmpty do + let s := worklist.back! + worklist := worklist.pop + let k := s.getKind + if k == ``Parser.Command.theorem || k == `lemma then return true + for arg in s.getArgs do + worklist := worklist.push arg + return false + +/-- Byte ranges of the outermost `by …` blocks inside `root` (embedded +proofs in a definition's value, replaced by `sorry`). -/ +partial def collectByBlocks (root : Syntax) : Array (String.Pos.Raw × String.Pos.Raw) := Id.run do + let mut acc : Array (String.Pos.Raw × String.Pos.Raw) := #[] + let mut worklist : Array Syntax := #[root] + while !worklist.isEmpty do + let stx := worklist.back! + worklist := worklist.pop + if stx.getKind == ``Lean.Parser.Term.byTactic then + match stx.getPos?, stx.getTailPos? with + | some s, some e => acc := acc.push (s, e) + | _, _ => for arg in stx.getArgs do worklist := worklist.push arg + else + for arg in stx.getArgs do + worklist := worklist.push arg + return acc + +/-- Every `SyntaxNodeKind` occurring in `stx` (notation uses show up as +nodes whose kind is the notation parser's name). -/ +partial def collectSyntaxKinds (stx : Syntax) (acc : NameSet := {}) : NameSet := Id.run do + let mut acc := acc + let mut worklist : Array Syntax := #[stx] + while !worklist.isEmpty do + let s := worklist.back! + worklist := worklist.pop + acc := acc.insert s.getKind + for arg in s.getArgs do + worklist := worklist.push arg + return acc + +/-- Every identifier appearing anywhere in `stx`, as strings. -/ +partial def collectIdents (stx : Syntax) : Array String := Id.run do + let mut acc : Array String := #[] + let mut worklist : Array Syntax := #[stx] + while !worklist.isEmpty do + let s := worklist.back! + worklist := worklist.pop + if s.isIdent then acc := acc.push s.getId.toString + for a in s.getArgs do + worklist := worklist.push a + return acc + +/-- Notation/syntax-defining command kinds, replayed as context so that +declarations using them still parse. Extends LMLExposition's set with the +Mathlib `notation3` command and `elab_rules`/`declare_syntax_cat`. -/ +def isNotationCmdKind (k : SyntaxNodeKind) : Bool := + k == ``Parser.Command.«notation» || k == ``Parser.Command.«mixfix» + || k == ``Parser.Command.«macro» || k == ``Parser.Command.«macro_rules» + || k == ``Parser.Command.«syntax» || k == ``Parser.Command.«elab» + || k == `Lean.Parser.Command.elab_rules || k == ``Parser.Command.syntaxCat + || k == `Mathlib.Notation3.notation3 || k == `Lean.Parser.Command.binderPredicate + -- Mathlib's `scoped[NS] infixl …` wrapper: dropping it loses the + -- notation entirely, so declarations using it cannot be re-parsed. + || k == `Mathlib.Tactic.scopedNS + -- Attribute/extension registration commands (`register_simp_attr …`) + -- must replay for inline `@[custom_attr]` uses to elaborate. + || (match k with + | .str _ "registerSimpAttr" => true + | .str _ "registerLabelAttr" => true + | _ => false) + +/-- Short context tag for a command kind, or `none` when the command is +neither context nor (potentially) a declaration wrapper. -/ +def contextTag (k : SyntaxNodeKind) : Option String := + if k == ``Parser.Command.namespace then some "ns" + else if k == ``Parser.Command.«end» then some "end" + else if k == ``Parser.Command.«open» then some "open" + else if k == ``Parser.Command.«variable» then some "var" + else if k == ``Parser.Command.«section» + || k == `Lean.Parser.Command.noncomputableSection then some "sec" + else if k == ``Parser.Command.«set_option» then some "opt" + else if k == ``Parser.Command.universe then some "univ" + else if isNotationCmdKind k then some "nota" + else none + +/-- Decomposes a `variable` command into binders as +`(startByte, endByte, identifiers)`. -/ +def decomposeVariable (stx : Syntax) : Array (Nat × Nat × Array String) := Id.run do + let binderNodes := if stx.getArgs.size ≥ 2 then stx[1].getArgs else #[] + let mut res : Array (Nat × Nat × Array String) := #[] + for b in binderNodes do + match b.getPos?, b.getTailPos? with + | some s, some e => res := res.push (s.byteIdx, e.byteIdx, collectIdents b) + | _, _ => pure () + return res + +/-- `open NS (a b c)`: the namespace as spelled and the listed identifiers. -/ +def openOnlyParts (stx : Syntax) : Option (String × Array String) := + if stx.getKind == ``Parser.Command.«open» && stx.getArgs.size ≥ 2 + && stx[1].getKind == ``Parser.Command.openOnly && stx[1].getArgs.size ≥ 3 then + some (stx[1][0].getId.toString, collectIdents stx[1][2]) + else none + +/-- The individual declaration nodes of a command: a plain command yields +itself; a `mutual … end` yields each member, so surgery applies per member +(the previous whole-command scan found only the first `declVal`). -/ +partial def declarationNodes (stx : Syntax) : Array Syntax := Id.run do + if stx.getKind != ``Parser.Command.«mutual» then return #[stx] + let mut acc : Array Syntax := #[] + let mut worklist : Array Syntax := #[stx] + while !worklist.isEmpty do + let s := worklist.back! + worklist := worklist.pop + if s.getKind == ``Parser.Command.declaration || s.getKind == `lemma then + acc := acc.push s + else + for arg in s.getArgs do + worklist := worklist.push arg + return if acc.isEmpty then #[stx] else acc + +/-- Edits (byte range → replacement) that turn a declaration command into +its minimal-file form: theorem proofs become `:= sorry`; a definition keeps +its value but embedded `by` blocks become `sorry`. Mutual members are +handled individually. -/ +def surgeryEdits (stx : Syntax) (cmdEnd : String.Pos.Raw) : Array (Nat × Nat × String) := + Id.run do + let mut edits : Array (Nat × Nat) := #[] + let mut sorried : Array (Nat × Nat × String) := #[] + for node in declarationNodes stx do + let nodeEnd := (node.getTailPos?).getD cmdEnd + if isTheoremDecl node then + if let some valStart := findDeclValStx? node >>= (·.getPos?) then + sorried := sorried.push (valStart.byteIdx, nodeEnd.byteIdx, ":= sorry") + else + if let some v := findDeclValStx? node then + for (s, e) in collectByBlocks v do + -- Nested `byTactic` wrappers can yield the same byte range + -- twice; duplicate edits would emit `sorrysorry`. + if !edits.contains (s.byteIdx, e.byteIdx) then + edits := edits.push (s.byteIdx, e.byteIdx) + sorried := sorried.push (s.byteIdx, e.byteIdx, "sorry") + return sorried + +/-- Every identifier in `stx` paired with its start byte position. -/ +partial def collectIdentsWithPos (stx : Syntax) : Array (String × Nat) := Id.run do + let mut acc : Array (String × Nat) := #[] + let mut worklist : Array Syntax := #[stx] + while !worklist.isEmpty do + let s := worklist.back! + worklist := worklist.pop + if s.isIdent then + if let some pos := s.getPos? then + acc := acc.push (s.getId.toString, pos.byteIdx) + for a in s.getArgs do + worklist := worklist.push a + return acc + +/-- Pool modules transitively imported by `module` (inclusive), from the +environment's import graph. Restricts the syntactic-deps scan to +declarations actually visible at the command — a short name matching a +declaration in a *sibling* namespace of an unimported module must not +resolve (it wouldn't in Lean either). -/ +def moduleImportClosure (env : Environment) (module : Name) : NameSet := Id.run do + let mut closure : NameSet := {} + let mut stack : Array Name := #[module] + while h : stack.size > 0 do + let current := stack[stack.size - 1] + stack := stack.pop + if closure.contains current then continue + closure := closure.insert current + if let some idx := env.getModuleIdx? current then + if h2 : idx.toNat < env.header.moduleData.size then + for imported in env.header.moduleData[idx.toNat].imports do + if isPoolModule imported.module then + stack := stack.push imported.module + return closure + +/-- Exposed declarations a command's *source* mentions by (possibly +partially qualified) name, restricted to `visibleModules`. Elaborated terms +lose references that only exist syntactically — `simp only [name]` lists, +tactic arguments, reducible definitions inlined during elaboration — so the +builder needs this closure for commands whose bodies are kept. -/ +def syntacticDeps (env : Environment) (stx : Syntax) (self : Array Name) + (exposedByLast : Std.HashMap String (Array Name)) + (visibleModules : NameSet) : Array Name := Id.run do + -- Scan only the parts that survive surgery: a theorem's proof is replaced + -- by `sorry`, so identifiers at or past its `declVal` don't contribute. + let mut idents : Array String := #[] + for node in declarationNodes stx do + let pairs := collectIdentsWithPos node + match (if isTheoremDecl node then + findDeclValStx? node >>= (·.getPos?) else none) with + | none => idents := idents ++ pairs.map (·.1) + | some valStart => + idents := idents + ++ (pairs.filter (fun (_, pos) => pos < valStart.byteIdx)).map (·.1) + let mut acc : NameSet := {} + for ident in idents do + let lastComponent := (ident.splitOn ".").getLastD ident + for candidate in exposedByLast.getD lastComponent #[] do + if self.contains candidate then continue + let visible := match env.getModuleIdxFor? candidate with + | some idx => visibleModules.contains env.header.moduleNames[idx.toNat]! + | none => false + unless visible do continue + let cstr := candidate.toString + if cstr == ident || cstr.endsWith ("." ++ ident) then + acc := acc.insert candidate + return acc.toArray + +/-- Processes one module source: classifies each command and emits the JSON +entry list. `declPos` maps range-start byte indices to exposed declaration +names (several may share one range start); `notationKindsAt` maps range-start byte indices to pool parser-kind +names (so a notation command learns which kinds it defines); +`notationDeps` maps parser kinds to their expansion's exposed constants; +`allNotationKinds` is the pool-wide kind set for `usedNotations`. -/ +def processFile (env : Environment) (source : String) (filePath : String) + (declPos : Std.HashMap Nat (Array Name)) (notationKindsAt : Std.HashMap Nat Name) + (notationDeps : Std.HashMap Name (Array Name)) (allNotationKinds : NameSet) + (exposedByLast : Std.HashMap String (Array Name)) (visibleModules : NameSet) : + IO (Array Json) := do + let inputCtx := Parser.mkInputContext source filePath + let (_, parserState, messages) ← Parser.parseHeader inputCtx + let cmdState := Command.mkState env messages {} + let s ← IO.processCommands inputCtx parserState cmdState + let mut entries : Array Json := #[] + let mut nsPrefixStack : Array Name := #[Name.anonymous] + for stx in s.commands do + if stx.getKind == ``Parser.Module.header then continue + let some cmdStart := stx.getPos? | continue + let some cmdEnd := stx.getTailPos? | continue + let mut declNames : Array Name := #[] + for (pos, names) in declPos do + if pos ≥ cmdStart.byteIdx && pos < cmdEnd.byteIdx then + declNames := declNames ++ names + let mut kindNames : Array Name := #[] + for (pos, kindName) in notationKindsAt do + if pos ≥ cmdStart.byteIdx && pos < cmdEnd.byteIdx then + kindNames := kindNames.push kindName + -- Notation/tactic-defining commands (`elab "casesPlayer" : tactic`, + -- `macro …`) also *define* constants, but they must be replayed as + -- context so the syntax they introduce still parses. + if !declNames.isEmpty && !isNotationCmdKind stx.getKind then + let used := (collectSyntaxKinds stx).toArray.map normalizeKind + |>.filter allNotationKinds.contains + let sd := syntacticDeps env stx declNames exposedByLast visibleModules + entries := entries.push <| Json.mkObj <| [ + ("t", Json.str "d"), + ("s", Json.num cmdStart.byteIdx), + ("e", Json.num cmdEnd.byteIdx), + ("n", toJson (declNames.map escapeName)) + ] ++ (let ed := surgeryEdits stx cmdEnd + if ed.isEmpty then [] else + [("ed", Json.arr (ed.map fun (a, b, r) => + Json.arr #[Json.num a, Json.num b, Json.str r]))]) + ++ (if used.isEmpty then [] else [("un", toJson (used.map escapeName))]) + ++ (if sd.isEmpty then [] else [("sd", toJson (sd.map escapeName))]) + else if let some tag := contextTag stx.getKind then + let kind := stx.getKind + let nsName? := + if kind == ``Parser.Command.namespace && stx.getArgs.size ≥ 2 then + some stx[1].getId + else if kind == ``Parser.Command.«end» && stx.getArgs.size ≥ 2 then + -- `end A.B` names what it closes; the builder needs it to pop the + -- right number of (dotted) scope components. The optional name may + -- be a direct ident or wrapped in a null node. + if stx[1].isIdent then some stx[1].getId + else if stx[1].getNumArgs ≥ 1 && stx[1][0].isIdent then some stx[1][0].getId + else none + else none + -- Only `namespace` commands qualify and push; `end`/`section` manage + -- the stack without contributing a qualified name. + let qualifiedNs? := if kind == ``Parser.Command.namespace then + nsName?.map (nsPrefixStack.back! ++ ·) else none + if let some ns := qualifiedNs? then + nsPrefixStack := nsPrefixStack.push ns + else if tag == "sec" then + nsPrefixStack := nsPrefixStack.push nsPrefixStack.back! + else if tag == "end" && nsPrefixStack.size > 1 then + nsPrefixStack := nsPrefixStack.pop + let mut fields : List (String × Json) := [ + ("t", Json.str "c"), + ("s", Json.num cmdStart.byteIdx), + ("e", Json.num cmdEnd.byteIdx), + ("k", Json.str tag) + ] + if let some ns := nsName? then + fields := fields ++ [("ns", Json.str ns.toString)] + if let some qns := qualifiedNs? then + fields := fields ++ [("q", Json.str qns.toString)] + if tag == "var" then + let binders := decomposeVariable stx + fields := fields ++ [("b", Json.arr (binders.map fun (a, b, ids) => + Json.arr #[Json.num a, Json.num b, toJson ids]))] + if let some (ns, ids) := openOnlyParts stx then + fields := fields ++ [("on", Json.arr #[Json.str ns, toJson ids])] + if tag == "nota" && !kindNames.isEmpty then + fields := fields ++ [("kn", toJson (kindNames.map escapeName))] + let deps := kindNames.foldl (init := #[]) fun acc k => + acc ++ notationDeps.getD k #[] + unless deps.isEmpty do + fields := fields ++ [("nd", toJson (deps.map escapeName))] + entries := entries.push (Json.mkObj fields) + return entries + +/-- Writes the per-module command tables as JSONL: +`{"m": "", "c": [, …]}` per line. Only modules containing +exposed declarations or pool notation kinds are emitted. -/ +def emitCommands (outPath : System.FilePath) (exposed : NameSet) (names : Array Name) : + CoreM Unit := do + let env ← getEnv + let notationKinds ← poolNotationKinds env + let notationDeps := notationExpansionDeps env exposed + let allNotationKinds : NameSet := + notationKinds.foldl (init := {}) fun acc (n, _, _) => acc.insert n + -- Index exposed names by last component for the syntactic-deps scan. + let exposedByLast : Std.HashMap String (Array Name) := + exposed.toArray.foldl (init := {}) fun acc name => + let key := name.components.getLastD name |>.toString + acc.insert key ((acc.getD key #[]).push name) + -- Group exposed declarations and notation kinds by module. + let mut declsByModule : Std.HashMap Name (Array Name) := {} + for name in names do + if let some idx := env.getModuleIdxFor? name then + let module := env.header.moduleNames[idx.toNat]! + declsByModule := declsByModule.insert module + ((declsByModule.getD module #[]).push name) + let mut kindsByModule : Std.HashMap Name (Array (Name × Position)) := {} + for (kindName, module, pos) in notationKinds do + kindsByModule := kindsByModule.insert module + ((kindsByModule.getD module #[]).push (kindName, pos)) + IO.FS.createDirAll (outPath.parent.getD ".") + let handle ← IO.FS.Handle.mk outPath .write + let mut written := 0 + for moduleIdx in [0:env.header.moduleNames.size] do + let module := env.header.moduleNames[moduleIdx]! + unless isPoolModule module do continue + let moduleDecls := declsByModule.getD module #[] + let moduleKinds := kindsByModule.getD module #[] + if moduleDecls.isEmpty && moduleKinds.isEmpty then continue + let path := System.mkFilePath (module.components.map (·.toString)) + |>.addExtension "lean" + let some source ← (do + try pure (some (← IO.FS.readFile path)) catch _ => pure none) + | continue + let fileMap := FileMap.ofString source + -- One range start can carry several declarations (`irreducible_def`, + -- mutual blocks), so map each position to every name declared there. + let mut declPos : Std.HashMap Nat (Array Name) := {} + for name in moduleDecls do + if let some ranges ← findDeclarationRanges? name then + let key := (fileMap.ofPosition ranges.range.pos).byteIdx + declPos := declPos.insert key ((declPos.getD key #[]).push name) + let mut notationKindsAt : Std.HashMap Nat Name := {} + for (kindName, pos) in moduleKinds do + notationKindsAt := notationKindsAt.insert (fileMap.ofPosition pos).byteIdx kindName + let visibleModules := moduleImportClosure env module + let entries ← processFile env source path.toString declPos notationKindsAt + notationDeps allNotationKinds exposedByLast visibleModules + handle.putStrLn (Json.mkObj [ + ("m", Json.str module.toString), + ("c", Json.arr entries) + ]).compress + written := written + 1 + handle.flush + IO.println s!"exposition: wrote command tables for {written} modules to {outPath}" + +end Exposition.Commands + +unsafe def main (args : List String) : IO UInt32 := do let outPath := args[0]?.getD "exposition-dump.jsonl" + let commandsPath := args[1]?.getD "exposition-commands.jsonl" -- Further arguments override the imported modules (default: the whole pool); -- useful for testing against a partially built tree. - let modules := if args.length > 1 then args.drop 1 |>.map (·.toName) else [Exposition.poolRoot] + let modules := if args.length > 2 then args.drop 2 |>.map (·.toName) else [Exposition.poolRoot] Lean.initSearchPath (← Lean.findSysroot) + -- Extension states must be loaded (and initializers executed) so that + -- `IO.processCommands` can parse Mathlib/pool notations (`Type*`, ...); + -- without them, parse-error recovery silently truncates commands. + Lean.enableInitializersExecution let imports := modules.toArray.map fun module => ({ module } : Lean.Import) - let env ← Lean.importModules imports {} (trustLevel := 1024) + let env ← Lean.importModules imports {} (trustLevel := 1024) (loadExts := true) let coreContext : Lean.Core.Context := { fileName := "", fileMap := default, maxHeartbeats := 0 } - let (result, _) ← (Exposition.extract outPath).toIO coreContext { env } + let run : Lean.CoreM Unit := do + let (exposed, names) ← Exposition.exposedDecls env + Exposition.extract outPath exposed names + Exposition.Commands.emitCommands commandsPath exposed names + let (result, _) ← run.toIO coreContext { env } let _ := result return 0 diff --git a/scripts/exposition/build-minimal.mjs b/scripts/exposition/build-minimal.mjs new file mode 100644 index 0000000000..cf88279e07 --- /dev/null +++ b/scripts/exposition/build-minimal.mjs @@ -0,0 +1,65 @@ +#!/usr/bin/env node +// Build one minimal Lean file from a generated exposition site, exactly as +// the browser does (same builder module). Used by the verification harness +// (python -m lean_pool.exposition.verify). +// +// Usage: node build-minimal.mjs +// Exit codes: 0 built, 2 declaration not found, 3 build error. +import fs from "node:fs"; +import path from "node:path"; +import { createRequire } from "node:module"; + +const argv = process.argv.slice(2); +if (!argv[4]) { + console.error( + "usage: build-minimal.mjs "); + process.exit(3); +} +const [siteDir, repoRoot] = [path.resolve(argv[0]), path.resolve(argv[1])]; +const [project, declName, outFile] = argv.slice(2); + +const require = createRequire(import.meta.url); +const builder = require( + path.join(repoRoot, "python/lean_pool/exposition/static/assets/minimal.js")); + +const shard = JSON.parse( + fs.readFileSync(path.join(siteDir, "data/projects", `${project}.json`))); + +let target = shard.decls.findIndex( + (d) => d.name === declName || d.full === declName); +if (target < 0) { + // Card names sometimes carry an extra namespace prefix; suffix-match. + target = shard.decls.findIndex((d) => declName.endsWith(`.${d.name}`) + || d.name.endsWith(`.${declName}`)); +} +if (target < 0) { + console.error(`declaration not found in ${project}: ${declName}`); + process.exit(2); +} + +const sources = {}; +function loadModule(index) { + if (sources[index] !== undefined) return; + const file = path.join( + repoRoot, ...shard.modules[index].split(".")); + sources[index] = fs.readFileSync(`${file}.lean`); +} + +const cone = builder.coneIds(shard, target); +for (const moduleIndex of cone.modules) loadModule(moduleIndex); + +let result = builder.build(shard, sources, target); +for (let round = 0; result.pending && round < 4; round++) { + for (const moduleIndex of result.pending) loadModule(moduleIndex); + result = builder.build(shard, sources, target); +} +if (result.pending) { + console.error(`unresolved module sources for ${declName}`); + process.exit(3); +} + +fs.mkdirSync(path.dirname(outFile), { recursive: true }); +fs.writeFileSync(outFile, result.text); +console.log( + `${project}/${declName}: ${result.declarationCount} decls, ` + + `${result.moduleCount} modules, ${(result.text.length / 1024).toFixed(1)} KB`); diff --git a/scripts/exposition/extract-all.sh b/scripts/exposition/extract-all.sh new file mode 100755 index 0000000000..d5c3e2d94e --- /dev/null +++ b/scripts/exposition/extract-all.sh @@ -0,0 +1,52 @@ +#!/usr/bin/env bash +# Per-project exposition extraction driver. +# +# Each project is extracted against its own environment (Mathlib + that +# project only). A whole-pool environment would superpose every project's +# parser extensions, and a foreign notation can turn an identifier used by +# another project (ε, s, …) into a keyword token — parse-error recovery +# then silently truncates re-parsed commands. Lean never builds against +# such a superposition, and neither do we. +# +# Usage: [LEAN_CMD=lean] [EXTRACT_JOBS=N] extract-all.sh +# Run from the repository root with LEAN_PATH set (e.g. via `lake env`). +set -euo pipefail + +out_dump="${1:-exposition-dump.jsonl}" +out_cmds="${2:-exposition-commands.jsonl}" +jobs="${EXTRACT_JOBS:-2}" +lean_cmd="${LEAN_CMD:-lean}" +workdir="$(mktemp -d)" + +# Project roots: the second component of every module the index imports. +projects="$(sed -n 's/^import LeanPool\.//p' LeanPool.lean | cut -d. -f1 | sort -u)" +count="$(printf '%s\n' "$projects" | wc -l | tr -d ' ')" +echo "exposition: extracting $count projects ($jobs at a time)" + +extract_failed=0 +printf '%s\n' "$projects" | xargs -P "$jobs" -I '{}' sh -c ' + "$1" --run scripts/exposition/Extract.lean \ + "$2/dump-$3.jsonl" "$2/cmds-$3.jsonl" "LeanPool.$3" \ + > "$2/log-$3.txt" 2>&1 || { echo "$3" >> "$2/FAILED"; } +' extract "$lean_cmd" "$workdir" '{}' || extract_failed=1 + +if [ -f "$workdir/FAILED" ] || [ "$extract_failed" -ne 0 ]; then + echo "exposition: extraction FAILED for:" >&2 + cat "$workdir/FAILED" 2>/dev/null >&2 || true + while read -r project; do + echo "--- $project ---" >&2 + tail -15 "$workdir/log-$project.txt" >&2 || true + done < "$workdir/FAILED" + echo "exposition: work dir kept at $workdir" >&2 + exit 1 +fi + +: > "$out_dump" +: > "$out_cmds" +for project in $projects; do + cat "$workdir/dump-$project.jsonl" >> "$out_dump" + cat "$workdir/cmds-$project.jsonl" >> "$out_cmds" +done +rm -rf "$workdir" +echo "exposition: wrote $(wc -l < "$out_dump" | tr -d ' ') declarations to $out_dump" +echo "exposition: wrote $(wc -l < "$out_cmds" | tr -d ' ') module command tables to $out_cmds"