feat: static content archives

.github/workflows/ci.yml

@@ -145,6 +145,12 @@ jobs:
               run: |
                   inkscape --version
 
+            # The tests check that the tutorial emitter's own rendered HTML content loads through
+            # the same reader that a consuming site uses, so it is generated first.
+            - name: Generate the test tutorial site as rendered HTML content
+              run: |
+                  lake exe tutorial-example-rendered-html
+
             - name: Run tests
               run: |
                   lake test -- --verbose --check-tex
@@ -181,6 +187,22 @@ jobs:
               run: |
                   linkchecker --config=.linkchecker/linkcheckerrc --no-status ./_out/tut/
 
+            - name: Generate the site that mounts rendered HTML content
+              run: |
+                  lake exe mount-site --output _out/test-projects/mount-site
+
+            - name: Check internal links on the mounting site
+              run: |
+                  linkchecker --config=.linkchecker/linkcheckerrc --no-status ./_out/test-projects/mount-site/
+
+            # A site is served from wherever its root is mounted, so nothing that Verso emits may be
+            # root-relative. The fixture holds one on purpose, to pin that content may.
+            - name: Check that the generated sites work under a URL prefix
+              run: |
+                  ./scripts/check-url-prefix.sh _out/test-projects/demosite
+                  ./scripts/check-url-prefix.sh _out/tut
+                  ./scripts/check-url-prefix.sh _out/test-projects/mount-site --allow 'href="/"$'
+
             - name: Generate the manual
               run: |
                   ./generate.sh
@@ -268,8 +290,15 @@ jobs:
                     browser-tests/test_search_page.py \
                     browser-tests/test_toc_resize.py \
                     browser-tests/test_redirect.py \
+                    browser-tests/test_search_path_prefix.py \
                     browser-tests/test_katex.py -v
 
+            - name: Run the mounted content browser tests
+              run: |
+                  uv run --project browser-tests --extra test pytest \
+                    browser-tests/mount-site -v \
+                    --site-dir "$(pwd)/_out/test-projects/mount-site"
+
             - name: Build the VersoHtml site for browser tests
               run: |
                   # The verso-html genre renders literate JSON into a standalone HTML site.

.gitignore

@@ -16,6 +16,11 @@ multi.json
 single.json
 *.html
 !/doc/stats.html
+# Rendered HTML content fixtures are checked in and never regenerated. A new fixture directory
+# needs its own line here, or its fragments are silently left out of the repository.
+!/test-projects/rendered-html-fixture/**/*.html
+!/test-projects/rendered-html-sparse-fixture/**/*.html
+!/test-projects/rendered-html-conflict-fixture/**/*.html
 *.produced.out
 __pycache__
 test-projects/literate-config/lake-manifest.json

.prettierignore

@@ -8,6 +8,11 @@ html-multi
 htmlout
 .playwright-browsers
 
+# Hand-written fixtures, whose exact markup and JSON are what the tests read
+test-projects/rendered-html-fixture
+test-projects/rendered-html-sparse-fixture
+test-projects/rendered-html-conflict-fixture
+
 # Vendored files
 vendored-js
 *.min.js

browser-tests/mount-site/test_mounted_content.py

@@ -0,0 +1,61 @@
+"""Tests for a page that mounts rendered HTML content.
+
+The document carries the scripts of two Verso releases at once: the site's own, which reach the
+markup that the site rendered, and the mounted content's, which reach the markup that shipped with
+it. Nothing static shows how they behave together, so these tests drive a browser.
+"""
+
+from playwright.sync_api import expect, Page
+
+MOUNTED_PAGE = "/tutorials/v1/hashmap/"
+
+# The site's own content on a mounted page.
+SITE_MATH = "#site-math"
+SITE_TOKEN = "#site-token"
+
+# The mounted content's own markup.
+MOUNTED = ".verso-content.content"
+
+
+class TestMountedContent:
+    def test_math_is_rendered_once(self, server: str, page: Page):
+        page.goto(f"{server}{MOUNTED_PAGE}")
+        page.wait_for_load_state("networkidle")
+
+        math = page.locator(".math.inline, .math.display")
+        expect(math).not_to_have_count(0)
+        for i in range(math.count()):
+            expect(math.nth(i).locator(".katex")).to_have_count(1)
+
+        # Both the site's own math and the mounted content's math are rendered.
+        expect(page.locator(f"{SITE_MATH} .katex")).to_have_count(1)
+        expect(page.locator(f"{MOUNTED} .math.inline .katex")).not_to_have_count(0)
+
+    def test_hovers_work_on_the_sites_own_code(self, server: str, page: Page):
+        page.goto(f"{server}{MOUNTED_PAGE}")
+        page.wait_for_load_state("networkidle")
+
+        page.locator(SITE_TOKEN).hover()
+        expect(page.locator("[data-tippy-root]")).not_to_have_count(0)
+
+    def test_hovers_work_on_the_mounted_code(self, server: str, page: Page):
+        page.goto(f"{server}{MOUNTED_PAGE}")
+        page.wait_for_load_state("networkidle")
+
+        token = page.locator(f"{MOUNTED} .hl.lean .const.token").first
+        expect(token).to_be_visible()
+        token.hover()
+        expect(page.locator("[data-tippy-root]")).not_to_have_count(0)
+
+    def test_the_wrappers_are_separate(self, server: str, page: Page):
+        page.goto(f"{server}{MOUNTED_PAGE}")
+        page.wait_for_load_state("networkidle")
+
+        # The mounted content is marked as Verso content, and the site's own code on the same
+        # page is not, which is what keeps the two releases' scripts off each other's markup.
+        expect(page.locator(f"{MOUNTED}[data-verso-docs]")).to_have_count(1)
+        expect(
+            page.locator(f"{SITE_TOKEN}").locator(
+                "xpath=ancestor::*[contains(@class,'verso-content')]"
+            )
+        ).to_have_count(0)

doc/UsersGuide/Basic.lean

@@ -6,6 +6,7 @@ Author: David Thrane Christiansen
 import VersoManual
 import UsersGuide.Markup
 import UsersGuide.Websites
+import UsersGuide.RenderedHtml
 import UsersGuide.Manuals
 import UsersGuide.Elab
 import UsersGuide.Extensions
@@ -110,6 +111,8 @@ Mixing incompatible features results in an ordinary Lean type error.
 
 {include 0 UsersGuide.Websites}
 
+{include 0 UsersGuide.RenderedHtml}
+
 {include 0 UsersGuide.Manuals}
 
 {include 0 UsersGuide.Literate}

doc/UsersGuide/Output/HTML.lean

@@ -41,6 +41,8 @@ They are typically produced using an embedded DSL that is available when the nam
 
 {docstring Html.visitM}
 
+{docstring Html.rewriteUrls}
+
 {docstring Html.format}
 
 {docstring Html.asString}
@@ -151,7 +153,7 @@ The element's text content is the TeX code, which is not processed while generat
 For example, `` $`\frac{1}{2}` `` is represented in HTML as `<code class="math inline">\frac{1}{2}</code>`.
 
 Math is typeset in the browser using the bundled KaTeX library.
-When a page has loaded, the script in {name}`Html.math.js` renders every element with these classes.
+When a page has loaded, the script produced by {name}`Html.mathJs` renders every element with these classes.
 Pages that contain mathematical notation should include this script together with KaTeX itself: its stylesheet ({name}`Html.katex.css`), its code ({name}`Html.katex.js`), and its fonts ({name}`Html.katexFonts`).
 The stylesheet refers to the fonts by relative paths, so the file layout described in their docstrings should be preserved.
 
@@ -161,4 +163,4 @@ The stylesheet refers to the fonts by relative paths, so the file layout describ
 
 {docstring Html.katexFonts}
 
-{docstring Html.math.js}
+{docstring Html.mathJs}

doc/UsersGuide/Releases/Entries.lean

@@ -22,6 +22,7 @@ public import UsersGuide.Releases.Entries.LiterateHtmlKatex
 public import UsersGuide.Releases.Entries.LiterateProgramming
 public import UsersGuide.Releases.Entries.MethodInMultiVerso
 public import UsersGuide.Releases.Entries.ReleaseNotesChapter
+public import UsersGuide.Releases.Entries.RenderedHtmlContent
 public import UsersGuide.Releases.Entries.RoleDiagnostics
 public import UsersGuide.Releases.Entries.SearchPriority
 public import UsersGuide.Releases.Entries.VersionedReleaseNotes

doc/UsersGuide/Releases/Entries/RenderedHtmlContent.lean

@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2026 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+module
+
+public import UsersGuide.Releases.Entry
+import VersoBlog
+
+open Verso.Genre Manual InlineLean UsersGuide.Releases
+
+release_note
+  version := ⟨4, 34, 0⟩
+  breaking := true
+  tag := "rendered-html-content"
+  prs := [964]
+
+open Verso.Output.Html.Files
+
+open Verso.Genre
+
+#doc (Manual) "Rendered HTML Content" =>
+
+A Verso document can now render to a directory of HTML fragments, and the website genre supports integrating these fragments into a particular theme.
+
+:::paragraph
+Exported content can be rendered to a directory of fragments, and Verso websites can mount this exported content into their own URL structure, integrating it into their navigation structure and theme.
+This feature is described in a {ref "rendered-html"}[dedicated section].
+To make it possible for HTML fragments to be reliably bundled with required CSS and JavaScript, several changes were made that affect all rendered HTML:
+
+* Hover text is fetched from the path named by the nearest enclosing element carrying `data-verso-docs`, rather than from a fixed path, so one document holds as many sources of hover text as it holds regions of Verso content.
+  The prior behavior is a fallback when no `data-verso-docs` element is found.
+* Verso's scripts confine their queries, their listeners, and the data they fetch to the elements they were given, and register their listeners additively, so a page may include scripts from several Verso releases without them interfering with each others' markup.
+  The math script marks what it has rendered, preventing double rendering.
+* In the blog genre, KaTeX and `marked` are served from the site itself rather than from a CDN, so a page depends on nothing on the network.
+* The stylesheets and scripts that traversal accumulates are emitted as file references rather than as inline text, and the assets that have no name of their own are named by a hash of their contents.
+* A site's own scripts now skip any subtree marked with `verso-content`, which is what a mounted directory's markup carries, so they reach the site's own pages and nothing that a mount contributed.
+:::
+
+# Breaking Changes
+%%%
+tag := none
+%%%
+* The types that describe a genre's stylesheets and scripts were moved from the `Verso.Genre.Manual.Files` namespace to `Verso.Output.Html.Files`, where every genre that emits HTML can reach them.
+  In particular, {name}`CSS`, {name}`JS`, {name}`StaticCssFile`, {name}`CssFile`, {name}`StaticJsFile`, {name}`JsSourceMap`, and {name}`JsFile` were moved, and the modules `VersoManual.Html.Basic`, `VersoManual.Html.CssFile`, and `VersoManual.Html.JsFile` were replaced by `Verso.Output.Html.Files`.
+  The files should be sorted using the helper {name}`Verso.Output.Html.Files.sortByAfter`, which ensures that the ordering constraints between scripts are respected.
+
+* {name}`Blog.Theme.cssFiles` and {name}`Blog.Theme.jsFiles` contain {name}`CssFile` and {name}`JsFile` rather than tuples, as do {name}`Blog.TraverseState.cssFiles` and {name}`Blog.TraverseState.jsFiles`.
+
+* The `path` parameter that the website genre passes to the `post` and `archiveEntry` templates now includes a trailing slash.
+  `Blog.dirPathToString` has been replaced by `Verso.Multi.Path.relativeLink`.
+  Links to posts and to categories from these templates end in `/`, as the links from the post list already did.
+
+* A theme invokes {name}`Blog.Template.builtinHeader` before defining its own custom properties, so that its definitions override the ones that the header emits.
+  {name}`Blog.Theme.default` has been changed accordingly.
+  `Verso.Genre.Blog.Traverse.renderMathJs` and `Verso.Output.Html.math.js` have been consolidated to {name}`Verso.Output.Html.mathJs`.
+  {name Verso.Output.Html.mathJs}`mathJs` and {name}`Verso.Code.highlightingJs` take the selector for the elements their script belongs to, which is {lean}`"body"` for a whole page.