Merge main 63ed6bd into fix/explorer-math

One conflict, in CONTRIBUTING.md: #424 condensed the CI paragraph, and this branch's sentence on the WebKit job's MathJax tarball moves into its wording.

Author: Deicyde

AGENTS.md

@@ -31,12 +31,9 @@ workflow and cross-file maintenance.
   files under `blueprint/.implementation-notes/`; they are not mathematics or
   graph state. Rendered sites, the vault's dependency summary, dashboards, and
   runtime projections are derived views, not another durable scheduler or graph.
-- In consumer formalization work, Lean imports are allowed. Follow Formalize's
-  `autoform work import-impact` policy: baseline the affected articles and
-  repeat that evidence after rebuilding, check them for active conflicts, and
-  expand ownership only for validated downstream changes; when using claims,
-  also claim the article/module and check reported claim keys. Never replace
-  that evidence boundary with a blanket import ban.
+- In consumer formalization work, Lean imports are allowed;
+  [Formalize](skills/formalize/SKILL.md#import-edits) owns that policy. Never
+  replace it with a blanket import ban.
 - Public CLI and JSON shapes are contracts. Lean server work requires an
   explicit project root, bounded time and output, verified descendant cleanup,
   and no retry after dispatch with an unknown outcome. A project root is not an
@@ -73,4 +70,4 @@ The [CLI reference](autoform_cli/README.md) gives each command's exact rules.
 | `work`, `search` | invalid usage (2); bytes changed since the graph loaded; a refused library; under `--module-scope import-closure`, a file outside the captured sources that may import the closure | none; they leave out values they cannot represent, which `check` warns about |
 | `library index` | a missing or stale build (2); a stale index under `--check` (1) | none |
 | `project`, `doctor` | an inspection or catalog error, a failed diagnosis | a release pairing it cannot resolve |
-| `init` | an existing entry that differs from one it manages, without `--force` | the entries it left alone |
+| `init` | an input or target it cannot use safely: a case or Unicode variant of a path it manages (even with `--force`), a link or unusable root `.gitignore` in the way, a directory it cannot list, an invalid option or pinned Autoform tree | the existing entries it left alone; CI it skips when there is no Autoform ref to pin |

CHANGELOG.md

@@ -19,6 +19,9 @@ date when the release is tagged.
   commands, and a listing that runs out of time or is interrupted no longer
   leaves its transport running. Formalize treats a labelled `claim list`
   failure as an unreadable board, not as a board without claims (#432).
+- **Render.** An article's page lists its `mathlib_declaration` names in a
+  Mathlib row, as text without a link, so a `mathlib: true` article names the
+  declaration it restates (#388).
 - **Builds.** `project new` turns on Lake's artifact cache with
   `enableArtifactCache` and `restoreAllArtifacts`, so checkouts and worktrees
   on one toolchain reuse each other's builds; Setup offers the same two lines

CONTRIBUTING.md

@@ -22,31 +22,24 @@ dependency explorer regressions` installs the `browser` extra and WebKit and
 runs `tests/test_dag_viewer_browser.py` with `AUTOFORM_REQUIRE_BROWSER_TESTS=1`,
 so a missing browser fails the job instead of skipping its tests; locally they
 skip without the extra, and `make test-browser` installs both and runs them as
-CI does. `MathJax read-back cards (Node)` downloads the npm tarball of MathJax
-3.2.2, checks its sha256, and runs `tests/test_site_mathjax_node.py` in Node
-with `AUTOFORM_REQUIRE_MATHJAX_TESTS=1`; locally those tests skip unless `node`
-is on `PATH` and `AUTOFORM_MATHJAX_DIR` names an unpacked MathJax 3.2.2
-package. The WebKit job unpacks the same checked tarball too, for the
-explorer's typesetting test, which serves MathJax from it in place of the CDN
-and skips the same way. `real Lean
-(fixture toolchain)` builds and audits a project from the bundled Mathlib
-release and runs
-the real-Lean suites other than the skeleton suite, which `real Lean skeleton
-suite` runs with one `tests/test_project_inspect.py` test. Another job runs the
-inspection, bounded-subprocess, and transactional-output tests on Windows, and
-the last builds
-`tests/fixtures/repl-smoke` and runs `tests/test_real_repl.py` against the
-pinned upstream REPL, also checking the header parser on the oldest Lean release
-Autoform supports. Locally, tests that need Lean skip when
-`lake` is not on `PATH`. Those in `tests/test_skeleton.py`, `test_impact.py`,
-`test_contract.py`, `test_lake_artifact_audit.py`, `test_lsp_protocol.py` and
-`test_batch_diagnostics.py` also skip when elan is installed but the
-toolchain pinned in `tests/fixtures/skeleton-project/lean-toolchain` is
-missing; only the real-Lake test in `tests/test_project_inspect.py` lets elan
-download it. The `tests/test_library_generate.py`
-ones that run Lean build a fixture that clones Batteries from GitHub, so they
-run only when `AUTOFORM_REQUIRE_REAL_LIBRARY_TESTS=1` is set, as their CI job
-does; a missing toolchain or a failed download then fails them. Run
+CI does. The `MathJax read-back cards (Node)` tests skip locally unless `node`
+is on `PATH` and `AUTOFORM_MATHJAX_DIR` names an unpacked MathJax 3.2.2 package;
+`AUTOFORM_REQUIRE_MATHJAX_TESTS=1`, which CI sets, makes that a failure. The
+WebKit job unpacks the same checked MathJax tarball for the explorer's
+typesetting test, which serves MathJax from it in place of the CDN and skips
+the same way without it. The other jobs, which build and audit a project from the bundled Mathlib release,
+run the real-Lean suites, run the inspection, subprocess, and publication tests
+on Windows, and run `tests/test_real_repl.py` against the pinned upstream REPL,
+are listed with the tests each runs in
+[`tests.yml`](.github/workflows/tests.yml). Locally, tests that need Lean skip
+when `lake` is not on `PATH`, and most also skip when elan is installed but the
+toolchain pinned in `tests/fixtures/skeleton-project/lean-toolchain` is missing;
+only the real-Lake test in `tests/test_project_inspect.py` lets elan download
+it. `AUTOFORM_REQUIRE_REAL_LEAN_TESTS=1`, which CI sets, makes a missing
+toolchain a failure instead. The `tests/test_library_generate.py` tests that run
+Lean clone Batteries from GitHub, so they run only with
+`AUTOFORM_REQUIRE_REAL_LIBRARY_TESTS=1`, and then a missing toolchain or a
+failed download fails them. Run
 `lake build` in `skills/setup/assets/cabannes-thesis-project` when you change
 the example's Lean sources or declarations.