From 1d3c20412e1aa53c1336d8782676f6899c332985 Mon Sep 17 00:00:00 2001 From: TimeLordRaps Date: Mon, 12 Oct 2026 23:19:19 -0700 Subject: [PATCH 1/3] feat: make the proofsite legible and provenance-first --- .github/workflows/pages.yml | 6 +- README.md | 41 ++- docs/REFERENCE.md | 23 +- hosted/overlays/README.md | 6 + hosted/overlays/manifest.json | 37 ++- hosted/overlays/oai.l4del | 8 +- hosted/overlays/tpil.l4del | 90 ------- .../src/lean4_explainer_corpora/extension.py | 5 + .../src/lean4_explainer_corpora/overlays.py | 32 ++- .../src/lean4_explainer_corpora/showcase.py | 233 +++++++++++++++- packages/corpora/tests/test_cli_corpora.py | 8 +- packages/corpora/tests/test_corpora.py | 4 +- .../corpora/tests/test_hosted_overlays.py | 6 +- packages/corpora/tests/test_showcase.py | 45 +++- .../lean4_explainer_ecosystem/extension.py | 6 +- .../lean4_explainer_implications/extension.py | 21 +- packages/l4del/README.md | 8 +- packages/l4del/pyproject.toml | 4 +- .../src/lean4_explainer_l4del/__init__.py | 2 +- .../src/lean4_explainer_l4del/extension.py | 196 ++++++++++++-- .../src/lean4_explainer_l4del/grammar.py | 76 +++++- .../l4del/src/lean4_explainer_l4del/graph.py | 18 +- .../l4del/src/lean4_explainer_l4del/model.py | 1 + .../src/lean4_explainer_l4del/templates.py | 3 + packages/l4del/tests/test_features.py | 56 +++- packages/l4del/tests/test_l4del_spec.py | 54 +++- packages/l4del/tests/test_overlay.py | 37 +++ .../src/lean4_explainer_lean/extension.py | 4 +- .../map/src/lean4_explainer_map/extension.py | 27 +- packages/map/src/lean4_explainer_map/map.js | 11 + packages/map/tests/test_map.py | 4 + .../src/lean4_explainer_reader/extension.py | 2 + .../src/lean4_explainer_reader/reader.js | 14 + packages/reader/tests/test_reader.py | 7 + pyproject.toml | 4 +- scripts/audit_hosted_overlay_grounding.py | 252 ++++++++++++++++++ scripts/check_static_site.py | 234 ++++++++++++++++ scripts/generate_documented_hosted_overlay.py | 9 +- src/lean4_explainer/build.py | 11 +- src/lean4_explainer/config.py | 15 ++ src/lean4_explainer/extensions.py | 11 +- src/lean4_explainer/glossary.py | 23 +- src/lean4_explainer/render.py | 234 +++++++++++++--- src/lean4_explainer/search.py | 17 +- tests/test_build.py | 73 ++++- tests/test_generate_hosted_overlay.py | 28 ++ tests/test_overlay_grounding_audit.py | 145 ++++++++++ tests/test_static_site_check.py | 88 ++++++ 48 files changed, 2008 insertions(+), 231 deletions(-) create mode 100644 scripts/audit_hosted_overlay_grounding.py create mode 100644 scripts/check_static_site.py create mode 100644 tests/test_generate_hosted_overlay.py create mode 100644 tests/test_overlay_grounding_audit.py create mode 100644 tests/test_static_site_check.py diff --git a/.github/workflows/pages.yml b/.github/workflows/pages.yml index 544ed2c134..4c878f730d 100644 --- a/.github/workflows/pages.yml +++ b/.github/workflows/pages.yml @@ -27,7 +27,11 @@ jobs: - name: Install run: python -m pip install . packages/l4del packages/reader packages/map packages/implications packages/corpora packages/corpus-* - name: Build the showcase - run: lean4-explainer showcase --yes --out site --work work --jobs 4 --overlay-manifest hosted/overlays/manifest.json + run: lean4-explainer showcase --yes --out site --work work --jobs 4 --site-url https://timelordraps.github.io/lean4-explainer/ --overlay-manifest hosted/overlays/manifest.json + - name: Verify annotation grounding + run: python scripts/audit_hosted_overlay_grounding.py --manifest hosted/overlays/manifest.json --work work --report site/annotation-audit.json + - name: Validate the generated site + run: python scripts/check_static_site.py --site site --site-url https://timelordraps.github.io/lean4-explainer/ - name: Record build provenance run: | printf '{"repository_sha":"%s","built_at":"%s"}\n' "$GITHUB_SHA" "$(date -u +%Y-%m-%dT%H:%M:%SZ)" > site/build-info.json diff --git a/README.md b/README.md index 390af11406..c75f4f74c9 100644 --- a/README.md +++ b/README.md @@ -1,16 +1,18 @@ # lean4-explainer -**Read real, computer-checked mathematics, one step at a time.** +**Read real Lean source, one step at a time.** Lean 4 is a programming language where you write a math proof and the computer checks every single step. People have used it to formalize huge results, including Fermat's Last Theorem. But a pile of `.lean` files is hard to read if you have never seen one. -lean4-explainer turns that pile into a website you can browse like a guided tour: every theorem gets a plain-English heading, the idea behind it, the steps of the proof, and links to the things it depends on. +lean4-explainer turns that pile into a source-first website you can browse like a guided tour: declarations, comments, +explanations when available, dependency links, and the exact pinned source stay together. The site labels what was +checked by Lean, what was only scanned from text, and what remains an unreviewed explanatory overlay. -**See it live:** https://timelordraps.github.io/lean4-explainer/ (eight well-known Lean projects, including the Fermat's Last Theorem project) +**See it live:** https://timelordraps.github.io/lean4-explainer/ (eight well-known Lean projects, including the unfinished Fermat's Last Theorem formalization project) ## Who is this for? -Someone who loves math and is curious about Lean. You do not need to know Lean, and you do not need to install it to read the site. If you have seen calculus or differential equations in high school, you have the background for most of the pages. When a word is new, look it up in the **Glossary**, linked from every page: it has every definition in the project, every type, property, symbol and tactic the Reading explains, and Lean's own words. +Someone who loves math and is curious about Lean. You do not need to know Lean, and you do not need to install it to read the site. When a word is new, look it up in the **Glossary**, linked from every page: it has every definition in the project, every type, property, symbol and tactic the Reading explains, and Lean's own words. It is also for people who write Lean and want others to understand it. You add short comments above your theorems, and the site does the rest. @@ -35,14 +37,17 @@ Where a project has added explanations of its own (or we have, in a separate ove | **Prerequisites** | What you should understand first | | **Glossary** words | A word the explanations define links to its meaning in the Glossary | | The **statement** and a link to the real source | The exact Lean, when you want it | +| **Sources and attribution** links | The exact full-commit source plus primary project references; traceability and credit, not a claim of review | +| An **Explanation legend** | Lean4 Domain Explanation Language (L4DEL), plus every acronym the explanation defines; unexpanded source abbreviations are labeled rather than guessed | +| A linked **quotation** | Exact words kept distinct from the explainer's own prose and linked to the named source | ## How relationships show up Math is a web of results leaning on each other. The site shows that web in five ways: 1. **The map on each declaration.** Open "Map" under any result to see what it builds on (left) and what uses it (right), two steps each way. The links are read from the code itself, so every project has them, explained or not. Every box is a link, and the map wears the project's own colours. -2. **The project map** (`map.html`). The folders and how they use each other, and any one file with the files around it. -3. **The learning path** (`learning-path.html`). One reading order where nothing appears before the things it needs (from L4DEL `prereq` lines). +2. **The project map** (`map.html`). The folders and how they use each other, and any one file with the files around it. A searchable table exposes the same data without relying on the drawing. +3. **The learning path** (`learning-path.html`). One reading order where nothing appears before the things it needs (from Lean4 Domain Explanation Language `prereq` lines). 4. **Link lists** under each declaration: Prerequisites, See also, and the results it uses. 5. **Implication edges** (`implications.html`, with the optional implications extension). Some links are not in the code at all: one result could give another even though the published proof goes a different way. An edge says so, and since that is a claim, it keeps the exact hypotheses, the conclusion, the commit it was read at, and how far it has been checked (suggested, argued in words, or proved in Lean and checked by the kernel). Edges are kept apart from the links read from the code, so the map never mixes the two. @@ -70,9 +75,11 @@ pip install -e packages/corpora -e packages/corpus-flt lean4-explainer showcase --out site ``` -## Write your own explanations (L4DEL) + -L4DEL is a tiny way to explain a theorem inside a Lean comment. Put lines like these just above it: +## Write your own explanations with the Lean4 Domain Explanation Language (L4DEL) + +The Lean4 Domain Explanation Language (L4DEL) is a small, checked vocabulary for explaining a theorem inside a Lean comment. Put lines like these just above it: ```lean -- L4DEL: title: Two odd numbers add to an even number @@ -80,14 +87,19 @@ L4DEL is a tiny way to explain a theorem inside a Lean comment. Put lines like t -- L4DEL: step: Write each number as 2k + 1. -- L4DEL: step: Add them to get 2(k + m + 1). -- L4DEL: prereq: Nat.odd_iff +-- L4DEL: source: Exact formal source = https://github.com/OWNER/REPO/blob/FULL_COMMIT/Foo.lean#L42 +-- L4DEL: quote: Exact formal source = Two odd numbers add to an even number. +-- L4DEL: acronym: DEL = Domain Explanation Language theorem odd_add_odd ... ``` Lean treats them as ordinary comments, so your proofs are untouched. Run `lean4-explainer check` and it tells you what is missing or misspelled. Run `lean4-explainer annotate --file Foo.lean` and it prints a ready-to-fill template for every declaration that has no explanation. If you do not own the project, keep the explanations in a separate **overlay** file instead of editing their source. -The live showcase explicitly injects repository-owned overlays through a commit- and hash-bound manifest; corpus -packages on PyPI contain no L4DEL explanation text. The details are in the [reference](docs/REFERENCE.md). +The live showcase explicitly injects repository-owned overlays through a commit- and hash-bound manifest; every +rendered overlay links to its exact full-commit source and corpus-level primary references. Those links make a claim +auditable, but do not relabel AI-generated text as human-reviewed. Corpus packages on PyPI contain no hosted L4DEL +explanation text. The details are in the [reference](docs/REFERENCE.md). ## Pick your pieces @@ -98,7 +110,7 @@ The core is small and works alone. You add only what you want: | A quick page of your Lean code | the core | The site from your declarations and comments | | A plain-English reading of every declaration | `packages/reader` | The Reading: claim in words and as a typeset formula, givens, every proof step explained | | What builds on what | `packages/map` | A map on every declaration and a project map, read from the code | -| Titles, intuition, steps, glossary, learning path | `packages/l4del` | L4DEL | +| Titles, intuition, steps, linked quotations, acronym legends, glossary, learning path | `packages/l4del` | Lean4 Domain Explanation Language (L4DEL) | | Claims that one result gives another, each with its contract | `packages/implications` | Implication edges on the declarations they connect, and a page of them | | Proof state after each tactic, and a trust badge | `packages/lean` | Needs Lean installed. It runs Lean on your files | | `explain#Name` links, what changed between versions | `packages/ecosystem` | Links and a changes page | @@ -132,7 +144,12 @@ Two of the example projects are tutorials, so you can read them here and then do - The openai/math project is too big to publish twice (1.1 GB of source), so its pages fetch their file from GitHub, at the pinned commit, to make the Reading. Its glossary lists only the definitions that have a description (about 25,000 of 1.3 million). - The glossary lists definitions, not theorems: theorems are results, and each one is on its file page. - Doc comments are drawn as Markdown, with their formulas typeset. Tables and a few rarer forms show as written, and so does a formula whose TeX has a mistake in it. -- The explanations on the example projects were written for this site. They are not the authors' words, and the site says that too. +- The hosted explanations on the example projects are AI-generated and not human-reviewed. Most are mechanically + regenerated from source-controlled comments or formalization notes; the smaller curated layer is target-checked and + source-linked but remains unreviewed. The site says this beside every annotation and never presents it as mathematical authority. +- The openai/math card credits the repository's internal OpenAI model for producing its manuscripts and proof artifacts, + while explicitly recognizing that the collection builds on the accumulated work of the mathematics community. Individual + scholarly credit follows each manuscript's BibTeX and bibliography, not the site owner's name. - A few kinds of declaration (indented ones, ones made by macros) are not listed. ## More diff --git a/docs/REFERENCE.md b/docs/REFERENCE.md index e989e569fb..2257195394 100644 --- a/docs/REFERENCE.md +++ b/docs/REFERENCE.md @@ -67,9 +67,11 @@ Formulas stay as their TeX, inside ``, for the reader extensio - `sorry` detection is textual. It does not follow dependencies and does not check axioms. - Without the Lean extension, Lean is not run, so axiom and trust checks are UNKNOWN. -## L4DEL: write your own explanations + -L4DEL is an optional extension. It reads `-- L4DEL: key: value` line comments and adds an explanation layer to the site. The core never needs it, and a project that writes none gets the same output as without it. +## Lean4 Domain Explanation Language (L4DEL): write your own explanations + +The Lean4 Domain Explanation Language (L4DEL) is an optional extension. It reads `-- L4DEL: key: value` line comments and adds an explanation layer to the site. The core never needs it, and a project that writes none gets the same output as without it. ``` pip install lean4-explainer[l4del] @@ -82,7 +84,7 @@ Whenever a declaration has no valid L4DEL, the tool says what is missing and pri 3. **Paste** a template directly above its declaration, then replace every `TODO_` value. 4. **Build** with `lean4-explainer build --lean-root lean --out docs`. A `TODO_` left in a value is a warning, so the build reports it. -The generated site gets an L4DEL guide page (`annotate.html`), its `term` lines in the glossary (`glossary.html#t0`, …), and a learning path ordered by prerequisites. +The generated site gets a Lean4 Domain Explanation Language guide page (`annotate.html`), its `term` and `acronym` lines in the glossary, an explanation legend at the top of each annotated file page, and a learning path ordered by prerequisites. Acronym-looking text without an explicit expansion is labeled unresolved rather than guessed; this guarantee covers the explanation layer, not arbitrary identifiers in upstream Lean code. ### The directive grammar @@ -98,6 +100,9 @@ Each directive is one line comment: | `prereq` | comma-separated fully qualified names the proof depends on | a repeated name is an error | | `see` | comma-separated related declarations | a repeated name is an error | | `term` | `word = definition` | each word is defined once in the project | +| `acronym` | `SHORT = expansion` | one consistent expansion across the project; repeated in affected page legends | +| `source` | `label = https://URL` | repeatable; each URL is unique | +| `quote` | `source label = exact excerpt` | repeatable; label must match a `source`, or the hosted overlay's pinned Lean source | Rules: @@ -106,6 +111,8 @@ Rules: - A directive attaches to the next declaration. Only blank lines, comments, attribute lines, and `set_option` lines may separate them. Other code makes a directive an orphan, which is an error. - Anonymous declarations (`example`, unnamed `instance`) cannot carry directives. - `prereq` and `see` names are exact. `foo` does not match `Demo.foo`. A name that matches nothing is a warning. +- `source` links appear beside the explanation under **Sources and attribution**. Use a full-commit GitHub blob URL, DOI, or versioned arXiv URL where possible; a citation makes the wording traceable but does not make it reviewed or correct. +- `quote` keeps exact source words visually and semantically separate from `intuition` and `step` prose. Its source label becomes the quotation link. - A name with distinct definitions is ambiguous: a plain reference is an error, and it must be written `Name@path`, for example `Demo.value@Var/B.lean`. - Values are trimmed, must not be empty, and are at most 2000 characters. - The complete grammar is in `packages/l4del/src/lean4_explainer_l4del/grammar.py`. @@ -172,11 +179,11 @@ Licenses are those of each repository's `LICENSE` file at the pinned commit. Whe ``` lean4-explainer sources [NAME...] # installed corpora, pinned commits, licenses lean4-explainer fetch tutorials --yes # download only -lean4-explainer showcase --yes --out site # download and build one subsite each under a landing page +lean4-explainer showcase --yes --out site --site-url https://example.org/base/ # build a public, canonical site lean4-explainer # same as showcase; prints what it will download, asks first ``` -Without `--yes`, the commands print the plan and ask. When stdin is not a terminal they download nothing and exit with code 2. Corpus packages do not select or contain L4DEL overlays, so an ordinary showcase remains annotation-free even when the L4DEL tooling is installed. A hosted build may opt in with `--overlay-manifest PATH`; every entry is checked against the corpus repository, exact commit and overlay SHA-256, and its review provenance is shown on the landing page and beside rendered annotations. The showcase landing page shows each project's commit, Lean toolchain, `mathlib` commit, and license, and the license text is copied next to each subsite. Each corpus's build errors are printed (and its first warnings): an overlay or an implication edge that names a declaration the site does not have is an error, and the command then exits with code 1, so the Pages workflow does not publish a broken site. Output is about 975 MB for all eight (measured 2026-10-10 with the reader, the map, L4DEL and the implications extension), mostly openai/math, which gets one source link per file instead of one per declaration, no map, and a glossary of its described definitions only, to stay under the 1 GB Pages limit. +Without `--yes`, the commands print the plan and ask. When stdin is not a terminal they download nothing and exit with code 2. Corpus packages do not select or contain L4DEL overlays, so an ordinary showcase remains annotation-free even when the L4DEL tooling is installed. A hosted build may opt in with `--overlay-manifest PATH`; every entry is checked against the corpus repository, exact commit and overlay SHA-256, and its review provenance is shown on the landing page and beside rendered annotations. The hosted workflow also audits generated wording against pinned source-controlled comments or notes and publishes the machine-readable result as `annotation-audit.json`; curated wording is enumerated there as `source-linked-unreviewed`, not silently promoted to reviewed. The showcase landing page shows each project's commit, Lean toolchain, `mathlib` commit, and license, and the license text is copied next to each subsite. `--site-url` enables canonical and social metadata, a custom 404 page, `robots.txt`, and chunked sitemaps. Each corpus's build errors are printed (and its first warnings): an overlay or an implication edge that names a declaration the site does not have is an error, and the command then exits with code 1, so the Pages workflow does not publish a broken site. Output must remain below the configured byte budget; the workflow and release smoke check measure the generated artifact rather than relying on an older estimate. ## Extensions @@ -194,6 +201,10 @@ Pass `--config lean4-explainer.toml` to `build`. Unknown keys and wrong types ar - `source_links`: `"declaration"` (default, one link per declaration) or `"file"` (one per page, for very large trees). - `search`, `cross_links`: booleans that switch those features on or off. - `home`: relative URL of a landing page above this site. Adds an "All corpora" link to every page. +- `site_url`: canonical HTTPS base URL, without a query or fragment. Every page gets a canonical URL; navigation, feature, and annotated pages also get Open Graph/Twitter metadata. Unannotated file pages use a compact shell so very large corpora remain deployable. +- `description`: page description used in metadata. +- `project_url`: HTTPS source-project link shown in full page footers. +- `report_url`: HTTPS feedback or issue link shown in full page footers. - `byte_budget`: the build fails if the output exceeds this many bytes. The default is 1 GB, the GitHub Pages limit. - `glossary`: which of the project's definitions the glossary lists: `"all"` (default), `"described"` (only those with a doc comment, a plain comment or an extension's note; the showcase uses this for openai/math) or `"none"`. - `imports`: where file pages list imports: `"all"` (default), `"import-only"` (only on files that do nothing but import; the showcase uses this for openai/math, whose 336,022 imports would not fit) or `"none"`. @@ -206,7 +217,7 @@ Pass `--config lean4-explainer.toml` to `build`. Unknown keys and wrong types ar - **Defined in this project**: every `def`, `abbrev`, `structure`, `class`, `class inductive`, `inductive` and `opaque` (theorems, instances and examples are results, not words), under its own name (the last part of the full name), with the first paragraph of its description, or its declaration line when it has none, and a link to it. Identical copies in several files are one entry. More than 2,000 entries go on one page per first letter, `glossary-a.html` … `glossary-other.html`; up to that, a long list gets letter headings. The entries come from the incremental cache, so a rebuild that reuses every file still lists them all. - One section per extension that adds words (the `glossary` hook): L4DEL's `term` lines (the term links in explanations point here), and the reader's types, structures, properties, symbols and tactics. - **Lean words**: the language itself (`theorem`, `sorry`, `:=`, `namespace`, `⟨ ⟩`, `·`, …), including all of the README's "Words you will meet". -- Extension pages. L4DEL adds `annotate.html` and `learning-path.html`. The map extension (`packages/map`) adds `map.html`, with the project's folders and any one file with the files around it. It also gives every declaration a "Map" of what it builds on and what uses it, two steps each way, drawn when opened. Its links are read from the code by Lean's name rules (namespaces, `open`, imports, local names; see `packages/map/README.md`), and L4DEL `prereq` links are added as dashed arrows. Imports are followed through files that only import (from the core's import graph): in formal-conjectures that more than doubled the links, from 6,077 to 12,707. Set `map_dependencies = false` to leave it out. +- Extension pages. L4DEL adds `annotate.html` and `learning-path.html`. The map extension (`packages/map`) adds `map.html`, with the project's folders and any one file with the files around it. The same relationships also appear in a searchable file table and a collapsible text representation, so map navigation does not require the diagram or a pointer device. It gives every declaration a "Map" of what it builds on and what uses it, two steps each way, drawn when opened. Its links are read from the code by Lean's name rules (namespaces, `open`, imports, local names; see `packages/map/README.md`), and L4DEL `prereq` links are added as dashed arrows. Imports are followed through files that only import (from the core's import graph): in formal-conjectures that more than doubled the links, from 6,077 to 12,707. Set `map_dependencies = false` to leave it out. - Pages that have not changed since the last build are reused. The cache lives beside the output directory, outside the published site, and can be moved with `--cache`. It is loaded through an allow-list of this package's own types and the types extensions declare. A cache file that refers to anything else is ignored and rebuilt, never run. ## Development diff --git a/hosted/overlays/README.md b/hosted/overlays/README.md index 042db6cda9..d298c33d91 100644 --- a/hosted/overlays/README.md +++ b/hosted/overlays/README.md @@ -8,6 +8,12 @@ The build fails if any binding drifts. `ai-generated-unreviewed` overlays are vi the landing page and beside every rendered annotation. Change that provenance only after an identified human has reviewed the mathematical explanation, and record that identity in `reviewed_by`. +Every rendered overlay annotation links directly to the declaration in the immutable, full-commit GitHub source URL. +The manifest also supplies at least two corpus-level primary references (normally pinned project documentation plus a +paper, blueprint, catalogue, or textbook). Commit-pinned GitHub blobs are used instead of mutable branch links or an +on-demand Wayback snapshot: the URL names the exact bytes the site built, while the manifest hash makes drift fail +closed. These links establish traceability; they do **not** turn an AI-generated explanation into a human review. + The large generated sections copy or condense only material already present in the pinned source: declaration doc comments, immediately leading source comments, and (for openai/math) formalization notes plus Comparator configs. They do not infer mathematics from names. Existing curated entries remain separate at the top of each file and win diff --git a/hosted/overlays/manifest.json b/hosted/overlays/manifest.json index e8b6f0b54c..f787430472 100644 --- a/hosted/overlays/manifest.json +++ b/hosted/overlays/manifest.json @@ -5,6 +5,10 @@ "file": "formal-conjectures.l4del", "repo": "google-deepmind/formal-conjectures", "commit": "1646ca16afd6cc7a693d3bdc9f066c4d3cc01a89", + "sources": [ + {"label": "Pinned project documentation", "url": "https://github.com/google-deepmind/formal-conjectures/blob/1646ca16afd6cc7a693d3bdc9f066c4d3cc01a89/README.md"}, + {"label": "Formal Conjectures paper, arXiv v1", "url": "https://arxiv.org/abs/2605.13171v1"} + ], "sha256": "206fbdd02bb6f55040c0c6aa3173da79510d9f26b39f8519314886a8cd5f23b5", "provenance": "ai-generated-unreviewed" }, @@ -12,6 +16,10 @@ "file": "carleson.l4del", "repo": "fpvandoorn/carleson", "commit": "8972acdfd953c63bb2501ace20d61ced7c0697ec", + "sources": [ + {"label": "Pinned project documentation", "url": "https://github.com/fpvandoorn/carleson/blob/8972acdfd953c63bb2501ace20d61ced7c0697ec/README.md"}, + {"label": "Pinned Carleson blueprint", "url": "https://github.com/fpvandoorn/carleson/blob/8972acdfd953c63bb2501ace20d61ced7c0697ec/blueprint/src/chapter/main.tex"} + ], "sha256": "d419881f368932b5acc53d27296da73efe5e9e684a3b52dfa934b5c62728402c", "provenance": "ai-generated-unreviewed" }, @@ -19,6 +27,10 @@ "file": "flt.l4del", "repo": "ImperialCollegeLondon/FLT", "commit": "f6c6a2fe9796d6d89cd2a0d24e8a453729d881ff", + "sources": [ + {"label": "Pinned project documentation", "url": "https://github.com/ImperialCollegeLondon/FLT/blob/f6c6a2fe9796d6d89cd2a0d24e8a453729d881ff/README.md"}, + {"label": "Pinned FLT blueprint introduction", "url": "https://github.com/ImperialCollegeLondon/FLT/blob/f6c6a2fe9796d6d89cd2a0d24e8a453729d881ff/blueprint/src/chapter/ch01introduction.tex"} + ], "sha256": "cae45f492d97e1d2f40ffafcc6ee78b51b6cc8082759e32028b8fee001173e67", "provenance": "ai-generated-unreviewed" }, @@ -26,6 +38,10 @@ "file": "pfr.l4del", "repo": "teorth/pfr", "commit": "ce7ac95e620afe0ae448df63477de0b29e4dcf4d", + "sources": [ + {"label": "Pinned project documentation", "url": "https://github.com/teorth/pfr/blob/ce7ac95e620afe0ae448df63477de0b29e4dcf4d/README.md"}, + {"label": "Polynomial Freiman-Ruzsa proof paper, arXiv v2", "url": "https://arxiv.org/abs/2311.05762v2"} + ], "sha256": "410ce64ef99ddfed8caea0145b6c87c0a3367a18d55ea1fc85bcba81ad3b5523", "provenance": "ai-generated-unreviewed" }, @@ -33,6 +49,10 @@ "file": "compfiles.l4del", "repo": "dwrensha/compfiles", "commit": "47b19bbfe5f38dc49379a6b53008d2909c4d71c5", + "sources": [ + {"label": "Pinned compfiles documentation", "url": "https://github.com/dwrensha/compfiles/blob/47b19bbfe5f38dc49379a6b53008d2909c4d71c5/README.md"}, + {"label": "Pinned compfiles corpus index", "url": "https://github.com/dwrensha/compfiles/blob/47b19bbfe5f38dc49379a6b53008d2909c4d71c5/Compfiles.lean"} + ], "sha256": "49a34abe8c01a827fb13ba43288d59f2265619e1e0814c9f374c010da88e135a", "provenance": "ai-generated-unreviewed" }, @@ -40,6 +60,10 @@ "file": "mil.l4del", "repo": "leanprover-community/mathematics_in_lean", "commit": "dd6d752fedb14082f557913c2dccb2d4851e5173", + "sources": [ + {"label": "Pinned Mathematics in Lean documentation", "url": "https://github.com/leanprover-community/mathematics_in_lean/blob/dd6d752fedb14082f557913c2dccb2d4851e5173/README.md"}, + {"label": "Pinned Mathematics in Lean textbook", "url": "https://github.com/leanprover-community/mathematics_in_lean/blob/dd6d752fedb14082f557913c2dccb2d4851e5173/mathematics_in_lean.pdf"} + ], "sha256": "350a0527db91be06fc897939ee94d75020113c2b587802ffa28ac506d14df61c", "provenance": "ai-generated-unreviewed" }, @@ -47,14 +71,23 @@ "file": "tpil.l4del", "repo": "leanprover/theorem_proving_in_lean4", "commit": "4e28129fdd58037f8f5857548d5e99fe4fb0cc57", - "sha256": "2e4f408ca1865b2b8771e6c3c49a2d2f59fa94d4efd3d809fc95fe5a0409cf29", + "sources": [ + {"label": "Pinned Theorem Proving in Lean documentation", "url": "https://github.com/leanprover/theorem_proving_in_lean4/blob/4e28129fdd58037f8f5857548d5e99fe4fb0cc57/README.md"}, + {"label": "Pinned Theorem Proving in Lean 4 book index", "url": "https://github.com/leanprover/theorem_proving_in_lean4/blob/4e28129fdd58037f8f5857548d5e99fe4fb0cc57/book/TPiL.lean"} + ], + "sha256": "769189bc70b0b0f4f30b0eab64acd940ff690ff72cd2f69efc323d49cd58e3dc", "provenance": "ai-generated-unreviewed" }, "oai": { "file": "oai.l4del", "repo": "openai/math", "commit": "fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb", - "sha256": "00c457020aba4f1b7108c61ac939373f9dec945ec5692c1aa9345b96d1e2ed44", + "credit": "OpenAI's pinned repository says an unreleased internal model produced the manuscripts and supporting proof artifacts. The collection builds on the mathematics community's accumulated problems, results, language, and formal libraries; each manuscript's BibTeX and bibliography are the authority for individual scholarly credit.", + "sources": [ + {"label": "Pinned openai/math documentation", "url": "https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/README.md"}, + {"label": "Pinned formalization catalogue", "url": "https://github.com/openai/math/blob/fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb/lean/formalization.yaml"} + ], + "sha256": "56259df037bb701500b7c952ad7cf57f51efbf8f703ba872489904539237d86d", "provenance": "ai-generated-unreviewed" } } diff --git a/hosted/overlays/oai.l4del b/hosted/overlays/oai.l4del index c81024d06f..c3da6bb297 100644 --- a/hosted/overlays/oai.l4del +++ b/hosted/overlays/oai.l4del @@ -4343,7 +4343,7 @@ @file ComparatorChallenges/KLInvariance.lean @decl OAI.KLInvariance.NormalizedKL -- L4DEL: title: Exact equal-parameter normalization in the introduction --- L4DEL: intuition: Exact equal-parameter normalization in the introduction. The first family is R and the second is P. `reflect d p` is `q^d p(q⁻¹)` when `p.natDegree ≤ d`, which follows here from the degree bound (or the diagonal normalization). The sum is over the real Bruhat interval; its finiteness is a separate +-- L4DEL: intuition: Exact equal-parameter normalization in the introduction. The first family is R and the second is P. `reflect d p` is `q^d p(q⁻¹)` when `p.natDegree ≤ d`, which follows here from the degree bound (or the diagonal normalization). The sum is over the real Bruhat interval; its finiteness is a separate theorem, not a different definition of order. -- L4DEL: step: This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority. @file ComparatorChallenges/KLInvariance.lean @@ -5620,7 +5620,7 @@ @file ComparatorChallenges/PartitionConsistency.lean @decl OAI.PartitionConsistency.Derives -- L4DEL: title: Classical first-order natural deduction with equality --- L4DEL: intuition: Classical first-order natural deduction with equality. Hypotheses may be an infinite theory, but a derivation is a finite inductive proof. The `allI` and `exE` rules use a fresh last variable, and shift all assumptions to avoid capture. We allow finitely many free variables in proofs of closed sente +-- L4DEL: intuition: Classical first-order natural deduction with equality. Hypotheses may be an infinite theory, but a derivation is a finite inductive proof. The `allI` and `exE` rules use a fresh last variable, and shift all assumptions to avoid capture. We allow finitely many free variables in proofs of closed sentences. -- L4DEL: step: This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority. @file ComparatorChallenges/PartitionConsistency.lean @@ -6471,7 +6471,7 @@ @file ComparatorChallenges/RelativeGeneration.lean @decl OAI.RelativeGeneration.MainTarget -- L4DEL: title: Documented declaration: MainTarget --- L4DEL: intuition: Every irreducible inclusion of concrete type II₁ factors with separable predual of the larger factor has a dense Gδ full relative-generator locus in the normalized trace two-topology. The normalized faithful normal trace is asserted to exist; no representation, transport, cyclicity, or perturbation +-- L4DEL: intuition: Every irreducible inclusion of concrete type II₁ factors with separable predual of the larger factor has a dense Gδ full relative-generator locus in the normalized trace two-topology. The normalized faithful normal trace is asserted to exist; no representation, transport, cyclicity, or perturbation premise is imposed. -- L4DEL: step: This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority. @file ComparatorChallenges/RelativeGeneration.lean @@ -8186,7 +8186,7 @@ @file ComparatorChallenges/UniformKServer.lean @decl OAI.UniformKServer.UniformAlgorithmClaim -- L4DEL: title: Full uniform main objective in the explicit bit model, not a theorem or assumption --- L4DEL: intuition: Full uniform main objective in the explicit bit model, not a theorem or assumption. Machine transition steps are bit operations. Installing the standard input and reading/erasing the output adds only O(L + budget) charged bit operations, hence is absorbed by a single larger polynomial. A single dete +-- L4DEL: intuition: Full uniform main objective in the explicit bit model, not a theorem or assumption. Machine transition steps are bit operations. Installing the standard input and reading/erasing the output adds only O(L + budget) charged bit operations, hence is absorbed by a single larger polynomial. A single deterministic boot is sufficient for the source construction. -- L4DEL: step: This explanation is a condensed rendering of the declaration's own doc comment at the pinned source commit; consult the exact Lean statement below for authority. @file ComparatorChallenges/UniformSparsestCut.lean diff --git a/hosted/overlays/tpil.l4del b/hosted/overlays/tpil.l4del index d6b97832d2..680649abfc 100644 --- a/hosted/overlays/tpil.l4del +++ b/hosted/overlays/tpil.l4del @@ -186,12 +186,6 @@ -- L4DEL: intuition: ---- -- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. -@file book/TPiL/DependentTypeTheory.lean -@decl add --- L4DEL: title: Documented declaration: add --- L4DEL: intuition: --- --- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. - @file book/TPiL/DependentTypeTheory.lean @decl doTwice -- L4DEL: title: Documented declaration: doTwice @@ -366,30 +360,12 @@ -- L4DEL: intuition: ---- -- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. -@file book/TPiL/InductionAndRecursion.lean -@decl ack_gt_zero --- L4DEL: title: Documented declaration: ack_gt_zero --- L4DEL: intuition: ----------- --- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. - -@file book/TPiL/InductionAndRecursion.lean -@decl bar --- L4DEL: title: Documented declaration: bar --- L4DEL: intuition: ------ --- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. - @file book/TPiL/InductionAndRecursion.lean @decl f_or -- L4DEL: title: Documented declaration: f_or -- L4DEL: intuition: ---- -- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. -@file book/TPiL/InductionAndRecursion.lean -@decl foo --- L4DEL: title: Documented declaration: foo --- L4DEL: intuition: ------ --- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. - @file book/TPiL/InductionAndRecursion.lean @decl Hidden.and -- L4DEL: title: Documented declaration: and @@ -414,12 +390,6 @@ -- L4DEL: intuition: ---- -- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. -@file book/TPiL/InductionAndRecursion.lean -@decl sub1 --- L4DEL: title: Documented declaration: sub1 --- L4DEL: intuition: ------ --- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. - @file book/TPiL/InductionAndRecursion.lean @decl tail -- L4DEL: title: Documented declaration: tail @@ -432,12 +402,6 @@ -- L4DEL: intuition: ------ -- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. -@file book/TPiL/InductionAndRecursion.lean -@decl Vect.add --- L4DEL: title: Documented declaration: add --- L4DEL: intuition: ---- --- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. - @file book/TPiL/InductionAndRecursion.lean @decl Vect.head -- L4DEL: title: Documented declaration: head @@ -456,12 +420,6 @@ -- L4DEL: intuition: ----- -- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. -@file book/TPiL/InductionAndRecursion.lean -@decl zero_add --- L4DEL: title: Documented declaration: zero_add --- L4DEL: intuition: --- --- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. - @file book/TPiL/InductiveTypes.lean @decl Weekday.Weekday.Hidden.and -- L4DEL: title: Documented declaration: and @@ -546,24 +504,12 @@ -- L4DEL: intuition: ---- -- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. -@file book/TPiL/InductiveTypes.lean -@decl Weekday.Weekday.Hidden.zero_add --- L4DEL: title: Documented declaration: zero_add --- L4DEL: intuition: ---- --- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. - @file book/TPiL/InductiveTypes.lean @decl Weekday.Weekday.next_previous -- L4DEL: title: Documented declaration: next_previous -- L4DEL: intuition: ---- -- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. -@file book/TPiL/InductiveTypes.lean -@decl Weekday.Weekday.silly --- L4DEL: title: Documented declaration: silly --- L4DEL: intuition: ---- --- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. - @file book/TPiL/InteractingWithLean.lean @decl (example at line 470) -- L4DEL: title: Equivalent: @@ -600,12 +546,6 @@ -- L4DEL: intuition: ---- -- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. -@file book/TPiL/InteractingWithLean.lean -@decl List.isPrefix_self --- L4DEL: title: Documented declaration: isPrefix_self --- L4DEL: intuition: ---- --- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. - @file book/TPiL/InteractingWithLean.lean @decl {lit}`Nat`.(instance at line 1091) -- L4DEL: title: Documented declaration: (instance at line 1091) @@ -684,12 +624,6 @@ -- L4DEL: intuition: ---- -- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. -@file book/TPiL/PropositionsAndProofs.lean -@decl t1 --- L4DEL: title: Documented declaration: t1 --- L4DEL: intuition: ---- --- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. - @file book/TPiL/QuantifiersEquality.lean @decl (example at line 1014) -- L4DEL: title: Documented declaration: (example at line 1014) @@ -732,18 +666,6 @@ -- L4DEL: intuition: ---- -- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. -@file book/TPiL/QuantifiersEquality.lean -@decl even_plus_even --- L4DEL: title: Documented declaration: even_plus_even --- L4DEL: intuition: ---- --- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. - -@file book/TPiL/QuantifiersEquality.lean -@decl T --- L4DEL: title: Documented declaration: T --- L4DEL: intuition: ---- --- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. - @file book/TPiL/StructuresAndRecords.lean @decl with.p -- L4DEL: title: Documented declaration: p @@ -816,12 +738,6 @@ -- L4DEL: intuition: ---- -- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. -@file book/TPiL/TypeClasses.lean -@decl Ex.Ex.Add --- L4DEL: title: Documented declaration: Add --- L4DEL: intuition: ---- --- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. - @file book/TPiL/TypeClasses.lean @decl Ex.Ex.double -- L4DEL: title: Documented declaration: double @@ -893,10 +809,4 @@ -- L4DEL: title: Documented declaration: Morphism -- L4DEL: intuition: ---- -- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. - -@file book/TPiL/TypeClasses.lean -@decl Ex.Ex.s --- L4DEL: title: Documented declaration: s --- L4DEL: intuition: ---- --- L4DEL: step: This explanation is a condensed rendering of the declaration's own leading source comment at the pinned source commit; consult the exact Lean statement below for authority. # END GENERATED SOURCE-COMMENT ANNOTATIONS diff --git a/packages/corpora/src/lean4_explainer_corpora/extension.py b/packages/corpora/src/lean4_explainer_corpora/extension.py index 25121fbe09..5fcd531568 100644 --- a/packages/corpora/src/lean4_explainer_corpora/extension.py +++ b/packages/corpora/src/lean4_explainer_corpora/extension.py @@ -43,6 +43,10 @@ def register_cli(self, commands: argparse._SubParsersAction) -> None: build.add_argument("--out", type=Path, default=Path(_SITE_DEFAULT), help="output directory") build.add_argument("--work", type=Path, default=Path(_WORK_DEFAULT), help="where checkouts are kept") build.add_argument("--jobs", type=int, default=_DEFAULT_JOBS, help="worker processes for indexing") + build.add_argument( + "--site-url", + help="canonical public HTTPS URL for metadata, robots.txt and sitemaps (for example https://example.org/site/)", + ) build.add_argument( "--overlay-manifest", type=Path, @@ -116,6 +120,7 @@ def _showcase(args) -> int: link_out=[c for c in registry.installed().values() if c.name not in chosen], jobs=args.jobs, overlay_manifest=args.overlay_manifest, + site_url=args.site_url, ) except (ExplainerError, OSError) as exc: print(f"error: {exc}", file=sys.stderr) diff --git a/packages/corpora/src/lean4_explainer_corpora/overlays.py b/packages/corpora/src/lean4_explainer_corpora/overlays.py index 49e45a8fd2..236eca5fab 100644 --- a/packages/corpora/src/lean4_explainer_corpora/overlays.py +++ b/packages/corpora/src/lean4_explainer_corpora/overlays.py @@ -7,6 +7,7 @@ import re from dataclasses import dataclass from pathlib import Path +from urllib.parse import urlsplit from lean4_explainer.errors import ExplainerError @@ -21,6 +22,10 @@ } ) _SHA256_RE = re.compile(r"[0-9a-f]{64}") +DEFAULT_CREDIT = ( + "The upstream authors and contributors retain credit for the project and mathematics. " + "lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer." +) @dataclass(frozen=True) @@ -28,6 +33,8 @@ class HostedOverlay: path: Path provenance: str reviewed_by: str = "" + sources: tuple[tuple[str, str], ...] = () + credit: str = DEFAULT_CREDIT @property def disclosure(self) -> str: @@ -94,5 +101,28 @@ def load_overlay_manifest(path: Path, corpora: list[Corpus]) -> dict[str, Hosted raise ExplainerError(f"{where}: reviewed_by is required for {provenance}") if provenance == "ai-generated-unreviewed" and reviewed_by.strip(): raise ExplainerError(f"{where}: an unreviewed overlay cannot name a reviewer") - selected[corpus.name] = HostedOverlay(overlay, provenance, reviewed_by.strip()) + source_rows = entry.get("sources") + if not isinstance(source_rows, list) or not source_rows: + raise ExplainerError(f"{where}: sources must be a non-empty list of stable reference links") + sources: list[tuple[str, str]] = [] + for index, row in enumerate(source_rows, start=1): + if not isinstance(row, dict) or not isinstance(row.get("label"), str) or not row["label"].strip(): + raise ExplainerError(f"{where}: sources[{index}] needs a non-empty label") + url = row.get("url") + parsed = urlsplit(url) if isinstance(url, str) else None + if not parsed or parsed.scheme != "https" or not parsed.netloc or parsed.username or parsed.password: + raise ExplainerError(f"{where}: sources[{index}] must be an HTTPS URL without credentials") + if url in {found for _, found in sources}: + raise ExplainerError(f"{where}: source URL repeated: {url}") + sources.append((row["label"].strip(), url)) + credit = entry.get("credit", "") + if not isinstance(credit, str): + raise ExplainerError(f"{where}: credit must be a string") + selected[corpus.name] = HostedOverlay( + overlay, + provenance, + reviewed_by.strip(), + tuple(sources), + credit.strip() or DEFAULT_CREDIT, + ) return selected diff --git a/packages/corpora/src/lean4_explainer_corpora/showcase.py b/packages/corpora/src/lean4_explainer_corpora/showcase.py index eb6f3a4f69..5ba550018e 100644 --- a/packages/corpora/src/lean4_explainer_corpora/showcase.py +++ b/packages/corpora/src/lean4_explainer_corpora/showcase.py @@ -2,19 +2,21 @@ from __future__ import annotations +import json import os import subprocess import time from dataclasses import dataclass from html import escape from pathlib import Path +from urllib.parse import quote, urljoin, urlsplit from lean4_explainer.build import BuildSummary, build_site from lean4_explainer.config import PAGES_LIMIT_BYTES, Config from lean4_explainer.errors import ExplainerError from lean4_explainer.extensions import extensions from lean4_explainer.lake import LakeProject, include_patterns, read_lake -from lean4_explainer.render import ASSET_DIR, SITE_CSS +from lean4_explainer.render import ASSET_DIR, FAVICON_SVG, SITE_CSS from .registry import Corpus from .overlays import HostedOverlay, load_overlay_manifest @@ -29,12 +31,22 @@ h1 { font-size: 2.1rem; letter-spacing: 0.01em; } ol.list { counter-reset: none; padding: 0; } ol.list > li { list-style: none; background: var(--panel); border: 1px solid var(--line); border-left: 6px solid var(--card, var(--accent)); border-radius: 6px; padding: 0.8rem 1rem; margin-bottom: 0.8rem; } +.start { margin: 1rem 0 1.3rem; padding: 0.9rem 1rem; border: 1px solid var(--line); border-radius: 7px; background: var(--panel); } +.start h2 { margin-top: 0; } +.start ul { margin-bottom: 0; } +.card-actions { display: flex; flex-wrap: wrap; gap: 0.35rem 0.85rem; margin-top: 0.55rem; font-size: 0.92rem; } +.card-actions a { font-weight: 600; } """, ) GITHUB = "https://github.com" RAW = "https://raw.githubusercontent.com" _GIT_TIMEOUT_SECONDS = 1800 +SITE_REPOSITORY = "https://github.com/TimeLordRaps/lean4-explainer" +REPORT_URL = SITE_REPOSITORY + "/issues/new?title=Site%20feedback%3A%20" +SHOWCASE_DESCRIPTION = ( + "Explore declarations, source, grounded explanations, learning paths, and dependency maps across major Lean projects." +) @dataclass(frozen=True) @@ -88,8 +100,10 @@ def build_showcase( jobs: int = 1, fetch=fetch_corpus, overlay_manifest: Path | None = None, + site_url: str | None = None, ) -> ShowcaseResult: """Fetch every corpus first, so a failed download stops the run before anything is published.""" + public_url = _site_url(site_url) overlays = load_overlay_manifest(overlay_manifest, corpora) if overlay_manifest else {} checkouts = [(corpus, fetch(corpus, work_dir, base_url=base_url)) for corpus in corpora] out_dir.mkdir(parents=True, exist_ok=True) @@ -109,6 +123,10 @@ def build_showcase( source_links=corpus.source_links, byte_budget=byte_budget, home="../index.html", + site_url=f"{public_url}{corpus.name}/" if public_url else None, + description=f"Explore {corpus.title}: Lean declarations, pinned source, explanations, and dependencies.", + project_url=f"{GITHUB}/{corpus.repo}/tree/{corpus.commit}", + report_url=REPORT_URL, glossary=corpus.glossary, imports=corpus.imports, options=tuple( @@ -137,6 +155,7 @@ def build_showcase( items.append(ShowcaseItem(corpus, summary, project, time.monotonic() - started)) (out_dir / ASSET_DIR).mkdir(parents=True, exist_ok=True) (out_dir / ASSET_DIR / "site.css").write_text(SITE_CSS + LANDING_CSS, encoding="utf-8") + (out_dir / ASSET_DIR / "favicon.svg").write_text(FAVICON_SVG, encoding="utf-8") (out_dir / ".nojekyll").write_text("", encoding="utf-8") guide = next( (f"{i.corpus.name}/annotate.html" for i in items if (out_dir / i.corpus.name / "annotate.html").is_file()), @@ -145,9 +164,29 @@ def build_showcase( annotated = set(overlays) if any(ext.name == "l4del" for ext in extensions()) else set() curated = {i.corpus.name for i in items if (out_dir / i.corpus.name / "implications.html").is_file()} disclosures = {name: overlay.disclosure for name, overlay in overlays.items()} + credits = {name: overlay.credit for name, overlay in overlays.items()} + source_attributions = {name: overlay.sources for name, overlay in overlays.items()} + actions = _corpus_actions(items, out_dir) + start_links = _start_links(items, actions, out_dir) (out_dir / "index.html").write_text( - _landing(items, link_out or [], guide, annotated, curated, disclosures), encoding="utf-8" + _landing( + items, + link_out or [], + guide, + annotated, + curated, + disclosures, + actions, + start_links, + public_url, + credits=credits, + source_attributions=source_attributions, + ), + encoding="utf-8", ) + (out_dir / "404.html").write_text(_not_found(public_url), encoding="utf-8") + if public_url: + _write_discovery(out_dir, public_url) return ShowcaseResult(tuple(items), _tree_bytes(out_dir), byte_budget) @@ -161,6 +200,54 @@ def _copy_license(checkout: Path, target: Path, lean_root: str) -> None: return +def _site_url(value: str | None) -> str: + if not value: + return "" + parsed = urlsplit(value) + if parsed.scheme != "https" or not parsed.netloc or parsed.query or parsed.fragment: + raise ExplainerError("site_url must be an HTTPS URL without a query or fragment") + return value.rstrip("/") + "/" + + +def _corpus_actions(items: list[ShowcaseItem], out_dir: Path) -> dict[str, list[tuple[str, str]]]: + found: dict[str, list[tuple[str, str]]] = {} + for item in items: + name = item.corpus.name + root = out_dir / name + choices = [ + ("Browse", "index.html"), + ("Search", "search.html"), + ("Glossary", "glossary.html"), + ("Learn", "learning-path.html"), + ("Map", "map.html"), + ] + found[name] = [(label, f"{name}/{rel}") for label, rel in choices if (root / rel).is_file()] + return found + + +def _start_links( + items: list[ShowcaseItem], actions: dict[str, list[tuple[str, str]]], out_dir: Path +) -> list[tuple[str, str, str]]: + links: list[tuple[str, str, str]] = [] + titles = {item.corpus.name: item.corpus.title for item in items} + if (out_dir / "flt" / "FLT" / "Proof.lean.html").is_file(): + links.append(("Read an explained theorem", "flt/FLT/Proof.lean.html#L111", "Fermat's Last Theorem and its unfinished proof boundary")) + if (out_dir / "oai" / "search.html").is_file(): + links.append(("Search a concept", "oai/search.html?q=Hadwiger", "A shareable search in openai/math")) + for wanted, heading, detail in ( + ("Learn", "Follow a learning path", "Declarations ordered after their prerequisites"), + ("Glossary", "Use a project glossary", "Definitions and explanatory vocabulary"), + ): + match = next(((name, href) for name, rows in actions.items() for label, href in rows if label == wanted), None) + if match: + name, href = match + links.append((heading, href, f"{detail} in {titles[name]}")) + if not links and items: + first = items[0].corpus + links.append((f"Browse {first.title}", f"{first.name}/index.html", "Start at the corpus index")) + return links[:4] + + def _landing( items: list[ShowcaseItem], link_out: list[Corpus], @@ -168,8 +255,17 @@ def _landing( annotated: set[str] = frozenset(), # type: ignore[assignment] curated: set[str] = frozenset(), # type: ignore[assignment] disclosures: dict[str, str] | None = None, + actions: dict[str, list[tuple[str, str]]] | None = None, + start_links: list[tuple[str, str, str]] | None = None, + site_url: str = "", + credits: dict[str, str] | None = None, + source_attributions: dict[str, tuple[tuple[str, str], ...]] | None = None, ) -> str: disclosures = disclosures or {} + actions = actions or {} + start_links = start_links or [] + credits = credits or {} + source_attributions = source_attributions or {} cards = [] for item in items: corpus, summary, project = item.corpus, item.summary, item.project @@ -180,17 +276,40 @@ def _landing( mathlib = dict(project.pinned).get("mathlib") if project else None if mathlib: pins.append(f"mathlib {mathlib[:12]}") + corpus_actions = actions.get(corpus.name, ()) + action_html = "" + if corpus_actions: + action_html = ( + f'" + ) + attribution = "" + if corpus.name in annotated: + links = ", ".join( + f'{escape(label)}' + for label, url in source_attributions.get(corpus.name, ()) + ) + attribution = ( + f'
Credit: {escape(credits.get(corpus.name, ""))}' + + (f'
Primary project and mathematical sources: {links}.' if links else "") + ) cards.append( f'
  • {escape(corpus.title)} ' f'({escape(corpus.kind)})
    {escape(corpus.blurb)}
    ' f'{escape(", ".join(facts))}. {escape(", ".join(pins))}. ' - f'Source: {escape(corpus.repo)}. ' + f'Source: {escape(corpus.repo)} at the pinned commit. ' f'License: {escape(corpus.license)} (text).' + (f"
    {escape(corpus.license_note)}" if corpus.license_note else "") + ( "
    Selected declarations are explained with L4DEL from a hosted sidecar overlay; " "the upstream authors did not write these explanations and their sources are unchanged. " + "Each explanation links back to its exact pinned Lean source. " + escape(disclosures.get(corpus.name, "")) + + attribution if corpus.name in annotated else "" ) @@ -201,13 +320,31 @@ def _landing( if corpus.name in curated else "" ) - + "
    • " + + "    " + + action_html + + "" ) for corpus in link_out: cards.append( - f'
  • {escape(corpus.title)} ' + f'
  • {escape(corpus.title)} ' f'({escape(corpus.kind)}, not built into this site)
    {escape(corpus.blurb)}
    • ' ) + start = "" + if start_links: + rows = "".join( + f'
  • {escape(label)} — {escape(detail)}
    • ' + for label, href, detail in start_links + ) + start = f'

    Start exploring

    ' + canonical = f'' if site_url else "" + og_url = f'' if site_url else "" + audit = ( + '

    Annotation grounding audit (JSON): ' + "generated wording is checked against pinned source text; curated wording remains source-linked and " + "unreviewed.

    " + if annotated + else "" + ) return "\n".join( [ "", @@ -216,23 +353,39 @@ def _landing( '', '', "lean4-explainer showcase", + f'', + '', + f'', + '', + '', + canonical, + og_url, f'', + f'', "", "", - "
    ", + '', + '
    ', "

    lean4-explainer showcase

    ", "

    What lean4-explainer produces for the Lean projects below. Hosted annotations, when present, " - "carry their provenance beside the explanation. " + "carry their provenance and source grounding beside the explanation. " "To write your own explanations, start with the " - + (f'L4DEL guide' if guide else "L4DEL guide") - + ' or ' - "the README.

    ", + + ( + f'Lean4 Domain Explanation Language (L4DEL) guide' + if guide + else "Lean4 Domain Explanation Language (L4DEL) guide" + ) + + f' or the README.

    ', '

    Built from the source text only. Lean was not run, so axiom and trust checks are UNKNOWN ' "and sorry detection is textual.

    ", + audit, + start, + '

    All corpora

    ', '
      ', *cards, "
    ", "
    ", + f'', "", "", "", @@ -240,6 +393,64 @@ def _landing( ) +def _not_found(site_url: str) -> str: + base_path = urlsplit(site_url).path if site_url else "" + home = base_path or "index.html" + css = f"{base_path}{ASSET_DIR}/site.css" if base_path else f"{ASSET_DIR}/site.css" + icon = f"{base_path}{ASSET_DIR}/favicon.svg" if base_path else f"{ASSET_DIR}/favicon.svg" + return "\n".join( + [ + "", + '', + '', + '', + "Page not found — lean4-explainer", + f'', + f'', + "", + '

    That proof page is not here

    ', + "

    The corpus may have moved at a newer pinned commit, or the address may be incomplete.

    ", + f'

    Return to all corpora · Report a broken link

    ', + "
    ", + "", + ] + ) + + +def _write_discovery(out_dir: Path, site_url: str) -> None: + pages = sorted( + path.relative_to(out_dir).as_posix() + for path in out_dir.rglob("*.html") + if path.name != "404.html" + ) + urls = [urljoin(site_url, quote(path, safe="/")) for path in pages] + chunk_size = 45_000 + chunks = [urls[start : start + chunk_size] for start in range(0, len(urls), chunk_size)] or [[]] + for stale in out_dir.glob("sitemap-*.xml"): + stale.unlink() + names = [] + for number, chunk in enumerate(chunks, start=1): + name = f"sitemap-{number}.xml" + names.append(name) + body = "".join(f"{escape(url)}" for url in chunk) + (out_dir / name).write_text( + '\n' + + body + + "\n", + encoding="utf-8", + ) + index = "".join(f"{escape(urljoin(site_url, name))}" for name in names) + (out_dir / "sitemap.xml").write_text( + '\n' + + index + + "\n", + encoding="utf-8", + ) + (out_dir / "robots.txt").write_text( + f"User-agent: *\nAllow: /\nSitemap: {urljoin(site_url, 'sitemap.xml')}\n", encoding="utf-8" + ) + + def _overlay_options(overlay: HostedOverlay | None) -> list[tuple[str, object]]: if overlay is None: return [] @@ -247,6 +458,8 @@ def _overlay_options(overlay: HostedOverlay | None) -> list[tuple[str, object]]: ("overlay", str(overlay.path)), ("overlay_provenance", overlay.provenance), ("overlay_disclosure", overlay.disclosure), + ("overlay_sources", json.dumps(overlay.sources, ensure_ascii=False, separators=(",", ":"))), + ("overlay_credit", overlay.credit), ] diff --git a/packages/corpora/tests/test_cli_corpora.py b/packages/corpora/tests/test_cli_corpora.py index 27ad0f8ed1..d79310f7e2 100644 --- a/packages/corpora/tests/test_cli_corpora.py +++ b/packages/corpora/tests/test_cli_corpora.py @@ -96,14 +96,18 @@ def test_showcase_with_yes_builds_and_reports(tmp_path, monkeypatch, capsys): seen = {} def fake(corpora, work, out, **kwargs): - seen.update(names=[c.name for c in corpora], out=out, jobs=kwargs["jobs"]) + seen.update(names=[c.name for c in corpora], out=out, jobs=kwargs["jobs"], site_url=kwargs["site_url"]) return ShowcaseResult((), 1234, 1000) monkeypatch.setattr(extension.showcase, "build_showcase", fake) - code = cli.main(["showcase", "tutorials", "--yes", "--out", str(tmp_path / "s"), "--work", str(tmp_path / "w")]) + code = cli.main([ + "showcase", "tutorials", "--yes", "--site-url", "https://example.org/proofs/", + "--out", str(tmp_path / "s"), "--work", str(tmp_path / "w") + ]) assert seen["names"] == ["mil", "tpil"] + assert seen["site_url"] == "https://example.org/proofs/" assert code == 1 # the fake result is over its budget assert "over" in capsys.readouterr().err diff --git a/packages/corpora/tests/test_corpora.py b/packages/corpora/tests/test_corpora.py index 18d11e9ccf..778da177b7 100644 --- a/packages/corpora/tests/test_corpora.py +++ b/packages/corpora/tests/test_corpora.py @@ -89,8 +89,8 @@ def test_every_extra_installs_the_packages_of_its_corpora(): for extra, names in EXTRAS.items(): wanted = {f"lean4-explainer-{name}" for name in names} assert {item.split(">")[0].split("=")[0] for item in extras[extra]} >= wanted, extra - assert extras["l4del"] == ["lean4-explainer-l4del>=0.3.0"] # the version that leaves the map and the glossary page to others - assert "lean4-explainer-l4del>=0.3.0" in extras["all"] + assert extras["l4del"] == ["lean4-explainer-l4del>=0.5.0"] # legends and linked quotes; overlays remain hosted-only + assert "lean4-explainer-l4del>=0.5.0" in extras["all"] # 0.2.0 follows imports through files that only import (the core's import graph, core 0.3.0) assert extras["map"] == ["lean4-explainer-map>=0.2.0"] and "lean4-explainer-map>=0.2.0" in extras["all"] # 0.4.0 carries the proved edge's bridge, its verification record and the discovered catalogue diff --git a/packages/corpora/tests/test_hosted_overlays.py b/packages/corpora/tests/test_hosted_overlays.py index 601b6a1e80..4cc2257b1d 100644 --- a/packages/corpora/tests/test_hosted_overlays.py +++ b/packages/corpora/tests/test_hosted_overlays.py @@ -18,7 +18,7 @@ "mil": 74, "oai": 1316, "pfr": 523, - "tpil": 144, + "tpil": 129, } @@ -31,6 +31,8 @@ def test_real_hosted_overlays_are_bound_parseable_and_annotation_rich(): for name, hosted in selected.items(): assert hosted.path.parent == HOSTED assert hosted.provenance == "ai-generated-unreviewed" + assert len(hosted.sources) >= 2 + assert all(url.startswith("https://") for _, url in hosted.sources) overlay = parse_overlay(hosted.path.read_text(encoding="utf-8"), str(hosted.path)) counts[name] = sum(len(declarations) for declarations in overlay.files.values()) for file, declarations in overlay.files.items(): @@ -44,4 +46,4 @@ def test_real_hosted_overlays_are_bound_parseable_and_annotation_rich(): assert not errors assert counts == EXPECTED - assert sum(counts.values()) == 14_990 + assert sum(counts.values()) == 14_975 diff --git a/packages/corpora/tests/test_showcase.py b/packages/corpora/tests/test_showcase.py index 9c64e617e8..1d5585b37c 100644 --- a/packages/corpora/tests/test_showcase.py +++ b/packages/corpora/tests/test_showcase.py @@ -10,7 +10,7 @@ from lean4_explainer.errors import ExplainerError from lean4_explainer_corpora import CorporaExtension, installed -from lean4_explainer_corpora.showcase import build_showcase, fetch_corpus +from lean4_explainer_corpora.showcase import GITHUB, build_showcase, fetch_corpus CORPORA = installed() @@ -96,6 +96,37 @@ def test_showcase_builds_a_subsite_per_corpus_and_a_landing_page(upstream, tmp_p assert (out / ".nojekyll").is_file() +def test_public_showcase_has_onboarding_metadata_recovery_and_discovery_files(upstream, tmp_path): + corpus, base = upstream + out = tmp_path / "site" + public = "https://example.org/lean/" + + build_showcase([corpus], tmp_path / "work", out, base_url=base, site_url=public) + + landing = (out / "index.html").read_text(encoding="utf-8") + assert "Start exploring" in landing + assert 'aria-label="Explore Demo corpus"' in landing + assert '>Browse' in landing and '>Search' in landing and '>Glossary' in landing + assert '' in landing + assert f"{GITHUB}/{corpus.repo}/tree/{corpus.commit}" in landing + assert (out / "404.html").is_file() and "Return to all corpora" in (out / "404.html").read_text(encoding="utf-8") + assert f"Sitemap: {public}sitemap.xml" in (out / "robots.txt").read_text(encoding="utf-8") + assert "sitemap-1.xml" in (out / "sitemap.xml").read_text(encoding="utf-8") + assert f"{public}demo/index.html" in (out / "sitemap-1.xml").read_text(encoding="utf-8") + subsite = (out / "demo" / "index.html").read_text(encoding="utf-8") + assert f'' in subsite + assert ">Project source" in subsite and ">Report a site issue" in subsite + assert (out / "_assets" / "favicon.svg").is_file() + + +def test_showcase_rejects_a_non_https_public_url(upstream, tmp_path): + corpus, base = upstream + + with pytest.raises(ExplainerError, match="site_url"): + build_showcase([corpus], tmp_path / "work", tmp_path / "site", base_url=base, site_url="http://example.org/") + + def test_showcase_copies_each_license_and_shows_it_on_the_landing_page(upstream, tmp_path): corpus, base = upstream corpus = replace(corpus, license="Apache-2.0", license_note="Parts are CC-BY-SA 4.0.") @@ -194,6 +225,9 @@ def test_a_corpus_overlay_annotates_the_subsite_and_the_landing_says_who_wrote_i "commit": corpus.commit, "sha256": hashlib.sha256(overlay.read_bytes()).hexdigest(), "provenance": "ai-generated-unreviewed", + "sources": [ + {"label": "Pinned documentation", "url": "https://example.org/repo/blob/abc/README.md"} + ], } }, } @@ -211,9 +245,16 @@ def test_a_corpus_overlay_annotates_the_subsite_and_the_landing_says_who_wrote_i assert "A sidecar title" in page assert "AI-generated and not human-reviewed" in page assert "not mathematical authority" in page + assert "Pinned Lean source" in page and "Pinned documentation" in page + assert "https://example.org/repo/blob/abc/README.md" in page landing = (out / "index.html").read_text(encoding="utf-8") assert "hosted sidecar overlay" in landing and "did not write these explanations" in landing assert "AI-generated and not human-reviewed" in landing + assert "Lean4 Domain Explanation Language (L4DEL) guide" in landing + assert "Primary project and mathematical sources" in landing + assert "upstream authors and contributors retain credit" in landing + assert 'href="annotation-audit.json"' in landing + assert "curated wording remains source-linked and unreviewed" in landing assert build_site_result.total_bytes > 0 @@ -248,6 +289,8 @@ def test_overlay_manifest_fails_closed_when_its_binding_is_wrong(upstream, tmp_p "commit": corpus.commit, "sha256": hashlib.sha256(overlay.read_bytes()).hexdigest(), "provenance": "human-authored", + "reviewed_by": "A reviewer", + "sources": [{"label": "Pinned documentation", "url": "https://example.org/repo/blob/abc/README.md"}], } entry[field] = value manifest = tmp_path / "manifest.json" diff --git a/packages/ecosystem/src/lean4_explainer_ecosystem/extension.py b/packages/ecosystem/src/lean4_explainer_ecosystem/extension.py index c994f41cc9..6f716c355e 100644 --- a/packages/ecosystem/src/lean4_explainer_ecosystem/extension.py +++ b/packages/ecosystem/src/lean4_explainer_ecosystem/extension.py @@ -141,7 +141,7 @@ def _find_page(ctx) -> str: '', '', ] - return page("Find", 0, body, ctx) + return page("Find", 0, body, ctx, canonical_path="find.html") def _names_script(ctx, limit: int) -> str: @@ -156,7 +156,7 @@ def _changes_page(ctx, analysis: Analysis) -> str: body = ["

    Changes since the baseline

    "] if analysis.changes is None: body.append(f'

    {escape(analysis.baseline_error or "No baseline was compared.")}

    ') - return page("Changes", 0, body, ctx) + return page("Changes", 0, body, ctx, canonical_path="changes.html") c = analysis.changes if c.level != "declaration": body.append( @@ -181,4 +181,4 @@ def _changes_page(ctx, analysis: Analysis) -> str: body.append("") if not any(rows for _, rows in sections): body.append("

    Nothing changed.

    ") - return page("Changes", 0, body, ctx) + return page("Changes", 0, body, ctx, canonical_path="changes.html") diff --git a/packages/implications/src/lean4_explainer_implications/extension.py b/packages/implications/src/lean4_explainer_implications/extension.py index af21e4490b..eec392c306 100644 --- a/packages/implications/src/lean4_explainer_implications/extension.py +++ b/packages/implications/src/lean4_explainer_implications/extension.py @@ -244,13 +244,24 @@ def pages(self, ctx, analysis: Analysis) -> Mapping[str, str]: for shard in sorted((cat_dir / "shards").glob("*.json")): out[f"implications/catalogue/shards/{shard.name}"] = shard.read_text(encoding="utf-8") out["implications/catalogue.js"] = CS.script() - out["implications/catalogue.html"] = page("Checked implications", 1, CS.catalogue_body(analysis.catalogue) - + [''], ctx) + out["implications/catalogue.html"] = page( + "Checked implications", + 1, + CS.catalogue_body(analysis.catalogue) + [''], + ctx, + canonical_path="implications/catalogue.html", + ) if analysis.catalogue is not None or analysis.path: argued = [(e.id, f"{', '.join(_bare(s) for s in e.sources)} → {_bare(e.target) or 'a composite'}") for e in analysis.found.edges if e.status in ("argued", "proposed")] cands = [(c.id, c.phrase) for c in analysis.found.candidates] if analysis.catalogue is not None or argued or cands: - out["implications/notes.html"] = page("Implication notes", 1, CS.notes_body(analysis.catalogue or {}, argued, cands), ctx) + out["implications/notes.html"] = page( + "Implication notes", + 1, + CS.notes_body(analysis.catalogue or {}, argued, cands), + ctx, + canonical_path="implications/notes.html", + ) return out def glossary(self, ctx, analysis: Analysis) -> Sequence[GlossarySection]: @@ -416,7 +427,7 @@ def _bridge_source_page(ctx, analysis: Analysis, rel: str, sha: str, text: str) + "", f'
    {lines}
    ', ] - return page(rel, depth, body, ctx) + return page(rel, depth, body, ctx, canonical_path=_bridge_page(rel)) def _index_page(ctx, analysis: Analysis, kernel) -> str: @@ -467,7 +478,7 @@ def _index_page(ctx, analysis: Analysis, kernel) -> str: ) body.append("") body.append('

    The same edges as data: implications.json.

    ') - return page("Implications", 0, body, ctx) + return page("Implications", 0, body, ctx, canonical_path="implications.html") def _edge_card(ctx, analysis: Analysis, edge: E.Edge, kernel) -> str: diff --git a/packages/l4del/README.md b/packages/l4del/README.md index ab39182709..987ec8e972 100644 --- a/packages/l4del/README.md +++ b/packages/l4del/README.md @@ -1,9 +1,13 @@ # lean4-explainer-l4del -L4DEL (Lean4 Domain Explanation Language) for [lean4-explainer](https://github.com/TimeLordRaps/lean4-explainer). +Lean4 Domain Explanation Language (L4DEL) for [lean4-explainer](https://github.com/TimeLordRaps/lean4-explainer). L4DEL is a set of `-- L4DEL: key: value` line comments that add titles, intuition, proof steps, prerequisites, related -declarations and glossary terms to a declaration. This package adds them to the generated site (the terms to its glossary page), plus a +declarations, glossary terms, top-of-page acronym legends, structured source citations, and linked quotations to a declaration. A citation uses +`-- L4DEL: source: label = https://stable.example/source`; it is displayed beside the explanation and may be repeated. +An acronym uses `-- L4DEL: acronym: SHORT = expansion`. A quotation uses +`-- L4DEL: quote: source label = exact excerpt` and must name one of the annotation's sources. +This package adds them to the generated site (the terms to its glossary page), plus a learning path ordered by prerequisites, an annotation guide, and the `check` and `annotate` commands. ``` diff --git a/packages/l4del/pyproject.toml b/packages/l4del/pyproject.toml index 4a748a012d..b88b485ef5 100644 --- a/packages/l4del/pyproject.toml +++ b/packages/l4del/pyproject.toml @@ -4,8 +4,8 @@ build-backend = "hatchling.build" [project] name = "lean4-explainer-l4del" -version = "0.3.0" -description = "L4DEL (Lean4 Domain Explanation Language) for lean4-explainer: comment-based titles, intuition, steps, prerequisites, glossary and learning path." +version = "0.5.0" +description = "Lean4 Domain Explanation Language (L4DEL) for lean4-explainer: sourced explanations, acronym legends, linked quotes, glossary and learning paths." readme = "README.md" requires-python = ">=3.11" license = "Apache-2.0" diff --git a/packages/l4del/src/lean4_explainer_l4del/__init__.py b/packages/l4del/src/lean4_explainer_l4del/__init__.py index 825642ec75..35ef333563 100644 --- a/packages/l4del/src/lean4_explainer_l4del/__init__.py +++ b/packages/l4del/src/lean4_explainer_l4del/__init__.py @@ -1,4 +1,4 @@ -"""L4DEL (Lean4 Domain Explanation Language) extension for lean4-explainer.""" +"""Lean4 Domain Explanation Language (L4DEL) extension for lean4-explainer.""" from .extension import L4delExtension, __version__ from .grammar import L4Notes, parse_l4del diff --git a/packages/l4del/src/lean4_explainer_l4del/extension.py b/packages/l4del/src/lean4_explainer_l4del/extension.py index 80c504760c..fdaab55111 100644 --- a/packages/l4del/src/lean4_explainer_l4del/extension.py +++ b/packages/l4del/src/lean4_explainer_l4del/extension.py @@ -9,6 +9,7 @@ import argparse import hashlib +import json import re import sys from collections.abc import Mapping, Sequence @@ -22,26 +23,37 @@ from lean4_explainer.errors import ExplainerError from lean4_explainer.extensions import Diagnostic, Extension, GlossaryEntry, GlossarySection, ParseResult, SourceView from lean4_explainer.objects import Objects -from lean4_explainer.render import Context, href, page, refs, up_path +from lean4_explainer.render import Context, filter_box, href, page, refs, source_href, up_path from lean4_explainer.scan import Declaration, parse_source from .grammar import L4Notes, parse_l4del -from .graph import PathStep, build_glossary, build_learning_path, build_links, merge_notes, unresolved_links +from .graph import PathStep, build_acronyms, build_glossary, build_learning_path, build_links, merge_notes, unresolved_links from .model import FileSummary, Note from .overlay import load_overlay from .templates import annotation_report, annotation_state, notes_of, placeholder_block -__version__ = "0.3.0" +__version__ = "0.5.0" _PREFIX = "L4DEL:" _CARRIER_RE = re.compile(r"^[ \t]*L4DEL:(?P.*)$") _WARNING_PREVIEW = 20 -_CACHE_SCHEMA = 2 # L4Notes gained overlay origin/provenance rendering in schema 2. +_CACHE_SCHEMA = 6 # Navigation names the purpose without introducing an unexplained acronym. +_ACRONYM_TOKEN_RE = re.compile(r"(? keys it builds on sees: dict = field(default_factory=dict, repr=False) # key -> related keys (both directions) @@ -85,9 +101,14 @@ class L4delExtension(Extension): "overlay": str, "overlay_provenance": str, "overlay_disclosure": str, + "overlay_sources": str, + "overlay_credit": str, } # overlay: a sidecar file of annotations (see overlay.py) # ---- parsing and indexing ---- + def promote_file_page(self, lean_file: Any) -> bool: + return any(self.name in declaration.ext for declaration in lean_file.declarations) + def hides_comment(self, body: str) -> bool: return body.strip().startswith(_PREFIX) @@ -95,7 +116,7 @@ def is_described(self, payload: Any) -> bool: return not payload.is_empty def describe(self, payload: Any) -> str: - return payload.intuition or payload.title or "" + return payload.intuition or (payload.quotes[0][1] if payload.quotes else None) or payload.title or "" def parse(self, view: SourceView) -> ParseResult: diagnostics: list[Diagnostic] = [] @@ -147,10 +168,11 @@ def index_file(self, path: str, declarations: Sequence[Declaration], diagnostics prereqs=n.prereqs, see=n.see, terms=n.terms, + acronyms=n.acronyms, ) for decl in named for n in (notes_of(decl),) - if n.title or n.prereqs or n.see or n.terms + if n.title or n.prereqs or n.see or n.terms or n.acronyms ) issues = tuple( f"{d.severity}: {path}:{d.line}: {d.message}" for decl in declarations for d in notes_of(decl).diagnostics @@ -180,15 +202,17 @@ def analyze(self, objects: Objects, summaries: Mapping[str, Any], options: Mappi unannotated += summary.unannotated merged, merge_issues = merge_notes(notes, objects) terms, term_issues = build_glossary(merged) + acronyms, acronym_issues = build_acronyms(merged) use_path = bool(options.get("learning_path", True)) steps, path_issues = build_learning_path(merged, objects) if use_path else ([], []) prereq_edges, see_edges = build_links(merged, objects) - graph_issues = [*merge_issues, *path_issues, *unresolved_links(notes, objects)] + graph_issues = [*merge_issues, *acronym_issues, *path_issues, *unresolved_links(notes, objects)] words = sorted(terms, key=len, reverse=True) pattern = re.compile(r"(? str: overlay = load_overlay(str(path)).digest[:16] if path else "" disclosure = str(options.get("overlay_disclosure", "")) disclosure_digest = hashlib.sha256(disclosure.encode("utf-8")).hexdigest()[:16] if disclosure else "" + sources = str(options.get("overlay_sources", "")) + sources_digest = hashlib.sha256(sources.encode("utf-8")).hexdigest()[:16] if sources else "" + credit = str(options.get("overlay_credit", "")) + credit_digest = hashlib.sha256(credit.encode("utf-8")).hexdigest()[:16] if credit else "" return ( f"l4del:{__version__}:schema={_CACHE_SCHEMA}:learning_path={options.get('learning_path', True)}:" - f"overlay={overlay}:provenance={options.get('overlay_provenance', '')}:disclosure={disclosure_digest}" + f"overlay={overlay}:provenance={options.get('overlay_provenance', '')}:" + f"disclosure={disclosure_digest}:sources={sources_digest}:credit={credit_digest}" ) # ---- rendering ---- @@ -227,6 +256,19 @@ def declaration_blocks( top: list[str] = [] depth = len(dirs) options = dict(ctx.options) + sources = list(payload.sources) + if payload.origin == "overlay" and ctx.source_url: + pinned = source_href(rel, decl.line, ctx) + if pinned not in {url for _, url in sources}: + ref = ctx.source_ref[:12] if ctx.source_ref else "configured revision" + sources.insert(0, (f"Pinned Lean source ({ref})", pinned)) + if payload.origin == "overlay": + for shared in _overlay_sources(options.get("overlay_sources")): + if shared[1] not in {url for _, url in sources}: + sources.append(shared) + source_by_label = {label: url for label, url in sources} + if payload.origin == "overlay" and sources: + source_by_label.setdefault("Pinned Lean source", sources[0][1]) disclosure = str(options.get("overlay_disclosure", "")).strip() if not disclosure and options.get("overlay_provenance") == "ai-generated-unreviewed": disclosure = ( @@ -238,6 +280,17 @@ def declaration_blocks( '" ) + for label, excerpt in payload.quotes: + url = source_by_label.get(label, "") + citation = ( + f'{escape(label)}' + if url + else f'{escape(label)} (source link unresolved)' + ) + top.append( + f'
    ' + f'

    {_highlight(excerpt, analysis, depth)}

    — {citation}
    ' + ) if payload.intuition: top.append(f'

    {_highlight(payload.intuition, analysis, depth)}

    ') if payload.steps: @@ -247,6 +300,11 @@ def declaration_blocks( top.append(refs("Prerequisites", payload.prereqs, None, dirs, ctx)) if payload.see: top.append(refs("See also", payload.see, None, dirs, ctx)) + if sources: + links = ", ".join( + f'{escape(label)}' for label, url in sources + ) + top.append(f'

    Sources and attribution: {links}

    ') bottom = [ f'

    {escape(word)}: {escape(definition)}

    ' for word, definition in payload.terms @@ -255,8 +313,61 @@ def declaration_blocks( bottom.append(_hint(decl, payload, ctx)) return "".join(top), "".join(bottom) + def file_preamble(self, lean_file: Any, ctx: Context, analysis: Analysis) -> str: + payloads = [ + payload + for declaration in lean_file.declarations + for payload in (declaration.ext.get(self.name),) + if isinstance(payload, L4Notes) and not payload.is_empty + ] + if not payloads: + return "" + tokens = {"L4DEL"} + for payload in payloads: + parts = [ + payload.title or "", + payload.intuition or "", + *payload.steps, + *(definition for _, definition in payload.terms), + *(excerpt for _, excerpt in payload.quotes), + ] + tokens.update(token for part in parts for token in _ACRONYM_TOKEN_RE.findall(part)) + tokens.update(short for short, _ in payload.acronyms) + project_acronyms = analysis.acronyms if isinstance(analysis, Analysis) else {} + local_acronyms = {short: expansion for payload in payloads for short, expansion in payload.acronyms} + definitions = { + "L4DEL": _L4DEL_EXPANSION, + **{key: value[0] for key, value in project_acronyms.items()}, + **local_acronyms, + } + rows = [] + for token in sorted(tokens, key=str.casefold): + expansion = definitions.get(token) + if expansion: + meaning = escape(expansion) + else: + meaning = "Used in an explanation or its source, but not expanded by this annotation. Follow its linked source." + rows.append(f'
    {escape(token)}
    {meaning}
    ') + options = dict(ctx.options) + credit = str(options.get("overlay_credit", "")).strip() + shared = _overlay_sources(options.get("overlay_sources")) + source_links = "" + if shared: + links = ", ".join( + f'{escape(label)}' for label, url in shared + ) + source_links = f'

    Project sources: {links}

    ' + credit_html = f'

    Credit: {escape(credit)}

    ' if credit else "" + return ( + '
    ' + '

    Explanation legend

    ' + '

    L4DEL explanations are a separate layer. They do not change the Lean source. ' + 'Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

    ' + f'
    {"".join(rows)}
    {credit_html}{source_links}
    ' + ) + def nav_links(self, up: str, options: Mapping[str, Any]) -> Sequence[tuple[str, str]]: - links = [("L4DEL guide", f"{up}annotate.html")] # the core links its glossary page, which lists the terms + links = [("Explanation guide", f"{up}annotate.html")] if options.get("learning_path", True): links.append(("Learning path", f"{up}learning-path.html")) return links @@ -272,8 +383,25 @@ def glossary(self, ctx: Context, analysis: Analysis) -> Sequence[GlossarySection GlossaryEntry(term=term, meaning=escape(definition), where=(rel, line, decl_name), anchor=analysis.anchors[term]) for term, (definition, decl_name, (rel, line)) in analysis.terms.items() ) - intro = "Words defined in the explanations on this site (L4DEL term lines). Where they appear, they link here." - return (GlossarySection(key="l4del", title="Terms from the explanations", entries=entries, intro=intro),) + intro = ( + "Words defined in the explanations on this site (Lean4 Domain Explanation Language term lines). " + "Where they appear, they link here." + ) + acronym_entries = tuple( + GlossaryEntry(term=short, meaning=escape(expansion), where=(rel, line, decl_name)) + for short, (expansion, decl_name, (rel, line)) in analysis.acronyms.items() + ) + sections = [GlossarySection(key="l4del", title="Terms from the explanations", entries=entries, intro=intro)] + if acronym_entries: + sections.append( + GlossarySection( + key="l4del-acronyms", + title="Acronyms from the explanations", + entries=acronym_entries, + intro="Explicit expansions supplied by acronym lines and repeated in each affected page's legend.", + ) + ) + return tuple(sections) def status(self, analysis: Analysis) -> str: return ( @@ -372,6 +500,24 @@ def _highlight(text: str, analysis: Analysis, depth: int) -> str: return "".join(pieces) +def _overlay_sources(raw: object) -> tuple[tuple[str, str], ...]: + if not raw: + return () + try: + rows = json.loads(str(raw)) + except json.JSONDecodeError as exc: + raise ExplainerError(f"overlay_sources is not valid JSON: {exc}") from exc + if not isinstance(rows, list) or not all( + isinstance(row, list) + and len(row) == 2 + and all(isinstance(value, str) and value for value in row) + and row[1].startswith("https://") + for row in rows + ): + raise ExplainerError("overlay_sources must be a JSON list of [label, https://URL] pairs") + return tuple((row[0], row[1]) for row in rows) + + def _hint(decl: Declaration, payload: L4Notes, ctx: Context) -> str: objects = ctx.objects ambiguous = objects.ambiguous if objects else frozenset() @@ -387,7 +533,8 @@ def _hint(decl: Declaration, payload: L4Notes, ctx: Context) -> str: def _learning_path_page(steps: list[PathStep], warnings: list[str], ctx: Context) -> str: body = ["

    Learning path

    ", '

    Each declaration appears after its prerequisites.

    '] if steps: - body.append('
      ') + body.append(filter_box("Filter learning path")) + body.append('
        ') for step in steps: rel, line = step.location link = escape(href([], rel, f"#L{line}"), quote=True) @@ -402,13 +549,20 @@ def _learning_path_page(steps: list[PathStep], warnings: list[str], ctx: Context if warnings: body.append("

        Warnings

        ") body.append('
          ' + "".join(f'
        • {escape(w)}
          • ' for w in warnings) + "
        ") - return page("Learning path", 0, body, ctx) + return page("Learning path", 0, body, ctx, canonical_path="learning-path.html") def _guide_page(ctx: Context) -> str: body = [ - "

        Annotating with L4DEL

        ", - '

        lean4-explainer reads L4DEL from Lean line comments. An annotation is optional at first. ' + "

        Lean4 Domain Explanation Language (L4DEL)

        ", + '
        ' + '

        Acronym legend

        ' + f'
        L4DEL
        ' + f'
        {_L4DEL_EXPANSION}
        ' + '

        A domain explanation language keeps expert meaning, provenance, definitions, and reading order explicit ' + 'instead of asking a reader to infer them from jargon.

        ', + '

        lean4-explainer reads Lean4 Domain Explanation Language directives from Lean line comments. ' + "An annotation is optional at first. " "The tool checks every directive it finds, and for each declaration without a valid annotation it " "prints a template to paste in.

        ", "

        Workflow

        ", @@ -427,7 +581,17 @@ def _guide_page(ctx: Context) -> str: "
      1. prereq: comma-separated fully qualified names the proof depends on.
        2. " "
      2. see: comma-separated related declarations.
        3. " "
      3. term: word = definition. Each word is defined once in the project.
        4. " + "
      4. acronym: SHORT = expansion. The expansion appears in the legend at the top " + "of every affected file page. Acronym-looking source text without a supplied expansion is labeled as unresolved; " + "the renderer never guesses what an upstream author meant.
        5. " + "
      5. source: label = https://URL. Repeat it for independent sources.
        6. " + "
      6. quote: source label = exact excerpt. The label must match a source line; the " + "excerpt is rendered as a linked quotation rather than being passed off as the explainer's prose.
        7. " "", + "

        Sources and attribution

        ", + "

        Use immutable links where possible: a full-commit repository blob for the exact formal source, " + "a DOI or versioned arXiv record for a paper, or a versioned project blueprint. A citation makes an " + "explanation traceable; it does not by itself certify that the explanation is correct.

        ", "

        Rules

        ", "

        Only line comments carry directives. A directive attaches to the next declaration. " "Anonymous declarations cannot carry directives. Keys are case-sensitive. " @@ -439,4 +603,4 @@ def _guide_page(ctx: Context) -> str: "

        Example

        ", f"
        {escape(_GUIDE_EXAMPLE)}
        ", ] - return page("L4DEL guide", 0, body, ctx) + return page("Lean4 Domain Explanation Language (L4DEL) guide", 0, body, ctx, canonical_path="annotate.html") diff --git a/packages/l4del/src/lean4_explainer_l4del/grammar.py b/packages/l4del/src/lean4_explainer_l4del/grammar.py index 1f15312144..80d8afad06 100644 --- a/packages/l4del/src/lean4_explainer_l4del/grammar.py +++ b/packages/l4del/src/lean4_explainer_l4del/grammar.py @@ -4,7 +4,7 @@ carrier = "--" , { " " | "\t" } , "L4DEL:" , ( " " | "\t" ) , directive ; directive = key , ":" , value ; - key = "title" | "intuition" | "step" | "prereq" | "see" | "term" ; + key = "title" | "intuition" | "step" | "prereq" | "see" | "term" | "acronym" | "source" | "quote" ; Rules: - Only line comments are carriers. "L4DEL:" inside a block, doc, or module comment is an error. @@ -17,6 +17,13 @@ declaration, is an error. - term: "word = definition". word is the text before the first "=", trimmed. definition is the rest, trimmed. Both must be non-empty. A word may be defined only once in the whole project. +- acronym: "SHORT = expansion". SHORT is two or more uppercase letters, digits, or hyphens, starting + with a letter. Definitions are collected into the explanation legend at the top of each affected page. +- source: "label = https://url". Labels and URLs must be non-empty, URLs must use HTTPS, and the + same URL may appear only once on a declaration. Source may be repeated to cite independent material. +- quote: "source label = exact excerpt". The label must name a source on the annotation. Hosted + overlays may use the reserved label "Pinned Lean source", which the renderer binds to the exact + declaration at the configured commit. Quote may be repeated. - A value is trimmed of spaces and tabs, must be non-empty, and is at most 2000 characters. - A directive attaches to the next declaration header. Between them only blank lines, comments, attribute lines, set_option lines, and other directives may appear. Any other code makes the @@ -33,15 +40,17 @@ import unicodedata from collections.abc import Iterable from dataclasses import dataclass +from urllib.parse import urlsplit from lean4_explainer.extensions import Diagnostic -KEYS = ("title", "intuition", "step", "prereq", "see", "term") +KEYS = ("title", "intuition", "step", "prereq", "see", "term", "acronym", "source", "quote") PLACEHOLDER = "TODO_" MAX_VALUE = 2000 _BLANK = " \t" _DIRECTIVE_RE = re.compile(r"^(?P[A-Za-z]+):(?P.*)$") _NAME_RE = re.compile(r"^[^\s,:=()\[\]{}]+$") +_ACRONYM_RE = re.compile(r"^[A-Z][A-Z0-9-]+$") @dataclass(frozen=True) @@ -52,12 +61,25 @@ class L4Notes: prereqs: tuple[str, ...] = () see: tuple[str, ...] = () terms: tuple[tuple[str, str], ...] = () + acronyms: tuple[tuple[str, str], ...] = () + sources: tuple[tuple[str, str], ...] = () + quotes: tuple[tuple[str, str], ...] = () diagnostics: tuple[Diagnostic, ...] = () origin: str = "source" @property def is_empty(self) -> bool: - return not (self.title or self.intuition or self.steps or self.prereqs or self.see or self.terms) + return not ( + self.title + or self.intuition + or self.steps + or self.prereqs + or self.see + or self.terms + or self.acronyms + or self.sources + or self.quotes + ) def normalize_directive(text: str) -> str: @@ -71,6 +93,10 @@ def parse_l4del(directives: Iterable[tuple[int, str]]) -> L4Notes: prereqs: list[str] = [] see: list[str] = [] terms: list[tuple[str, str]] = [] + acronyms: list[tuple[str, str]] = [] + sources: list[tuple[str, str]] = [] + quotes: list[tuple[str, str]] = [] + quote_lines: list[int] = [] diagnostics: list[Diagnostic] = [] def fail(line: int, message: str) -> None: @@ -114,6 +140,41 @@ def fail(line: int, message: str) -> None: fail(line, f"term '{word}' given twice for one declaration") else: terms.append((word, definition)) + elif key == "acronym": + short, separator, expansion = value.partition("=") + short, expansion = short.strip(_BLANK), expansion.strip(_BLANK) + if not separator or not short or not expansion: + fail(line, "acronym needs the form 'SHORT = expansion'") + elif PLACEHOLDER not in short and not _ACRONYM_RE.fullmatch(short): + fail(line, "acronym name must start with A-Z and contain only uppercase letters, digits, or hyphens") + elif short in {existing for existing, _ in acronyms}: + fail(line, f"acronym '{short}' given twice for one declaration") + else: + acronyms.append((short, expansion)) + elif key == "source": + label, separator, url = value.partition("=") + label, url = label.strip(_BLANK), url.strip(_BLANK) + parsed = urlsplit(url) + if not separator or not label or not url: + fail(line, "source needs the form 'label = https://url'") + elif parsed.scheme != "https" or not parsed.netloc or parsed.username or parsed.password: + fail(line, "source URL must be an HTTPS URL without credentials") + elif label in {existing for existing, _ in sources}: + fail(line, f"source label repeated: {label}") + elif url in {existing for _, existing in sources}: + fail(line, f"source URL repeated: {url}") + else: + sources.append((label, url)) + elif key == "quote": + label, separator, excerpt = value.partition("=") + label, excerpt = label.strip(_BLANK), excerpt.strip(_BLANK) + if not separator or not label or not excerpt: + fail(line, "quote needs the form 'source label = exact excerpt'") + elif (label, excerpt) in quotes: + fail(line, f"quote from '{label}' repeated") + else: + quotes.append((label, excerpt)) + quote_lines.append(line) else: target = prereqs if key == "prereq" else see for name in (part.strip(_BLANK) for part in value.split(",")): @@ -123,6 +184,12 @@ def fail(line: int, message: str) -> None: fail(line, f"name '{name}' repeated in {key}") else: target.append(name) + source_labels = {label for label, _ in sources} + for (label, _), line in zip(quotes, quote_lines, strict=True): + if label != "Pinned Lean source" and label not in source_labels: + diagnostics.append( + Diagnostic("error", line, f"quote source label '{label}' has no matching source directive") + ) return L4Notes( title=title, intuition=intuition, @@ -130,5 +197,8 @@ def fail(line: int, message: str) -> None: prereqs=tuple(prereqs), see=tuple(see), terms=tuple(terms), + acronyms=tuple(acronyms), + sources=tuple(sources), + quotes=tuple(quotes), diagnostics=tuple(diagnostics), ) diff --git a/packages/l4del/src/lean4_explainer_l4del/graph.py b/packages/l4del/src/lean4_explainer_l4del/graph.py index d32bb9803e..18641c1b66 100644 --- a/packages/l4del/src/lean4_explainer_l4del/graph.py +++ b/packages/l4del/src/lean4_explainer_l4del/graph.py @@ -91,6 +91,22 @@ def build_glossary(notes: Sequence[Note]) -> tuple[dict[str, tuple[str, str, Loc return terms, issues +def build_acronyms(notes: Sequence[Note]) -> tuple[dict[str, tuple[str, str, Location]], list[str]]: + """One unambiguous expansion per acronym across a project.""" + found: dict[str, tuple[str, str, Location]] = {} + issues: list[str] = [] + for note in notes: + for short, expansion in note.acronyms: + kept = found.get(short) + if kept is not None and kept[0] != expansion: + issues.append( + f"error: {note.rel}:{note.line}: acronym '{short}' is already expanded as '{kept[0]}'; keeping the first" + ) + else: + found.setdefault(short, (expansion, note.name, (note.rel, note.line))) + return found, issues + + def merge_notes(notes: Sequence[Note], objects: Objects) -> tuple[list[Note], list[str]]: """One note per object. Identical copies may repeat an annotation; differing ones conflict.""" merged: dict[str, Note] = {} @@ -106,7 +122,7 @@ def merge_notes(notes: Sequence[Note], objects: Objects) -> tuple[list[Note], li def _content(note: Note) -> tuple[object, ...]: - return (note.title, note.prereqs, note.see, note.terms) + return (note.title, note.prereqs, note.see, note.terms, note.acronyms) def unresolved_links(notes: Sequence[Note], objects: Objects) -> list[str]: diff --git a/packages/l4del/src/lean4_explainer_l4del/model.py b/packages/l4del/src/lean4_explainer_l4del/model.py index a51a01f8d9..1ae3c8cdcd 100644 --- a/packages/l4del/src/lean4_explainer_l4del/model.py +++ b/packages/l4del/src/lean4_explainer_l4del/model.py @@ -14,6 +14,7 @@ class Note: prereqs: tuple[str, ...] see: tuple[str, ...] terms: tuple[tuple[str, str], ...] + acronyms: tuple[tuple[str, str], ...] = () @dataclass(frozen=True) diff --git a/packages/l4del/src/lean4_explainer_l4del/templates.py b/packages/l4del/src/lean4_explainer_l4del/templates.py index eef28ab96c..46b03687ec 100644 --- a/packages/l4del/src/lean4_explainer_l4del/templates.py +++ b/packages/l4del/src/lean4_explainer_l4del/templates.py @@ -51,6 +51,9 @@ def placeholder_block( f"-- L4DEL: intuition: {PLACEHOLDER}one_plain_sentence_why_it_holds", f"-- L4DEL: step: {PLACEHOLDER}first_proof_step", f"-- L4DEL: prereq: {prereq}", + f"-- L4DEL: source: {PLACEHOLDER}source_label = https://example.org/{PLACEHOLDER}stable_source", + f"-- L4DEL: quote: {PLACEHOLDER}source_label = {PLACEHOLDER}exact_source_excerpt", + f"-- L4DEL: acronym: {PLACEHOLDER}SHORT = {PLACEHOLDER}full_expansion", ] ) diff --git a/packages/l4del/tests/test_features.py b/packages/l4del/tests/test_features.py index 48430378a1..e670b3d72d 100644 --- a/packages/l4del/tests/test_features.py +++ b/packages/l4del/tests/test_features.py @@ -7,9 +7,10 @@ from lean4_explainer_l4del.graph import build_glossary, build_learning_path, unresolved_links from lean4_explainer.objects import plain_objects, resolve from lean4_explainer_l4del.grammar import parse_l4del +from lean4_explainer_l4del.extension import L4delExtension from lean4_explainer.render import file_page from lean4_explainer.scan import parse_source -from lean4_explainer.search import shard_key, write_search +from lean4_explainer.search import search_keys, shard_key, write_search def _note(name, rel, line, title=None, prereqs=(), terms=()): @@ -44,6 +45,30 @@ def test_l4del_structured_keys(): assert notes.diagnostics == () +def test_an_annotated_file_gets_full_share_metadata(make_context): + extension = L4delExtension() + ctx = make_context(site_url="https://example.org/", extensions=((extension, None),)) + annotated = parse_source("-- L4DEL: title: Fact\ntheorem fact : True := trivial\n", "A.lean") + bare = parse_source("theorem fact : True := trivial\n", "B.lean") + + assert '= {"ab", "he", "op"} + assert name in written["_assets/search/s_he.js"] + assert entries == 1 + + +def test_learning_path_can_be_filtered(tmp_path): + lean = tmp_path / "lean" + _tree( + lean, + {"A.lean": "-- L4DEL: title: First idea\ntheorem A.first : True := trivial\n"}, + ) + out = tmp_path / "docs" + build_site(lean, out) + + html = (out / "learning-path.html").read_text(encoding="utf-8") + assert 'aria-label="Filter learning path"' in html + assert '
          ' in html + + def test_learning_path_puts_prerequisites_first(): locations = {"A.basic": ("a.lean", 1), "A.next": ("a.lean", 5)} notes = [ diff --git a/packages/l4del/tests/test_l4del_spec.py b/packages/l4del/tests/test_l4del_spec.py index 635a3479a5..2778d074b7 100644 --- a/packages/l4del/tests/test_l4del_spec.py +++ b/packages/l4del/tests/test_l4del_spec.py @@ -27,6 +27,7 @@ def test_clean_annotation_has_no_issues(): "-- L4DEL: intuition: Two items share a box.\n" "-- L4DEL: step: Count the boxes.\n" "-- L4DEL: term: box = a container\n" + "-- L4DEL: source: Pinned proof = https://example.org/proof/abc#L1\n" "theorem t : True := trivial\n" ) assert issues(text) == [] @@ -59,6 +60,57 @@ def test_repeated_name_is_error(): ] +def test_sources_are_structured_repeatable_https_links(): + text = ( + "-- L4DEL: source: Formal statement = https://example.org/repo/blob/abc/A.lean#L2\n" + "-- L4DEL: source: Paper = https://doi.org/10.1000/example\n" + "theorem t : True := trivial\n" + ) + notes = parse_source(text, "a.lean").declarations[0].ext["l4del"] + assert notes.sources == ( + ("Formal statement", "https://example.org/repo/blob/abc/A.lean#L2"), + ("Paper", "https://doi.org/10.1000/example"), + ) + assert issues(text) == [] + + +def test_source_rejects_mutable_or_malformed_links_and_duplicates(): + assert issues("-- L4DEL: source: Paper = http://example.org/paper\ntheorem t : True := trivial\n") == [ + "error: line 1: source URL must be an HTTPS URL without credentials" + ] + assert issues("-- L4DEL: source: https://example.org/paper\ntheorem t : True := trivial\n") == [ + "error: line 1: source needs the form 'label = https://url'" + ] + repeated = ( + "-- L4DEL: source: One = https://example.org/paper\n" + "-- L4DEL: source: Two = https://example.org/paper\n" + "theorem t : True := trivial\n" + ) + assert issues(repeated) == ["error: line 2: source URL repeated: https://example.org/paper"] + + +def test_acronym_and_linked_quote_are_structured(): + text = ( + "-- L4DEL: acronym: DEL = Domain Explanation Language\n" + "-- L4DEL: source: Original paper = https://example.org/paper\n" + "-- L4DEL: quote: Original paper = The exact source words.\n" + "theorem t : True := trivial\n" + ) + notes = parse_source(text, "a.lean").declarations[0].ext["l4del"] + assert notes.acronyms == (("DEL", "Domain Explanation Language"),) + assert notes.quotes == (("Original paper", "The exact source words."),) + assert issues(text) == [] + + +def test_quote_must_name_a_source_and_acronym_names_are_explicit(): + assert issues("-- L4DEL: quote: Missing = Words\ntheorem t : True := trivial\n") == [ + "error: line 1: quote source label 'Missing' has no matching source directive" + ] + assert issues("-- L4DEL: acronym: Np = nondeterministic polynomial time\ntheorem t : True := trivial\n") == [ + "error: line 1: acronym name must start with A-Z and contain only uppercase letters, digits, or hyphens" + ] + + def test_space_before_directive_is_required(): assert issues("-- L4DEL:title: X\ntheorem t : True := trivial\n") == [ "error: line 1: L4DEL: needs a space before the directive" @@ -118,7 +170,7 @@ def test_unannotated_declaration_state_and_valid_template(): assert annotation_state(decl) == "unannotated" block = placeholder_block(decl, {}) parsed = parse_source(block + "\ntheorem t : True := trivial\n", "a.lean").declarations[0] - assert [d.severity for d in notes_of(parsed).diagnostics] == ["warning"] * 4 + assert [d.severity for d in notes_of(parsed).diagnostics] == ["warning"] * 7 assert all("placeholder" in d.message for d in notes_of(parsed).diagnostics) diff --git a/packages/l4del/tests/test_overlay.py b/packages/l4del/tests/test_overlay.py index 745c7a43a4..df6b4bfdb8 100644 --- a/packages/l4del/tests/test_overlay.py +++ b/packages/l4del/tests/test_overlay.py @@ -27,6 +27,7 @@ @decl Demo.first -- L4DEL: title: First, explained -- L4DEL: intuition: Trivial things are true. +-- L4DEL: source: Logic reference = https://example.org/logic @decl Demo.second -- L4DEL: step: Apply trivial. @decl Demo.inline @@ -78,10 +79,46 @@ def test_overlay_annotations_reach_the_page_and_the_source_is_untouched(tmp_path page = (out / "Demo.lean.html").read_text(encoding="utf-8") assert "First, explained" in page and "Trivial things are true." in page + assert 'Sources and attribution:' in page and 'href="https://example.org/logic"' in page assert "Apply trivial." in page assert (root / "Demo.lean").read_text(encoding="utf-8") == SOURCE # the sidecar never writes upstream +def test_linked_quote_renders_as_a_citation(tmp_path): + overlay = """@file Demo.lean +@decl Demo.first +-- L4DEL: source: Original note = https://example.org/note +-- L4DEL: quote: Original note = Exact words from the note. +""" + _, out, _ = _site(tmp_path, overlay) + rendered = (out / "Demo.lean.html").read_text(encoding="utf-8") + assert '
          ' in rendered + assert '>Original note' in rendered + + +def test_overlay_adds_the_configured_pinned_source_beside_the_explanation(tmp_path): + root = tmp_path / "src" + root.mkdir() + (root / "Demo.lean").write_text(SOURCE, encoding="utf-8") + overlay = tmp_path / "demo.l4del" + overlay.write_text(OVERLAY, encoding="utf-8") + config = Config( + source_url="https://github.com/example/repo/blob/{ref}/{path}#L{line}", + source_ref="0123456789abcdef", + options=( + ("overlay", str(overlay)), + ("overlay_sources", '[["Pinned project documentation","https://example.org/docs/abc"]]'), + ), + ) + + build_site(root, tmp_path / "out", config, tmp_path / "idx") + + page = (tmp_path / "out" / "Demo.lean.html").read_text(encoding="utf-8") + assert "Pinned Lean source (0123456789ab)" in page + assert "https://github.com/example/repo/blob/0123456789abcdef/Demo.lean#L4" in page + assert "Pinned project documentation" in page and "https://example.org/docs/abc" in page + + def test_unreviewed_overlay_discloses_its_provenance_beside_the_annotation(tmp_path): root = tmp_path / "src" root.mkdir() diff --git a/packages/lean/src/lean4_explainer_lean/extension.py b/packages/lean/src/lean4_explainer_lean/extension.py index 067da9f1a7..b0c879fdc6 100644 --- a/packages/lean/src/lean4_explainer_lean/extension.py +++ b/packages/lean/src/lean4_explainer_lean/extension.py @@ -271,7 +271,7 @@ def _trust_page(ctx, analysis: Analysis) -> str: body = ["

          Trust

          "] if not analysis.toolchain: body.append('

          Lean was not found on the PATH, so no declaration was checked. All trust is UNKNOWN.

          ') - return page("Trust", 0, body, ctx) + return page("Trust", 0, body, ctx, canonical_path="trust.html") body.append( f'

          Axioms come from the Lean kernel ({escape(analysis.toolchain)}): the constants each declaration ' "depends on, as Lean's collectAxioms reports them. Standard axioms are propext, Classical.choice and Quot.sound.

          " @@ -309,4 +309,4 @@ def _trust_page(ctx, analysis: Analysis) -> str: if len(rows) > _TRUST_ROWS: body.append(f'
        1. … and {len(rows) - _TRUST_ROWS} more
          2. ') body.append("
        ") - return page("Trust", 0, body, ctx) + return page("Trust", 0, body, ctx, canonical_path="trust.html") diff --git a/packages/map/src/lean4_explainer_map/extension.py b/packages/map/src/lean4_explainer_map/extension.py index fbb1f7a19b..4ff8903c21 100644 --- a/packages/map/src/lean4_explainer_map/extension.py +++ b/packages/map/src/lean4_explainer_map/extension.py @@ -20,7 +20,7 @@ from typing import Any from lean4_explainer.extensions import Extension, ParseResult, SourceView -from lean4_explainer.render import Context, href, page +from lean4_explainer.render import Context, filter_box, href, page from .deps import Resolver, bound_in, declaration_end, imports_in, names_in, opens_in, reverse, variables_in, reachable, visible_files @@ -52,6 +52,11 @@ #project-map .depmap-wrap { width: calc(100vw - 2rem); position: relative; left: 50%; transform: translateX(-50%); } #project-map .controls { display: flex; flex-wrap: wrap; gap: 0.6rem; align-items: center; margin: 0.5rem 0; } #project-map input[type="search"] { min-width: 18rem; } +.map-table-wrap { overflow-x: auto; } +.map-table { width: 100%; border-collapse: collapse; font-size: 0.9rem; } +.map-table th, .map-table td { padding: 0.35rem 0.5rem; border-bottom: 1px solid var(--line); text-align: left; } +.map-table th:not(:first-child), .map-table td:not(:first-child) { text-align: right; white-space: nowrap; } +.depmap-text { font-size: 0.88rem; } """ @@ -282,8 +287,18 @@ def file(rel: str) -> int: a = file(ctx.locations[target][0]) if a != b: weights[(a, b)] = weights.get((a, b), 0) + 1 + builds_on: dict[int, set[int]] = {index: set() for index in range(len(order))} + used_by: dict[int, set[int]] = {index: set() for index in range(len(order))} + for a, b in weights: + builds_on[b].add(a) + used_by[a].add(b) data = {"f": order, "e": [[a, b, w] for (a, b), w in sorted(weights.items())]} payload = json.dumps(data, ensure_ascii=False, separators=(",", ":")).replace("<", "\\u003c") + rows = "".join( + f'{item[0]}{item[2]}' + f'{len(builds_on[index])}{len(used_by[index])}' + for index, item in enumerate(order) + ) body = [ "

        Map

        ", '

        How this project builds on itself. An arrow goes from a file to a file that uses something ' @@ -291,8 +306,16 @@ def file(rel: str) -> int: "every declaration's own map, on its file page, shows the same thing one result at a time.

        ", '
        ', f'', + '

        Files as a table

        ', + '

        The same map data in a searchable keyboard- and screen-reader-friendly form.

        ', + filter_box("Filter map files"), + '
        ' + '' + '' + + rows + + "
        Files and cross-file dependency counts
        FileDeclarationsBuilds onUsed by
        ", ] if not data["e"]: body.insert(2, '

        No file uses another yet, so there is nothing to connect.

        ') - return page("Map", 0, body, ctx) + return page("Map", 0, body, ctx, canonical_path="map.html") diff --git a/packages/map/src/lean4_explainer_map/map.js b/packages/map/src/lean4_explainer_map/map.js index ea471118f1..8c5fd949eb 100644 --- a/packages/map/src/lean4_explainer_map/map.js +++ b/packages/map/src/lean4_explainer_map/map.js @@ -333,6 +333,17 @@ (left.length ? " Drawn: " + left.join(", and ") + "." : "") + " Boxes are links; point at one to light up its arrows."; box.appendChild(legend); + const text = document.createElement("details"); + text.className = "depmap-text"; + const rows = items.map((item, index) => { + let relation = index === local.get(here) ? "current declaration" : "two steps away"; + if (edges.some((edge) => edge[0] === index && edge[1] === local.get(here))) relation = "builds on"; + if (edges.some((edge) => edge[0] === local.get(here) && edge[1] === index)) relation = "used by"; + const label = esc(item.name) + " — " + relation; + return "
      7. " + (item.href && !item.here ? '' + label + "" : label) + "
        8. "; + }).join(""); + text.innerHTML = "Text version of this map
          " + rows + "
        "; + box.appendChild(text); wire(wrap); }); li.appendChild(box); diff --git a/packages/map/tests/test_map.py b/packages/map/tests/test_map.py index 448d1b03b3..8fa4997ed3 100644 --- a/packages/map/tests/test_map.py +++ b/packages/map/tests/test_map.py @@ -271,6 +271,10 @@ def test_the_project_map_links_files_and_is_in_the_navigation(tmp_path): a, b = files["Demo/Base.lean"][0], files["Demo/More.lean"][0] assert data["e"] == [[a, b, 2]] # middle uses base, top uses base_pos: two uses, all one way assert '
        ' in page and 'src="_assets/map.js"' in page + assert 'Files and cross-file dependency counts' in page + assert 'aria-label="Filter map files"' in page + assert '>Demo/Base.lean201' in page + assert "Text version of this map" in MAP_JS assert 'href="../map.html">Map' in (out / "Demo" / "Base.lean.html").read_text(encoding="utf-8") assert (out / "_assets" / "map.js").read_text(encoding="utf-8") == MAP_JS diff --git a/packages/reader/src/lean4_explainer_reader/extension.py b/packages/reader/src/lean4_explainer_reader/extension.py index 3468e657d2..fd3cf2dd5f 100644 --- a/packages/reader/src/lean4_explainer_reader/extension.py +++ b/packages/reader/src/lean4_explainer_reader/extension.py @@ -47,6 +47,8 @@ CSS = """ #reader-note { font-size: 0.9rem; color: var(--muted); border-left: 3px solid var(--line); padding: 0.2rem 0.6rem; margin: 0.6rem 0; } #reader-note .reader-status:empty { display: none; } +#reader-note .reader-controls { display: inline-flex; gap: 0.35rem; margin-left: 0.45rem; } +#reader-note button { font: inherit; color: inherit; background: transparent; border: 1px solid var(--line); border-radius: 4px; cursor: pointer; } details.reading { margin: 0.45rem 0 0.2rem; } details.reading > summary { cursor: pointer; font-size: 0.9rem; color: var(--muted); } details.reading[open] > summary { margin-bottom: 0.3rem; } diff --git a/packages/reader/src/lean4_explainer_reader/reader.js b/packages/reader/src/lean4_explainer_reader/reader.js index 41332f1ea2..143e142c6d 100644 --- a/packages/reader/src/lean4_explainer_reader/reader.js +++ b/packages/reader/src/lean4_explainer_reader/reader.js @@ -1386,6 +1386,20 @@ const trace = li.querySelector("details.trace"); if (trace && !eager) trace.addEventListener("toggle", fill); }); + if (document.querySelector("details.reading")) { + const controls = document.createElement("span"); + controls.className = "reader-controls"; + [["Expand all readings", true], ["Collapse all readings", false]].forEach(([label, open]) => { + const button = document.createElement("button"); + button.type = "button"; + button.textContent = label; + button.addEventListener("click", () => { + document.querySelectorAll("details.reading").forEach((reading) => { reading.open = open; }); + }); + controls.appendChild(button); + }); + note.appendChild(controls); + } status(eager ? "" : "Open any “Reading” to see it."); }).catch((e) => status("Could not load the source (" + e.message + "). The source links still work.")); } diff --git a/packages/reader/tests/test_reader.py b/packages/reader/tests/test_reader.py index e25b7246fe..8f09f16e4c 100644 --- a/packages/reader/tests/test_reader.py +++ b/packages/reader/tests/test_reader.py @@ -103,6 +103,13 @@ def test_a_page_carries_its_source_and_loads_the_reader(tmp_path): assert "Lean was not run" in READER_JS # the note is written by the script, so pages stay small +def test_readings_have_page_level_expand_and_collapse_controls(): + assert 'reader-controls' in READER_JS + assert 'Expand all readings' in READER_JS + assert 'Collapse all readings' in READER_JS + assert 'document.querySelectorAll("details.reading")' in READER_JS + + def test_source_that_contains_a_closing_script_tag_cannot_end_the_block(tmp_path): text = DEMO.replace("/-- A doc comment. -/", '/-- see "" -/') page, _ = _build(tmp_path, text) diff --git a/pyproject.toml b/pyproject.toml index 4031cc1e00..85c5385a7c 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -24,7 +24,7 @@ test = ["pytest>=8"] lean = ["lean4-explainer-lean>=0.2.0"] ecosystem = ["lean4-explainer-ecosystem>=0.1.0"] # 0.2.0 leaves the drawing to the map extension, so the two never draw two maps -l4del = ["lean4-explainer-l4del>=0.3.0"] +l4del = ["lean4-explainer-l4del>=0.5.0"] reader = ["lean4-explainer-reader>=0.2.0"] map = ["lean4-explainer-map>=0.2.0"] # 0.2.0 reads bridge files and recorded checks, and shows the discovery catalogue @@ -38,7 +38,7 @@ compfiles = ["lean4-explainer-compfiles>=0.1.0"] tutorials = ["lean4-explainer-mil>=0.1.0", "lean4-explainer-tpil>=0.1.0"] oai = ["lean4-explainer-oai>=0.4.0"] all = [ - "lean4-explainer-l4del>=0.3.0", + "lean4-explainer-l4del>=0.5.0", "lean4-explainer-reader>=0.2.0", "lean4-explainer-map>=0.2.0", "lean4-explainer-implications>=0.2.0", diff --git a/scripts/audit_hosted_overlay_grounding.py b/scripts/audit_hosted_overlay_grounding.py new file mode 100644 index 0000000000..ecddae0992 --- /dev/null +++ b/scripts/audit_hosted_overlay_grounding.py @@ -0,0 +1,252 @@ +"""Verify hosted explanations against the exact pinned source checkouts. + +Generated annotations must reproduce source-controlled doc comments, leading +comments, or openai/math formalization notes. Curated annotations are checked +for an exact declaration target and durable reference links, but deliberately +remain unreviewed: this tool is not a mathematical peer reviewer. +""" + +from __future__ import annotations + +import argparse +import hashlib +import json +import re +import subprocess +from pathlib import Path +from urllib.parse import quote, urlsplit + +from lean4_explainer.scan import Declaration, parse_source +from lean4_explainer_l4del.grammar import normalize_directive, parse_l4del +from lean4_explainer_l4del.overlay import parse_overlay + +try: # direct script execution puts scripts/ on sys.path; test imports put the repository root there + from generate_documented_hosted_overlay import _bounded, _title + from generate_oai_hosted_overlay import _bounded_scope, _note +except ModuleNotFoundError: # pragma: no cover - the other branch is covered by the Pages command + from scripts.generate_documented_hosted_overlay import _bounded, _title + from scripts.generate_oai_hosted_overlay import _bounded_scope, _note + + +def _head(path: Path) -> str: + done = subprocess.run( + ["git", "rev-parse", "HEAD"], cwd=path, capture_output=True, text=True, encoding="utf-8", timeout=30 + ) + return done.stdout.strip() if done.returncode == 0 else "" + + +def _source_path(checkout: Path, rel: str) -> Path: + direct = checkout / rel + if direct.is_file(): + return direct + nested = checkout / "lean" / rel + return nested + + +def _stable_reference(url: str) -> bool: + parsed = urlsplit(url) + host = (parsed.hostname or "").lower() + parts = parsed.path.strip("/").split("/") + if host == "github.com" and len(parts) >= 5 and parts[2] in {"blob", "tree"}: + return bool(re.fullmatch(r"[0-9a-f]{40}", parts[3])) + if host == "arxiv.org": + return bool(re.fullmatch(r"/abs/\d{4}\.\d{4,5}v\d+", parsed.path)) + if host == "doi.org": + return bool(parsed.path.strip("/")) + if host == "web.archive.org": + return bool(re.match(r"^/web/\d{14}/", parsed.path)) + return False + + +def _oai_note_targets(checkout: Path) -> dict[tuple[str, str], set[str]]: + found: dict[tuple[str, str], set[str]] = {} + docs = checkout / "lean" / "docs" + configs = checkout / "lean" / "ComparatorChallenges" + if not docs.is_dir() or not configs.is_dir(): + return found + for path in sorted(docs.glob("*.md")): + note = _note(path) + if note is None: + continue + for stem in note.comparators: + config_path = configs / f"{stem}.json" + if not config_path.is_file(): + continue + config = json.loads(config_path.read_text(encoding="utf-8")) + for name in config.get("theorem_names", []) + config.get("definition_names", []): + if isinstance(name, str): + found.setdefault((f"ComparatorChallenges/{stem}.lean", name), set()).add(note.scope) + return found + + +def _generated_line(text: str) -> int: + for number, line in enumerate(text.splitlines(), start=1): + if line.startswith("# BEGIN GENERATED"): + return number + return len(text.splitlines()) + 1 + + +def audit(manifest_path: Path, work_dir: Path) -> tuple[dict, list[str]]: + document = json.loads(manifest_path.read_text(encoding="utf-8")) + entries = document.get("overlays", {}) + errors: list[str] = [] + report: dict = { + "schema": 1, + "manifest_sha256": hashlib.sha256(manifest_path.read_bytes()).hexdigest(), + "status": "PASS", + "corpora": {}, + "curated_entries": [], + "limitations": ( + "Generated wording is checked against pinned source-controlled text. Curated wording is source-linked " + "and target-checked but remains AI-generated-unreviewed until an identified human reviewer signs it off." + ), + } + for corpus_name, entry in sorted(entries.items()): + where = f"{corpus_name}" + checkout = work_dir / corpus_name + expected_commit = entry.get("commit", "") + actual_commit = _head(checkout) if checkout.is_dir() else "" + if actual_commit != expected_commit: + errors.append(f"{where}: checkout HEAD {actual_commit or 'missing'} != {expected_commit}") + continue + overlay_path = manifest_path.parent / entry.get("file", "") + text = overlay_path.read_text(encoding="utf-8") + if hashlib.sha256(overlay_path.read_bytes()).hexdigest() != entry.get("sha256"): + errors.append(f"{where}: overlay SHA-256 does not match manifest") + continue + shared = entry.get("sources", []) + if not isinstance(shared, list) or len(shared) < 2: + errors.append(f"{where}: fewer than two corpus-level reference links") + for source in shared if isinstance(shared, list) else (): + url = source.get("url") if isinstance(source, dict) else None + parsed = urlsplit(url) if isinstance(url, str) else None + if not parsed or parsed.scheme != "https" or not parsed.netloc: + errors.append(f"{where}: invalid corpus reference URL {url!r}") + elif not _stable_reference(url): + errors.append(f"{where}: corpus reference URL is not immutable {url!r}") + + overlay = parse_overlay(text, str(overlay_path)) + marker = _generated_line(text) + declarations: dict[tuple[str, str], Declaration] = {} + source_git_paths: dict[str, str] = {} + by_digest: dict[tuple[str, int], set[str]] = {} + for rel, targets in overlay.files.items(): + path = _source_path(checkout, rel) + if not path.is_file(): + errors.append(f"{where}:{rel}: source file is missing") + continue + source_git_paths[rel] = path.relative_to(checkout).as_posix() + extra = ("problem", "determine") if corpus_name == "compfiles" else () + source = path.read_bytes().decode("utf-8-sig", errors="replace").replace("\r\n", "\n") + for declaration in parse_source(source, rel, extra_kinds=extra, statements=True).declarations: + declarations.setdefault((rel, declaration.name), declaration) + description = declaration.doc or declaration.comment + if description: + value = _bounded_scope(description) if corpus_name == "oai" else _bounded(description) + value = normalize_directive(value) + by_digest.setdefault((declaration.name, declaration.code_digest), set()).add(value) + + note_targets = _oai_note_targets(checkout) if corpus_name == "oai" else {} + for target, scopes in note_targets.items(): + declaration = declarations.get(target) + if declaration is not None: + by_digest.setdefault((declaration.name, declaration.code_digest), set()).update(scopes) + + total = curated = generated = matched = 0 + for rel, targets in overlay.files.items(): + for name, directives in targets.items(): + total += 1 + declaration = declarations.get((rel, name)) + if declaration is None: + errors.append(f"{where}:{rel}:{name}: declaration target is missing") + continue + notes = parse_l4del(directives) + for diagnostic in notes.diagnostics: + if diagnostic.severity == "error": + errors.append(f"{where}:{rel}:{name}:{diagnostic.line}: {diagnostic.message}") + if not notes.title or not notes.intuition: + errors.append(f"{where}:{rel}:{name}: annotation needs both title and intuition") + first_line = min((line for line, _ in directives), default=0) + if first_line < marker: + curated += 1 + source_path = quote(source_git_paths[rel], safe="/") + report["curated_entries"].append( + { + "corpus": corpus_name, + "file": rel, + "declaration": name, + "line": declaration.line, + "title": notes.title, + "intuition": notes.intuition, + "source_statement": declaration.statement, + "source_statement_sha256": hashlib.sha256( + declaration.statement.encode("utf-8") + ).hexdigest(), + "review_state": "source-linked-unreviewed", + "exact_source_url": ( + f"https://github.com/{entry.get('repo')}/blob/{expected_commit}/" + f"{source_path}#L{declaration.line}" + ), + "corpus_references": shared, + } + ) + continue + generated += 1 + candidates = by_digest.get((name, declaration.code_digest), set()) + if notes.intuition not in candidates: + errors.append(f"{where}:{rel}:{name}: generated intuition no longer matches its pinned source text") + continue + if corpus_name != "oai": + description = declaration.doc or declaration.comment or "" + if notes.title != normalize_directive(_title(name, description)): + errors.append(f"{where}:{rel}:{name}: generated title no longer matches its pinned source text") + continue + matched += 1 + report["corpora"][corpus_name] = { + "repo": entry.get("repo"), + "commit": expected_commit, + "overlay_sha256": entry.get("sha256"), + "annotations": total, + "generated_source_matched": matched, + "generated": generated, + "curated_source_linked_unreviewed": curated, + "shared_reference_links": len(shared) if isinstance(shared, list) else 0, + } + if errors: + report["status"] = "FAIL" + report["errors"] = errors + report["totals"] = { + "annotations": sum(row["annotations"] for row in report["corpora"].values()), + "generated_source_matched": sum(row["generated_source_matched"] for row in report["corpora"].values()), + "curated_source_linked_unreviewed": sum( + row["curated_source_linked_unreviewed"] for row in report["corpora"].values() + ), + } + return report, errors + + +def main() -> int: + parser = argparse.ArgumentParser() + parser.add_argument("--manifest", required=True, type=Path) + parser.add_argument("--work", required=True, type=Path) + parser.add_argument("--report", type=Path) + args = parser.parse_args() + report, errors = audit(args.manifest, args.work) + if args.report: + args.report.parent.mkdir(parents=True, exist_ok=True) + args.report.write_text(json.dumps(report, indent=2, ensure_ascii=False) + "\n", encoding="utf-8") + for error in errors[:50]: + print(f"error: {error}") + if len(errors) > 50: + print(f"error: {len(errors) - 50} more") + totals = report["totals"] + print( + f"hosted overlay grounding {report['status']}: {totals['annotations']} annotations; " + f"{totals['generated_source_matched']} generated source matches; " + f"{totals['curated_source_linked_unreviewed']} curated source-linked and still unreviewed" + ) + return 1 if errors else 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/scripts/check_static_site.py b/scripts/check_static_site.py new file mode 100644 index 0000000000..0da28b6103 --- /dev/null +++ b/scripts/check_static_site.py @@ -0,0 +1,234 @@ +"""Fail closed on the public proofsite's small but consequential release contract. + +This is deliberately a smoke gate rather than an exhaustive crawler: it checks +the landing page, recovery/discovery files, every corpus home and the feature +pages that exist. It never requests external URLs. +""" + +from __future__ import annotations + +import argparse +import json +import re +from html.parser import HTMLParser +from pathlib import Path, PurePosixPath +from urllib.parse import quote, unquote, urljoin, urlsplit +from xml.etree import ElementTree + + +class Document(HTMLParser): + def __init__(self) -> None: + super().__init__(convert_charrefs=True) + self.hrefs: list[str] = [] + self.meta: dict[tuple[str, str], str] = {} + self.ids: set[str] = set() + self.classes: set[str] = set() + self.text: list[str] = [] + + def handle_starttag(self, tag: str, attrs: list[tuple[str, str | None]]) -> None: + values = dict(attrs) + if values.get("id"): + self.ids.add(values["id"] or "") + self.classes.update((values.get("class") or "").split()) + if tag == "a" and values.get("href"): + self.hrefs.append(values["href"] or "") + if tag == "link" and values.get("rel") and values.get("href"): + self.meta[("link", values["rel"] or "")] = values["href"] or "" + if tag == "meta": + key = values.get("name") or values.get("property") + if key and values.get("content"): + self.meta[("meta", key)] = values["content"] or "" + + def handle_data(self, data: str) -> None: + if data.strip(): + self.text.append(data.strip()) + + +def _document(path: Path) -> Document: + doc = Document() + doc.feed(path.read_text(encoding="utf-8")) + return doc + + +def _local_target(site: Path, page: Path, href: str, base_path: str) -> Path | None: + parsed = urlsplit(href) + if parsed.scheme or parsed.netloc or href.startswith(("mailto:", "javascript:")): + return None + raw = unquote(parsed.path) + if not raw: + return None + directory = raw.endswith("/") + if raw.startswith("/"): + if base_path and raw.startswith(base_path): + raw = raw[len(base_path) :] + else: + return None + target = site / raw + else: + target = page.parent / raw + if directory: + target /= "index.html" + try: + target.resolve().relative_to(site.resolve()) + except ValueError: + return Path("__outside_site__") + return target + + +def _sample_pages(site: Path) -> list[Path]: + pages = [site / "index.html", site / "404.html"] + for corpus in sorted(path for path in site.iterdir() if path.is_dir() and (path / "index.html").is_file()): + pages.append(corpus / "index.html") + for name in ("search.html", "glossary.html", "learning-path.html", "map.html", "annotate.html"): + if (corpus / name).is_file(): + pages.append(corpus / name) + featured = site / "flt" / "FLT" / "Proof.lean.html" + if featured.is_file(): + pages.append(featured) + return list(dict.fromkeys(pages)) + + +def check_site(site: Path, site_url: str) -> list[str]: + errors: list[str] = [] + site = site.resolve() + parsed_url = urlsplit(site_url) + if parsed_url.scheme != "https" or not parsed_url.netloc or parsed_url.query or parsed_url.fragment: + return ["site URL must be HTTPS without a query or fragment"] + site_url = site_url.rstrip("/") + "/" + base_path = parsed_url.path.rstrip("/") + "/" + required = ("index.html", "404.html", "robots.txt", "sitemap.xml", "_assets/favicon.svg") + for rel in required: + if not (site / rel).is_file(): + errors.append(f"missing {rel}") + if errors: + return errors + + samples = _sample_pages(site) + for page in samples: + rel = page.relative_to(site).as_posix() + doc = _document(page) + if rel != "404.html": + required_meta = [("meta", "description")] + if not rel.endswith(".lean.html"): + required_meta.extend((("meta", "og:title"), ("meta", "og:description"), ("meta", "twitter:card"))) + for key in required_meta: + if not doc.meta.get(key): + errors.append(f"{rel}: missing {key[1]}") + if "skip-link" not in doc.classes or "content" not in doc.ids: + errors.append(f"{rel}: missing skip navigation or #content") + if not doc.meta.get(("link", "canonical")): + errors.append(f"{rel}: missing canonical link") + for href in doc.hrefs: + target = _local_target(site, page, href, base_path) + if target is not None and not target.is_file(): + errors.append(f"{rel}: broken local link {href}") + + landing = _document(site / "index.html") + landing_text = " ".join(landing.text) + if "Start exploring" not in landing_text or "All corpora" not in landing_text: + errors.append("index.html: missing reader onboarding") + if "Lean4 Domain Explanation Language (L4DEL)" not in landing_text: + errors.append("index.html: explanation language is not introduced by its full name") + if "Report a site issue" not in landing_text: + errors.append("index.html: missing feedback route") + if landing.meta.get(("link", "canonical")) != site_url: + errors.append("index.html: canonical URL does not match --site-url") + if "annotation-audit.json" in landing.hrefs: + audit_path = site / "annotation-audit.json" + if not audit_path.is_file(): + errors.append("index.html: linked annotation audit is missing") + else: + try: + audit = json.loads(audit_path.read_text(encoding="utf-8")) + curated = audit.get("curated_entries", []) + expected_curated = audit.get("totals", {}).get("curated_source_linked_unreviewed") + if audit.get("status") != "PASS": + errors.append("annotation-audit.json: status is not PASS") + if expected_curated != len(curated): + errors.append("annotation-audit.json: curated entry count is inconsistent") + if any( + item.get("review_state") != "source-linked-unreviewed" + or not re.match(r"https://github\.com/.+/blob/[0-9a-f]{40}/", item.get("exact_source_url", "")) + or not item.get("source_statement_sha256") + for item in curated + ): + errors.append("annotation-audit.json: a curated entry lacks fail-closed source evidence") + except (json.JSONDecodeError, OSError) as exc: + errors.append(f"annotation-audit.json: cannot parse: {exc}") + + not_found = " ".join(_document(site / "404.html").text) + if "Return to all corpora" not in not_found: + errors.append("404.html: missing recovery link") + + featured = site / "flt" / "FLT" / "Proof.lean.html" + if featured.is_file(): + text = featured.read_text(encoding="utf-8") + featured_doc = _document(featured) + if not featured_doc.meta.get(("meta", "og:title")) or not featured_doc.meta.get(("meta", "twitter:card")): + errors.append("flt/FLT/Proof.lean.html: featured annotation lacks full share metadata") + if "Sources and attribution:" not in text or not re.search(r"github\.com/[^/]+/[^/]+/blob/[0-9a-f]{40}/", text): + errors.append("flt/FLT/Proof.lean.html: hosted annotation lacks an exact pinned grounding link") + featured_text = " ".join(featured_doc.text) + if "Explanation legend" not in featured_text or "Lean4 Domain Explanation Language" not in featured_text: + errors.append("flt/FLT/Proof.lean.html: annotation lacks its page-top explanation legend") + if "Credit:" not in featured_text or "Project sources:" not in featured_text: + errors.append("flt/FLT/Proof.lean.html: annotation lacks author credit or project sources") + + sitemap_files: set[str] = set() + try: + index = ElementTree.parse(site / "sitemap.xml").getroot() + for node in index.findall("{*}sitemap/{*}loc"): + name = PurePosixPath(urlsplit(node.text or "").path).name + if name: + sitemap_files.add(name) + except (ElementTree.ParseError, OSError) as exc: + errors.append(f"sitemap.xml: cannot parse: {exc}") + listed: set[str] = set() + for name in sitemap_files: + path = site / name + if not path.is_file(): + errors.append(f"sitemap.xml: missing referenced {name}") + continue + try: + root = ElementTree.parse(path).getroot() + for node in root.findall("{*}url/{*}loc"): + url = node.text or "" + if url.startswith(site_url): + listed.add(unquote(url[len(site_url) :])) + except ElementTree.ParseError as exc: + errors.append(f"{name}: cannot parse: {exc}") + expected = { + path.relative_to(site).as_posix() + for path in site.rglob("*.html") + if path.name != "404.html" + } + missing = expected - listed + extra = listed - expected + if missing: + errors.append(f"sitemaps omit {len(missing)} HTML page(s), first: {sorted(missing)[0]}") + if extra: + errors.append(f"sitemaps list {len(extra)} missing page(s), first: {sorted(extra)[0]}") + + robots = (site / "robots.txt").read_text(encoding="utf-8") + if f"Sitemap: {urljoin(site_url, 'sitemap.xml')}" not in robots: + errors.append("robots.txt: sitemap URL does not match --site-url") + return errors + + +def main() -> int: + parser = argparse.ArgumentParser() + parser.add_argument("--site", required=True, type=Path) + parser.add_argument("--site-url", required=True) + args = parser.parse_args() + errors = check_site(args.site, args.site_url) + for error in errors: + print(f"error: {error}") + if errors: + return 1 + pages = sum(1 for _ in args.site.rglob("*.html")) + print(f"static site smoke gate passed: {pages} HTML pages") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/scripts/generate_documented_hosted_overlay.py b/scripts/generate_documented_hosted_overlay.py index 95dd05de49..4e7fd94f9d 100644 --- a/scripts/generate_documented_hosted_overlay.py +++ b/scripts/generate_documented_hosted_overlay.py @@ -90,17 +90,24 @@ def generate(corpus_name: str, checkout: Path, current: str) -> tuple[str, int, base = _base(current) existing = _targets(base) + seen_source_targets: set[tuple[str, str]] = set() blocks: list[tuple[str, str, str]] = [] source_described = 0 for rel, path in sources: text = path.read_bytes().decode("utf-8-sig", errors="replace").replace("\r\n", "\n") lean_file = parse_source(text, rel, extra_kinds=corpus.extra_kinds) for declaration in lean_file.declarations: + target = (rel, declaration.name) + # An overlay selects by file and name, not by source occurrence. If a + # file repeats a name, it attaches to the first occurrence; never use + # a later occurrence's comment to describe that earlier declaration. + if target in seen_source_targets: + continue + seen_source_targets.add(target) description = declaration.doc or declaration.comment if not description: continue source_described += 1 - target = (rel, declaration.name) if target in existing: continue kind = "doc comment" if declaration.doc else "leading source comment" diff --git a/src/lean4_explainer/build.py b/src/lean4_explainer/build.py index bab6e87fbc..208d5bc53d 100644 --- a/src/lean4_explainer/build.py +++ b/src/lean4_explainer/build.py @@ -20,6 +20,7 @@ from .objects import Copy, Objects, index_objects from .render import ( ASSET_DIR, + FAVICON_SVG, SITE_CSS, SITE_JS, Context, @@ -41,6 +42,9 @@ ] CACHE_FORMAT = 9 +# Rendered-page compatibility is separate from the parsed-source cache. Increment this when +# shared HTML changes so incremental builds rewrite pages without needlessly rescanning Lean. +PAGE_FORMAT = 3 # Lake's build configuration and its older dependency directory are not library source. Always skipped, # at the root and in any subdirectory, on top of the user's exclude patterns. Hidden directories (.lake) # are already skipped by the scanner. @@ -207,7 +211,7 @@ def _build_site( tree = collect_tree(lean_root, config, cache_dir, jobs) for rel in tree.stale: (out_dir / (rel + ".html")).unlink(missing_ok=True) - digest = hashlib.sha256(_fingerprint(config).encode("utf-8")) + digest = hashlib.sha256(f"{_fingerprint(config)}|page:{PAGE_FORMAT}".encode("utf-8")) for rel, _ in tree.sources: entry = tree.cache.files[rel] digest.update(rel.encode("utf-8") + b"\0" + entry.names.encode("utf-8") + b"\0" + entry.lines.tobytes()) @@ -229,12 +233,17 @@ def _build_site( extensions=tuple(tree.analyses), options=config.options + (("_root", str(lean_root)),), # as `analyze` gets them: `_root` is where the sources are home=config.home, + site_url=config.site_url, + description=config.description, + project_url=config.project_url, + report_url=config.report_url, source_links=config.source_links, imports=config.imports, ) out_dir.mkdir(parents=True, exist_ok=True) written = _write(out_dir / ASSET_DIR / "site.css", SITE_CSS + "".join(ext.css(dict(config.options)) for ext, _ in tree.analyses)) + written += _write(out_dir / ASSET_DIR / "favicon.svg", FAVICON_SVG) written += _write(out_dir / ASSET_DIR / "site.js", SITE_JS) written += _write(out_dir / ".nojekyll", "") diff --git a/src/lean4_explainer/config.py b/src/lean4_explainer/config.py index b636b4d498..7dd9584dbe 100644 --- a/src/lean4_explainer/config.py +++ b/src/lean4_explainer/config.py @@ -6,6 +6,7 @@ import tomllib from dataclasses import dataclass from pathlib import Path +from urllib.parse import urlsplit from .errors import ExplainerError from .extensions import config_keys @@ -27,6 +28,10 @@ class Config: byte_budget: int = PAGES_LIMIT_BYTES source_links: str = "declaration" # "declaration": one link per declaration; "file": one per page home: str | None = None # relative URL of a landing page above this site, when it is one of several + site_url: str | None = None # canonical HTTPS base URL for this site + description: str = "Explore Lean declarations, source, explanations, and dependencies." + project_url: str | None = None # public source repository shown in the footer + report_url: str | None = None # issue/feedback URL shown in the footer glossary: str = "all" # the project's definitions in the glossary: "all", "described" (with a description) or "none" imports: str = "all" # imports on file pages: "all", "import-only" (files that only import) or "none" options: tuple[tuple[str, object], ...] = () # keys that installed extensions declared, sorted @@ -44,6 +49,10 @@ class Config: "byte_budget": int, "source_links": str, "home": str, + "site_url": str, + "description": str, + "project_url": str, + "report_url": str, "glossary": str, "imports": str, } @@ -80,6 +89,12 @@ def load_config(path: Path | None) -> Config: raise ExplainerError(f"'extra_kinds' entries must be plain keywords in {path}") if key == "source_links" and value not in ("declaration", "file"): raise ExplainerError(f"'source_links' must be \"declaration\" or \"file\" in {path}") + if key in ("site_url", "project_url", "report_url"): + parsed = urlsplit(value) + if parsed.scheme != "https" or not parsed.netloc or parsed.username or parsed.password: + raise ExplainerError(f"'{key}' must be an HTTPS URL without credentials in {path}") + if key == "site_url" and (parsed.query or parsed.fragment): + raise ExplainerError(f"'site_url' cannot contain a query or fragment in {path}") if key == "glossary" and value not in GLOSSARY_SCOPES: raise ExplainerError(f"'glossary' must be \"all\", \"described\" or \"none\" in {path}") if key == "imports" and value not in IMPORT_SCOPES: diff --git a/src/lean4_explainer/extensions.py b/src/lean4_explainer/extensions.py index 3c0df8533c..2d360dae37 100644 --- a/src/lean4_explainer/extensions.py +++ b/src/lean4_explainer/extensions.py @@ -15,7 +15,8 @@ 3. `analyze`: once per tree, with every file's summary and the name index. Returns an analysis object, which the later hooks receive. `review` then runs once all have analyzed, for issues that need another extension's analysis; `kernel_trust` is how an extension that runs Lean answers what the kernel says of a declaration. -4. `declaration_title`, `declaration_blocks`, `file_blocks`, `scripts`, `pages`, `nav_links`, `css`, `status`: rendering. +4. `declaration_title`, `declaration_blocks`, `file_preamble`, `file_blocks`, `scripts`, `pages`, `nav_links`, + `css`, `status`: rendering. `glossary`: sections of words for the glossary page, which the core writes. 5. `summary`: lines printed after a build. 6. `register_cli` / `run_cli`: extra subcommands. @@ -155,10 +156,18 @@ def declaration_blocks(self, decl: Any, payload: Any, rel: str, dirs: list[str], """HTML before and after the "also declared" block.""" return "", "" + def file_preamble(self, lean_file: Any, ctx: Any, analysis: Any) -> str: + """HTML near the top of a file page, after its path heading and before its statistics.""" + return "" + def file_blocks(self, lean_file: Any, text: str, ctx: Any, analysis: Any) -> str: """HTML after a file page's declaration list. `text` is the file's source, empty when it is not at hand.""" return "" + def promote_file_page(self, lean_file: Any) -> bool: + """Whether this file merits full share metadata instead of the compact large-corpus page shell.""" + return False + def scripts(self, options: Mapping[str, Any]) -> Sequence[str]: """Site-relative script paths (written through `pages`) that every page loads, deferred.""" return () diff --git a/src/lean4_explainer/glossary.py b/src/lean4_explainer/glossary.py index 742d45544a..0b97c54aec 100644 --- a/src/lean4_explainer/glossary.py +++ b/src/lean4_explainer/glossary.py @@ -14,7 +14,7 @@ from .extensions import GlossaryEntry, GlossarySection from .markdown import inline_html -from .render import _FILTER_HTML, Context, href, page +from .render import Context, filter_box, href, page from .scan import Declaration PAGE = "glossary.html" @@ -143,25 +143,29 @@ def glossary_pages( "

        Glossary

        ", '

        Every word this site uses, in one place: what this project defines, the words its ' "explanations and readings use, and Lean's own words. Type in the box to filter.

        ", - _FILTER_HTML, + filter_box("Filter glossary terms"), '", ] if project: + body.append('
        ') body.append('

        Defined in this project

        ') body.append(f'

        {escape(_project_intro(scope, split))}

        ') if split: body.append(_letter_row(letters, lambda letter: f"glossary-{letter}.html", counts=True)) else: body.extend(_project_list(project, letters)) + body.append("
        ") for section in (*shown, lean): + body.append('
        ') body.append(f'

        {escape(section.title)}

        ') if section.intro: body.append(f'

        {escape(section.intro)}

        ') entries = sorted(section.entries, key=lambda e: (e.term.casefold(), e.term, e.where or ("", 0, ""))) - body.append('
        ' + "".join(_entry_item(entry) for entry in entries) + "
        ") - pages = {PAGE: page("Glossary", 0, body, ctx)} + body.append('
        ' + "".join(_entry_item(entry) for entry in entries) + "
        ") + body.append("
        ") + pages = {PAGE: page("Glossary", 0, body, ctx, canonical_path=PAGE)} if split: for letter, entries in letters.items(): label = _label(letter) @@ -170,10 +174,11 @@ def glossary_pages( f'

        Definitions in this project whose names start with {escape(label)}. ' f'The whole glossary has the other sections.

        ', _letter_row(letters, lambda other: f"glossary-{other}.html", counts=False), - _FILTER_HTML, - '
        ' + "".join(_project_item(entry) for entry in entries) + "
        ", + filter_box("Filter glossary terms"), + '
        ' + "".join(_project_item(entry) for entry in entries) + "
        ", ] - pages[f"glossary-{letter}.html"] = page(f"Glossary: {label}", 0, shard, ctx) + name = f"glossary-{letter}.html" + pages[name] = page(f"Glossary: {label}", 0, shard, ctx, canonical_path=name) return pages @@ -231,11 +236,11 @@ def _project_intro(scope: str, split: bool) -> str: def _project_list(entries: list[_Entry], letters: dict[str, list[_Entry]]) -> list[str]: if len(entries) <= GROUP_AT: - return ['
        ' + "".join(_project_item(entry) for entry in entries) + "
        "] + return ['
        ' + "".join(_project_item(entry) for entry in entries) + "
        "] out = [_letter_row(letters, lambda letter: f"#g-project-{letter}", counts=False)] for letter, group in letters.items(): out.append(f'

        {_label(letter)}

        ') - out.append('
        ' + "".join(_project_item(entry) for entry in group) + "
        ") + out.append('
        ' + "".join(_project_item(entry) for entry in group) + "
        ") return out diff --git a/src/lean4_explainer/render.py b/src/lean4_explainer/render.py index e3627262b8..a9766dd734 100644 --- a/src/lean4_explainer/render.py +++ b/src/lean4_explainer/render.py @@ -6,7 +6,7 @@ from collections.abc import Iterable, Iterator, Mapping from dataclasses import dataclass, field from html import escape -from urllib.parse import quote +from urllib.parse import quote, urljoin from .extensions import Extension from .imports import docs_url @@ -15,6 +15,7 @@ from .scan import Declaration, FileSummary, LeanFile ASSET_DIR = "_assets" +FAVICON_SVG = """\n""" _NOTICE_TAIL = "Indented declarations and macro-generated declarations are not listed." @@ -24,23 +25,36 @@ def _notice(ctx: "Context") -> str: return "Generated by a source-level scanner, plus a Lean run where it succeeded: see the Trust page. Trust is UNKNOWN wherever Lean did not run. " + _NOTICE_TAIL return "Generated by a source-level scanner. Lean was not run, so axiom and trust checks are UNKNOWN. " + _NOTICE_TAIL -_FILTER_HTML = '' +def filter_box(label: str) -> str: + escaped = escape(label, quote=True) + return f'' SITE_CSS = """ :root { color-scheme: light dark; --fg: #1d1f23; --bg: #fbfbfa; --muted: #6b6e75; --line: #d9dade; --warn: #8a3b00; --warn-bg: #fff1e0; } @media (prefers-color-scheme: dark) { :root { --fg: #e6e6e6; --bg: #17181b; --muted: #9a9ca3; --line: #33363c; --warn: #ffb46b; --warn-bg: #3a2a18; } } * { box-sizing: border-box; } +[id] { scroll-margin-top: 5.5rem; } body { margin: 0; font: 16px/1.5 system-ui, sans-serif; color: var(--fg); background: var(--bg); } main { max-width: 56rem; margin: 0 auto; padding: 1.5rem; } +a:focus-visible, button:focus-visible, input:focus-visible, select:focus-visible, summary:focus-visible { outline: 3px solid var(--accent, currentColor); outline-offset: 3px; } +.skip-link { position: fixed; z-index: 100; top: 0.4rem; left: 0.4rem; padding: 0.45rem 0.7rem; background: var(--bg); border: 2px solid var(--fg); border-radius: 4px; transform: translateY(-180%); } +.skip-link:focus { transform: translateY(0); } h1 { font-size: 1.6rem; margin: 0.5rem 0 0.25rem; } h2 { font-size: 1.1rem; margin: 1.75rem 0 0.4rem; padding-bottom: 0.25rem; border-bottom: 1px solid var(--line); } a { color: inherit; } .muted, .ln, .crumbs, ol.decls > li > small { color: var(--muted); } .ln, ol.decls > li > small { font-size: 0.8rem; margin-left: 0.4rem; } -.crumbs { font-size: 0.85rem; } +.site-head { position: sticky; top: 0; z-index: 10; margin: -0.5rem 0 0.75rem; padding: 0.5rem 0 0.45rem; background: var(--bg); border-bottom: 1px solid var(--line); } +.site-head nav.top { margin-bottom: 0.15rem; } +.crumbs { font-size: 0.9rem; } +.crumbs a, .path-title a { text-underline-offset: 0.16em; } +.crumbs a:hover, .crumbs a:focus-visible, .path-title a:hover, .path-title a:focus-visible { color: var(--fg); text-decoration-thickness: 0.14em; } +.path-title { overflow-wrap: anywhere; } +.path-title a { color: inherit; } dl.summary { display: grid; grid-template-columns: max-content 1fr; gap: 0.2rem 1rem; } dl.summary dd { margin: 0; } input[type="search"] { width: 100%; margin: 0.75rem 0; padding: 0.5rem 0.75rem; font: inherit; color: var(--fg); background: transparent; border: 1px solid var(--line); border-radius: 6px; } +.filter-status { min-height: 1.5em; margin: -0.45rem 0 0.6rem; font-size: 0.85rem; color: var(--muted); } ol.decls, ul.list { list-style: none; padding: 0; } ol.decls > li, ul.list > li { padding: 0.45rem 0; border-bottom: 1px solid var(--line); } .kind, ol.decls > li > b:first-child { font-size: 0.75rem; text-transform: uppercase; letter-spacing: 0.05em; color: var(--muted); } @@ -66,7 +80,11 @@ def _notice(ctx: "Context") -> str: .warn { color: var(--warn); font-size: 0.9rem; margin: 0.3rem 0; } .src { font-size: 0.8rem; color: var(--muted); } a.term { text-decoration: underline dotted; } +a.decl-link { text-decoration: none; } +a.decl-link::after { content: " #"; color: var(--muted); opacity: 0; } +a.decl-link:hover::after, a.decl-link:focus-visible::after { opacity: 1; } nav.top { font-size: 0.9rem; margin-bottom: 0.5rem; color: var(--muted); } +.site-footer { max-width: 56rem; margin: 1rem auto 0; padding: 1rem 1.5rem 2rem; border-top: 1px solid var(--line); color: var(--muted); font-size: 0.88rem; } nav.toc, p.letters { font-size: 0.9rem; color: var(--muted); } dl.glossary { margin: 0.4rem 0; } dl.glossary dt { font-weight: 600; margin-top: 0.6rem; } @@ -77,6 +95,13 @@ def _notice(ctx: "Context") -> str: details.imports > summary, details.imported-by > summary { cursor: pointer; color: var(--muted); } details.imports ul.list, details.imported-by ul.list, section.imports ul.list { margin: 0.2rem 0 0.4rem; } details.imports ul.list > li, details.imported-by ul.list > li, section.imports ul.list > li { padding: 0.15rem 0; } +@media (max-width: 42rem) { + main { padding: 0.9rem; } + .site-head { position: static; margin-top: 0; } + .path-title { font-size: 1.18rem; } + nav.top { line-height: 1.9; } + .site-footer { padding: 0.9rem 0.9rem 1.5rem; } +} """ SITE_JS = """ @@ -87,24 +112,66 @@ def _notice(ctx: "Context") -> str: }; for (const box of document.querySelectorAll("input[data-filter]")) { - box.addEventListener("input", function () { + const scope = box.closest("main"); + const status = document.createElement("p"); + status.className = "filter-status"; + status.setAttribute("aria-live", "polite"); + box.insertAdjacentElement("afterend", status); + function filter() { const q = box.value.trim().toLowerCase(); - for (const el of document.querySelectorAll("main > ol.decls > li, main > ul.list > li, main > dl.glossary > div")) { + const rows = Array.from(scope.querySelectorAll("[data-filter-rows] > li, [data-filter-rows] > div, [data-filter-rows] > tr")); + let shown = 0; + for (const el of rows) { el.hidden = q !== "" && !el.textContent.toLowerCase().includes(q); + if (!el.hidden) shown += 1; + } + for (const section of scope.querySelectorAll("[data-filter-section]")) { + const sectionRows = Array.from(section.querySelectorAll("[data-filter-rows] > li, [data-filter-rows] > div, [data-filter-rows] > tr")); + section.hidden = q !== "" && sectionRows.length > 0 && !sectionRows.some(function (row) { return !row.hidden; }); + } + status.textContent = q === "" ? "" : (shown === 0 ? "No matches." : shown + (shown === 1 ? " match." : " matches.")); + } + box.addEventListener("input", filter); + box.addEventListener("keydown", function (event) { + if (event.key === "Escape" && box.value !== "") { + box.value = ""; + filter(); } }); } + for (const row of document.querySelectorAll("ol.decls > li[id]")) { + const code = row.querySelector(":scope > code"); + if (!code) continue; + const link = document.createElement("a"); + link.className = "decl-link"; + link.href = "#" + row.id; + link.setAttribute("aria-label", "Permanent link to " + code.textContent); + code.replaceWith(link); + link.appendChild(code); + } + const search = document.getElementById("q"); if (!search) return; const root = document.body.dataset.root || ""; const out = document.getElementById("results"); - function show(q, key) { + const searchStatus = document.getElementById("search-status"); + + function rememberQuery(value) { + if (!window.history || !window.URL) return; + const url = new URL(window.location.href); + if (value) url.searchParams.set("q", value); + else url.searchParams.delete("q"); + window.history.replaceState(null, "", url.pathname + url.search + url.hash); + } + + function show(words, key) { out.textContent = ""; let shown = 0; for (const [name, file, line] of window.L4[key] || []) { - if (!name.toLowerCase().startsWith(q)) continue; + const lower = name.toLowerCase(); + if (!words.every(function (word) { return lower.includes(word); })) continue; const item = document.createElement("li"); const link = document.createElement("a"); link.href = root + window.L4F[file] + "#L" + line; @@ -114,31 +181,40 @@ def _notice(ctx: "Context") -> str: shown += 1; if (shown === 200) break; } - if (shown === 0) out.textContent = "No matches."; + searchStatus.textContent = shown === 0 ? "No matches." : shown + (shown === 1 ? " result." : (shown === 200 ? "+ results." : " results.")); } search.addEventListener("input", function () { - const q = search.value.trim().toLowerCase(); + const raw = search.value.trim(); + const q = raw.toLowerCase(); + rememberQuery(raw); out.textContent = ""; + searchStatus.textContent = ""; if (q.length < 2) { - out.textContent = "Type at least two characters."; + searchStatus.textContent = "Type at least two characters."; return; } - const key = q.slice(0, 2).replace(/[^a-z0-9]/g, "_"); + const words = q.split(/\\s+/).filter(Boolean); + const key = words[0].slice(0, 2).replace(/[^a-z0-9]/g, "_").padEnd(2, "_"); if (window.L4[key]) { - show(q, key); + show(words, key); return; } const script = document.createElement("script"); script.src = root + "_assets/search/s_" + key + ".js"; script.onload = function () { - if (search.value.trim().toLowerCase() === q) show(q, key); + if (search.value.trim().toLowerCase() === q) show(words, key); }; script.onerror = function () { - if (search.value.trim().toLowerCase() === q) out.textContent = "No matches."; + if (search.value.trim().toLowerCase() === q) searchStatus.textContent = "No matches."; }; document.head.appendChild(script); }); + const initial = new URLSearchParams(window.location.search).get("q"); + if (initial) { + search.value = initial; + search.dispatchEvent(new Event("input")); + } })(); """ @@ -164,6 +240,10 @@ class Context: status: str = "" objects: Objects | None = None home: str | None = None + site_url: str | None = None + description: str = "Explore Lean declarations, source, explanations, and dependencies." + project_url: str | None = None + report_url: str | None = None extensions: tuple[tuple[Extension, object], ...] = () # active extensions with their analysis of the tree options: tuple[tuple[str, object], ...] = () source_links: str = "declaration" @@ -191,9 +271,13 @@ def file_page(lean_file: LeanFile, ctx: Context | None = None, text: str = "") - axioms = sum(decl.kind == "axiom" for decl in declarations) body = [ _crumbs(dirs, name), - f"

        {escape(lean_file.path)}

        ", - f'

        {_stats(len(declarations), sorry, axioms)}

        ', + _path_title(dirs, name), ] + for ext, analysis in ctx.extensions: + preamble = ext.file_preamble(lean_file, ctx, analysis) + if preamble: + body.append(preamble) + body.append(f'

        {_stats(len(declarations), sorry, axioms)}

        ') if ctx.source_url and ctx.source_links == "file": href = escape(source_href(lean_file.path, 1, ctx), quote=True) body.append(f'

        source

        ') @@ -203,8 +287,8 @@ def file_page(lean_file: LeanFile, ctx: Context | None = None, text: str = "") - if shown: body.extend(_import_blocks(lean_file, dirs, ctx)) if declarations: - body.append(_FILTER_HTML) - body.append('
          ') + body.append(filter_box("Filter declarations")) + body.append('
            ') body.extend(_decl_item(decl, lean_file.path, dirs, ctx) for decl in declarations) body.append("
          ") elif not (shown and lean_file.import_only): @@ -213,7 +297,18 @@ def file_page(lean_file: LeanFile, ctx: Context | None = None, text: str = "") - block = ext.file_blocks(lean_file, text, ctx, analysis) if block: body.append(block) - return page(lean_file.path, len(dirs), body, ctx) + # A large corpus can have more than 100,000 file pages. Keep their essential SEO and + # accessibility metadata, but reserve repeated social-card/footer markup for navigation + # and feature pages so the static artifact remains deployable. + promoted = any(ext.promote_file_page(lean_file) for ext, _ in ctx.extensions) + return page( + lean_file.path, + len(dirs), + body, + ctx, + canonical_path=lean_file.path + ".html", + compact=not promoted, + ) def _import_blocks(lean_file: LeanFile, dirs: list[str], ctx: Context) -> list[str]: @@ -280,28 +375,29 @@ def _folder_page( f'

          {_stats(folder.declarations, folder.sorry, folder.axioms)}; ' f"{folder.file_count} files

          " ) - body.append(_FILTER_HTML) + body.append(filter_box("Filter folders and files")) if folder.folders: - body.append("

          Folders

          ") - body.append('
            ') + body.append('

            Folders

            ') + body.append('
              ') for name in sorted(folder.folders): child = folders[(*dirs, name)] body.append( f'
            • {escape(name)}/ ' f'{child.file_count} files, {child.declarations} declarations
              • ' ) - body.append("
            ") + body.append("
          ") if folder.files: - body.append("

          Files

          ") - body.append('
            ') + body.append('

            Files

            ') + body.append('
              ') for summary in sorted(folder.files, key=lambda s: s.path): name = summary.path.split("/")[-1] body.append( f'
            • {escape(name)} ' f'{_file_note(summary)}
              • ' ) - body.append("
            ") - return page(page_title, len(dirs), body, ctx) + body.append("
          ") + canonical = "/".join((*dirs, "index.html")) if dirs else "index.html" + return page(page_title, len(dirs), body, ctx, canonical_path=canonical) def _file_note(summary: FileSummary) -> str: @@ -439,12 +535,21 @@ def href(from_dirs: list[str], to_rel: str, anchor: str = "") -> str: def search_page(ctx: Context) -> str: body = [ "

          Search

          ", - '', + '', + '', + '

          Matches words anywhere in qualified names. Enter at least two characters.

          ', + '

          ', '
            ', - '

            Matches qualified names that start with the query.

            ', f'', ] - return page("Search", 0, body, ctx) + return page( + "Search", + 0, + body, + ctx, + canonical_path="search.html", + description=f"Search declarations in {ctx.title}.", + ) def _stats(declarations: int, sorry: int, axioms: int) -> str: @@ -456,15 +561,33 @@ def up_path(levels: int) -> str: def _crumbs(dirs: list[str] | tuple[str, ...], tail: str) -> str: - items = [f'lean'] + items = [f'Corpus home'] for depth, name in enumerate(dirs, start=1): items.append(f'{escape(name)}') if tail: items.append(f"{escape(tail)}") - return '" + return '" -def page(title: str, depth: int, body: list[str], ctx: Context) -> str: +def _path_title(dirs: list[str] | tuple[str, ...], tail: str) -> str: + items = [] + for depth, name in enumerate(dirs, start=1): + target = up_path(len(dirs) - depth) + "index.html" + items.append(f'{escape(name)}') + items.append(f"{escape(tail)}") + return '

            ' + "/".join(items) + "

            " + + +def page( + title: str, + depth: int, + body: list[str], + ctx: Context, + *, + canonical_path: str | None = None, + description: str | None = None, + compact: bool = False, +) -> str: up = up_path(depth) links = [("All corpora", f"{up}{ctx.home}")] if ctx.home else [] links.append(("Index", f"{up}index.html")) @@ -474,6 +597,39 @@ def page(title: str, depth: int, body: list[str], ctx: Context) -> str: if ctx.search: links.append(("Search", f"{up}search.html")) nav = '" + header = ['
            ', nav] + content = body + if body and body[0].startswith('