Exposition: LML extraction methodology + verified minimal files (207/238)

.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)

.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

.gitignore

@@ -4,6 +4,7 @@
 
 # Exposition build outputs (see python/lean_pool/exposition/)
 /exposition-dump.jsonl
+/exposition-commands.jsonl
 /exposition-site/
 
 # Python

python/lean_pool/exposition/SCHEMA.md

@@ -114,41 +114,48 @@ Link recipes: `doi` → `https://doi.org/<doi>`, `arxiv` →
 `https://arxiv.org/abs/<arxiv>`, `url` as-is, `github_repo` →
 `https://github.com/<github_repo>`.
 
-### 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`
 

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, "