fix(release): retain project API docs on Pages

.github/workflows/publish_release_pages.yml

@@ -213,8 +213,10 @@ jobs:
               raise SystemExit("Pages artifact must use the /ReasBook/ base path")
           if manifest.get("artifact") != "pages":
               raise SystemExit("GitHub Pages requires the pages artifact")
-          if manifest["total_bytes"] > 850_000_000:
-              raise SystemExit("Pages site exceeds the 850 MB operational budget")
+          if manifest["total_bytes"] > 1_000_000_000:
+              raise SystemExit("Pages site exceeds GitHub's 1 GB hard limit")
+          if manifest["total_bytes"] > 920_000_000:
+              raise SystemExit("Pages site exceeds the 920 MB operational budget")
           if manifest["file_count"] > 60_000:
               raise SystemExit("Pages site exceeds the 60,000-file budget")
           artifacts = release_set.get("artifacts")

CHANGELOG.md

@@ -17,8 +17,9 @@ Significant user-facing and release-engineering changes are recorded here.
 ### Changed
 
 - GitHub Pages is a publish-only target; full Lean builds run on SiFlow.
-- GitHub Pages now receives a size-bounded canonical projection with lightweight
-  compatibility redirects and detailed-API placeholders; the full historical
+- GitHub Pages now retains every selected project's API pages while using
+  lightweight placeholders only for external dependencies. Its operational
+  site budget is 920 MB with an independent 1 GB hard gate; the full historical
   site remains unchanged for self-hosting.
 - Repository scripts are thin project adapters while reusable behavior lives
   in the SDK packages.

config/deploy/github-pages.yml

@@ -25,9 +25,10 @@ policy:
 
 # A release has one build identity and two immutable delivery artifacts.
 # The full artifact retains bounded reachable project-module API docs and every
-# project version for self-hosting. Pages keeps canonical Verso versions and
-# project entry API pages; omitted detailed API links become explicit
-# placeholders whose source pages must exist in the verified full artifact.
+# project version for self-hosting. Pages keeps canonical Verso routes and all
+# API pages owned by every selected ProjectSpec; omitted external-dependency
+# API links become explicit placeholders whose source pages must exist in the
+# verified full artifact.
 artifacts:
   full:
     history_mode: full
@@ -40,7 +41,7 @@ artifacts:
     history_mode: canonical
     dependency_docs: stubs
     max_site_files: 60000
-    max_site_bytes: 850000000
+    max_site_bytes: 920000000
     max_archive_members: 180000
     max_bundle_bytes: 950000000
 

docs/decisions/0002-target-specific-release-artifacts.md

@@ -2,7 +2,7 @@
 
 ## Status
 
-Accepted
+Accepted; project-owned API projection superseded in part by ADR-0008
 
 ## Date
 
@@ -53,6 +53,8 @@ pages, and theorem map remained available at their original URLs.
   exists in the full site. This preserves link closure without allowing the
   projection to hide a missing build output. The complete API documentation
   remains in the `full` artifact for self-hosting.
+  **Superseded by ADR-0008:** Pages now retains every API page owned by a
+  selected `ProjectSpec`; only external-dependency API pages use placeholders.
 - Every theorem map, whether generated or curated, carries a generated release
   context that matches its project specification. Repository source links are
   pinned to the full project commit; the branch name remains display metadata
@@ -100,6 +102,8 @@ pages, and theorem map remained available at their original URLs.
   except exact `.git` and `.github` path segments, which are rejected because
   GitHub always omits them. These are operational margins below GitHub's hard
   limits, not targets to fill.
+  **Superseded by ADR-0008:** the extracted-content operational limit is now
+  920 MB, with a separately enforced 1 GB hard gate. The other limits remain.
 - Self-hosted deployment accepts only the `full` artifact. It installs into a
   versioned directory, exposes the configured base path below `public/`, and
   atomically switches a `current` symlink. A failed health check restores the

docs/decisions/0008-project-owned-api-docs-on-pages.md

@@ -0,0 +1,116 @@
+# ADR-0008: Retain project-owned API documentation on GitHub Pages
+
+## Status
+
+Accepted
+
+## Date
+
+2026-09-05
+
+## Context
+
+ADR-0002 introduced a bounded GitHub Pages projection because the complete
+release site is already larger than GitHub Pages' 1 GB published-site limit.
+That projection retained only one API entry page per canonical project and
+replaced every deeper API link with a small placeholder.
+
+The resulting site fit comfortably within its 850,000,000-byte operational
+budget, but it did not provide usable API documentation.  In release
+`site-20260905T124421Z-e986b071fe51`, 5,520 of 7,183 HTML files in the Pages
+artifact were projection placeholders.  A reader could open a `Book`, `Paper`,
+or `Main` entry and then immediately leave the real documentation when
+following a chapter or declaration link.
+
+The same release provides enough evidence to choose a more useful boundary:
+
+- the existing Pages artifact is 712,116,853 bytes;
+- restoring every ReleaseSpec-owned project API page projects to about
+  885 MB; and
+- the complete self-hosted artifact is about 2.36 GB and therefore remains
+  unsuitable for GitHub Pages.
+
+GitHub documents a [1 GB limit for a published Pages
+site](https://docs.github.com/en/pages/getting-started-with-github-pages/github-pages-limits).
+The temporary GitHub deployment needs a smaller fail-closed operational
+budget, while the long-term self-hosted artifact must remain unchanged.
+
+## Decision
+
+- A `ProjectSpec` is the authority for API-document ownership.  For every
+  selected project version on a branch, the Pages projector copies all
+  existing documentation shapes derived from its kind and project identifier,
+  including nested `Books` or `Papers` layouts, flat namespace directories,
+  and a same-name top-level HTML entry.
+- Canonical selection continues to control catalog redirects and Verso routes.
+  It does not turn a non-canonical project version's API pages into external
+  dependency placeholders when a canonical project links to them.
+- A project API page may still link to a non-canonical Verso route omitted by
+  the Pages history policy. The projector closes that link with a lightweight
+  redirect to the project's verified canonical Verso route, preserving the
+  matching deep suffix when it exists. This is a history redirect, not an API
+  documentation placeholder.
+- The projector copies project documentation before computing link closure.
+  Consequently, links introduced by detailed project pages participate in the
+  same validation pass.
+- API pages outside all ReleaseSpec-derived ownership roots become explicit
+  external-dependency placeholders only when the verified source already marks
+  them external or their namespace is an allowed dependency such as Mathlib,
+  Lean, Batteries, or Init. Unknown unmarked namespaces fail closed instead of
+  silently hiding a project page.
+- The Pages operational limit is 920,000,000 bytes.  A separate
+  1,000,000,000-byte GitHub hard limit is enforced independently in profile
+  validation, local projection, bundle verification, and the publish workflow.
+  Raising the operational budget cannot disable the host limit.
+- Capacity overflow fails during local or remote packaging before an immutable
+  Release is published.  Selection is never changed implicitly to make an
+  oversized artifact fit.
+- The `full` artifact, its version-qualified URLs, and the self-hosted atomic
+  installation process are unchanged.
+
+This decision supersedes ADR-0002 only where it says that Pages retains project
+entry API pages while replacing detailed project API pages with placeholders.
+ADR-0002 continues to govern target-specific bundles, canonical history,
+ReleaseSet binding, immutable publication, and self-hosted delivery.
+
+## Alternatives considered
+
+### Keep only project API entry pages
+
+Rejected because the entry is not useful when its first project-module link
+leads to a generic capacity notice.
+
+### Copy every versioned documentation directory without ownership checks
+
+Rejected because it erases the contract between project content and external
+dependencies.  ReleaseSpec-derived roots make the boundary deterministic and
+cause an unknown project layout to fail instead of being silently reclassified.
+
+### Set the operational budget equal to GitHub's hard limit
+
+Rejected because metadata and normal project growth need headroom.  The
+920 MB budget leaves an independent 80 MB host margin and makes the next
+capacity decision explicit.
+
+### Change or trim the self-hosted artifact
+
+Rejected because the full artifact is the durable deployment target and is not
+subject to GitHub Pages' temporary hosting constraint.
+
+## Consequences
+
+- Detailed project API links work on GitHub Pages and remain byte-identical to
+  the verified branch output.
+- External dependency links remain visibly bounded instead of silently
+  increasing the artifact with transitive documentation.
+- Links from retained historical API pages to omitted historical Verso pages
+  converge on the explicit canonical project version without copying the
+  approximately 152 MB historical route trees.
+- The current release family has roughly 35 MB of operational headroom.  A
+  future release that crosses 920 MB must reduce a measured large component
+  (for example a generated Verso route) or move public serving to the
+  self-hosted deployment; it must not restore broad placeholders implicitly.
+- Changing this projection and its capacity policy changes the artifact-policy
+  digest and therefore requires a new immutable Release.  Existing Lean,
+  documentation, Verso, and theorem-map branch artifacts remain reusable after
+  identity revalidation.

sdk/deploy/README.md

@@ -269,9 +269,11 @@ for the allowed large archive is network-dominated.
 
 The Pages capacity policy is single-source: local packaging, local acceptance,
 and the workflow's `release verify --profile github-pages --artifact-policy
-pages` use the same checked-in 850 MB, 60,000-file, and
-180,000-archive-member limits. A bundle that the workflow would reject cannot
-pass local packaging merely because a verifier default was looser.
+pages` use the same checked-in 920 MB, 60,000-file, and
+180,000-archive-member operational limits. A separate 1 GB hard gate is
+enforced even if the operational policy is later raised. A bundle that the
+workflow would reject cannot pass local packaging merely because a verifier
+default was looser.
 
 When `--wait` is present, the command first waits up to 1,800 seconds for the
 workflow and then up to 300 seconds for the public Pages ReleaseSpec to

sdk/deploy/src/reasbook_deploy_sdk/release/README.md

@@ -34,7 +34,7 @@ The two artifacts have deliberately different content contracts:
 | Name | Contract | Intended target |
 | --- | --- | --- |
 | `full` | Every assembled project version, reachable project-module API docs, Verso, theorem maps, and explicit dependency stubs | Self-hosted server |
-| `pages` | Canonical version-qualified Verso routes, project entry API pages, theorem maps, and link-closed API placeholders | GitHub Pages |
+| `pages` | Canonical version-qualified Verso routes, every selected project's API pages, theorem maps, and external-dependency API placeholders | GitHub Pages |
 
 Both retain the `/ReasBook/` public base path. `release-set.json` binds their
 bundle hashes, site-tree hashes, sizes, and projection-policy hash to one
@@ -223,7 +223,8 @@ workflow uses GitHub's Release and per-asset verification commands,
 independently checks the tag target,
 archive/manifest/spec/ReleaseSet bindings, and recomputes the policy digest
 from its trusted checked-out profile. It enforces the compressed,
-180,000-archive-member, 850 MB site, and 60,000-file budgets before extraction.
+180,000-archive-member, 920 MB site, and 60,000-file operational budgets before
+extraction, plus an independent 1 GB published-site hard gate.
 Local packaging and acceptance load the same artifact policy, so these limits
 cannot first appear as a remote-only rejection. It has no full archive and
 performs no source build. Publishing an existing tag is
@@ -284,12 +285,12 @@ docs start at each configured entry root and include every reachable
 project-owned module, processed in batches of at most 128; Mathlib, Lean, and
 other external libraries are not rendered. The `full` artifact retains those
 generated module pages and every assembled project version. The Pages
-projection is assembled from an allowlist: explicit canonical versions,
-project entry API pages, Verso pages, theorem maps, and referenced runtime
-assets. Detailed API links omitted from that bounded artifact resolve to small
-explanatory placeholders only when the verified full site contains the target;
-they never become silent 404s. Unversioned catalog compatibility paths are
-redirects rather than copies of the large Verso trees.
+projection is assembled from an allowlist: canonical Verso routes, every API
+documentation shape owned by a selected `ProjectSpec`, theorem maps, and
+referenced runtime assets. API links outside those project-owned roots resolve
+to small external-dependency placeholders only when the verified full site
+contains the target; they never become silent 404s. Unversioned catalog
+compatibility paths are redirects rather than copies of the large Verso trees.
 
 ## Self-hosted installation