+ ...
+
+```
+
+`verso-content` marks a subtree as Verso content and is stable across Verso releases.
+The class names inside a fragment's markup are those that the content's own stylesheets style, and they may change from one release to the next.
+A site that styles a fragment's markup itself, such as one that places the local table of contents and styles it against `nav.local-toc`, writes its rules against the markup of the release that produced the content, and content from another release may need adaptor rules that bridge the two.
+:::
+
+## Conventions
+%%%
+tag := "fragment-conventions"
+%%%
+
+The fragment named `content` holds the page's body and is always present.
+A tutorial page also has `localNav` when it has a local table of contents, a code download, or a live editor link.
+
+
+# The URL Token
+%%%
+tag := "rendered-html-token"
+%%%
+
+Fragments are stored as text, so URLs in them are written relative to a unique token rather than to a fixed
+root.
+The consumer can relocate the markup in the URL hierarchy via a string replacement operation, rather than by parsing HTML and other languages.
+
+A fragment's token stands for the root of the mounted content.
+A consumer replaces it with a prefix such that the token followed by `/x` resolves to `x` under the mount point in the document that the consumer produces.
+The token expands with no trailing slash, and the content writes the separator.
+Each fragment specifies its own token in the manifest, and the producer chooses a token that does not occur in that fragment's content.
+
+{docstring Verso.RenderedHtml.defaultRootToken}
+
+{docstring Verso.RenderedHtml.chooseToken}
+
+{docstring Verso.RenderedHtml.hasToken}
+
+{docstring Verso.RenderedHtml.substitute}
+
+# Stylesheets, Scripts, and Theming
+%%%
+tag := "rendered-html-theming"
+%%%
+
+A Verso-based website places a mount's stylesheets and scripts through
+{name Verso.Genre.Blog.Template.builtinHeader}`builtinHeader`.
+A consumer of another kind places them as described here.
+
+Each stylesheet has an associated role.
+Stylesheet roles are:
+
+: `variables`
+
+ Defines default values for `--verso-*` custom properties on `:root`.
+ Consumers should emit these prior to Verso's defaults and their own themes, so that those will override the included content.
+
+: `content`
+
+ Styles the markup and reads the properties.
+ Consumers should emit these last, so that they take precedence over others.
+ A role that a consumer does not recognize is placed as `content`.
+
+
+When a Verso release renames a `--verso-*` property, archived content that reads the earlier name
+continues to render, because it carries its own value for that name.
+A site that wants such content to follow its theme defines the earlier name in terms of the current
+one in an adaptor stylesheet of its own, which applies to every mount, and the archived directory itself is
+untouched.
+
+A script under the static directory touches only nodes inside the wrapper that it belongs to.
+Each wrapper carries the identifier that its scripts select on, and each script confines its
+queries, its listeners, and the data that it fetches to that subtree.
+A page therefore carries the scripts of several Verso releases, and of the consuming site, without
+any of them affecting each other's markup.
+
+A directory also ships the libraries that its pages need, such as KaTeX, so a site that places
+several directories holds several copies of one library, under file names that need not match.
+These are plain scripts that assign globals, so the copy placed last owns the global, and their
+stylesheets follow the cascade in the same way.
+A stylesheet or script that is a copy of a library says which one in `provides`, which is what a
+site reads if it decides to place a single copy rather than all of them.
+
+{docstring Verso.Genre.Blog.Template.MountedAssets}
+
+# The Stability Contract
+%%%
+tag := "rendered-html-contract"
+%%%
+
+To enable the display of archived content without rebuilding it, producers and consumers may rely on the following properties:
+
+* Within a format version, the manifest only gains fields, and the format version is incremented only for a change that cannot be expressed as an additional field.
+ A consumer reads every format version up to and including its own, ignores unknown fields, and accepts an unrecognized value of an enumerated
+ field.
+
+* Fragments are rooted at a `` and carry no ``, ``, ` [--allow ]
+
+set -euo pipefail
+
+usage() {
+ echo "usage: $0 [--allow ]" >&2
+ exit 2
+}
+
+site=""
+allow=""
+while [ $# -gt 0 ]; do
+ case "$1" in
+ --allow)
+ [ $# -ge 2 ] || usage
+ allow="$2"
+ shift 2
+ ;;
+ -*) usage ;;
+ *)
+ [ -z "$site" ] || usage
+ site="$1"
+ shift
+ ;;
+ esac
+done
+
+[ -n "$site" ] || usage
+[ -d "$site" ] || {
+ echo "No such directory: $site" >&2
+ exit 2
+}
+
+prefix="a/url/prefix"
+work="$(mktemp -d)"
+trap 'rm -rf "$work"' EXIT
+mkdir -p "$work/$prefix"
+cp -R "$site/." "$work/$prefix/"
+
+# The attributes are the ones that `Verso.Output.Html.rewriteUrls` rewrites. An attribute name is
+# taken whole, so `metadata` is not read as `data`. A candidate list is checked at its first URL,
+# which is where a root-relative one in emitted content appears.
+#
+# A protocol-relative URL begins with two slashes and is left alone.
+attrs='href|src|data|poster|action|formaction|cite|ping|srcset|imagesrcset'
+pattern="(^|[[:space:]])($attrs)=\"/([^/\"]|\")|url\\([\"']?/[^/]"
+
+rc=0
+hits="$(grep -REon --include='*.html' --include='*.css' "$pattern" "$work/$prefix")" || rc=$?
+if [ "$rc" -gt 1 ]; then
+ echo "Failed to scan '$site' for root-relative URLs." >&2
+ exit 2
+fi
+if [ -n "$allow" ] && [ -n "$hits" ]; then
+ rc=0
+ hits="$(printf '%s\n' "$hits" | grep -Ev "$allow")" || rc=$?
+ if [ "$rc" -gt 1 ]; then
+ echo "Failed to apply --allow to the scan of '$site'." >&2
+ exit 2
+ fi
+fi
+
+if [ -n "$hits" ]; then
+ echo "Root-relative URLs in '$site' break when the site is served under a URL prefix:" >&2
+ printf '%s\n' "$hits" | sed "s|^$work/$prefix/||" >&2
+ exit 1
+fi
+
+if command -v linkchecker >/dev/null 2>&1; then
+ linkchecker --config=.linkchecker/linkcheckerrc --no-status "$work/$prefix/"
+else
+ echo "linkchecker is not installed, so only the URL check ran." >&2
+fi
+
+echo "'$site' works under a URL prefix."
diff --git a/src/multi-verso/MultiVerso/Slug.lean b/src/multi-verso/MultiVerso/Slug.lean
index 429994065..629390b25 100644
--- a/src/multi-verso/MultiVerso/Slug.lean
+++ b/src/multi-verso/MultiVerso/Slug.lean
@@ -110,16 +110,16 @@ where
/--
Converts a string to a valid slug, mangling as appropriate.
-/
-def asSlug (str : String) : String :=
- let rec loop (iter : String.Legacy.Iterator) (acc : String) : String :=
- if iter.atEnd then acc
- else
- let c := iter.curr
- loop iter.next <|
- if c ∈ Slug.validChars then acc.push c
- else if c.isWhitespace then acc.push '-'
- else acc ++ mangle c
- loop (String.Legacy.iter str) ""
+def asSlug (str : String) : String := Id.run do
+ let mut iter := str.startPos
+ let mut out := ""
+ while h : iter ≠ str.endPos do
+ let c := iter.get h
+ if c ∈ Slug.validChars then out := out.push c
+ else if c.isWhitespace then out := out.push '-'
+ else out := out ++ mangle c
+ iter := iter.next h
+ return out
/--
A slug is a well-formed string.
@@ -138,12 +138,6 @@ instance : ToString Slug := ⟨Slug.toString⟩
instance : ToJson Slug where
toJson s := ToJson.toJson s.toString
-instance : FromJson Slug where
- fromJson? v := private do
- let s : String ← FromJson.fromJson? v
- if asSlug s = s then pure ⟨s⟩
- else throw s!"String {s} contains invalid characters"
-
namespace Slug
instance : LT Slug where
@@ -163,6 +157,19 @@ instance : DecidableRel (@LE.le Slug _) := fun s1 s2 =>
defmethod String.sluggify (str : String) : Slug :=
⟨asSlug str⟩
+/--
+Returns {lean}`some str` as a slug if it is already a valid slug, or {name}`none` otherwise.
+-/
+def isSlug? (str : String) : Option Slug :=
+ if wf str then some str.sluggify else none
+
+instance : FromJson Slug where
+ fromJson? v := do
+ let s : String ← FromJson.fromJson? v
+ match isSlug? s with
+ | some slug => pure slug
+ | none => throw s!"String {s} contains invalid characters"
+
/--
Appends two slugs by appending their underlying strings.
-/
diff --git a/src/tests/TestMain.lean b/src/tests/TestMain.lean
index 28314873f..44eba9534 100644
--- a/src/tests/TestMain.lean
+++ b/src/tests/TestMain.lean
@@ -163,6 +163,24 @@ def testBlog (_ : Config) : IO Unit := do
if fails > 0 then
throw <| IO.userError s!"{fails} blog tests failed"
+def testRenderedHtml (_ : Config) : IO Unit := do
+ IO.println "Running rendered HTML content format tests..."
+ let fails ← Tests.RenderedHtml.runRenderedHtmlTests
+ if fails > 0 then
+ throw <| IO.userError s!"{fails} rendered HTML content format tests failed"
+
+def testRenderedHtmlExport (_ : Config) : IO Unit := do
+ IO.println "Running rendered HTML content export tests..."
+ let fails ← Tests.RenderedHtmlExport.runRenderedHtmlExportTests
+ if fails > 0 then
+ throw <| IO.userError s!"{fails} rendered HTML content export tests failed"
+
+def testRenderedHtmlMount (_ : Config) : IO Unit := do
+ IO.println "Running rendered HTML content mounting tests..."
+ let fails ← Tests.RenderedHtmlMount.runRenderedHtmlMountTests
+ if fails > 0 then
+ throw <| IO.userError s!"{fails} rendered HTML content mounting tests failed"
+
def testServe (_ : Config) : IO Unit := do
IO.println "Running serve tests..."
let fails ← Verso.Tests.Serve.runServeTests
@@ -363,6 +381,9 @@ def tests := [
testSerialization,
testSearchJs,
testBlog,
+ testRenderedHtml,
+ testRenderedHtmlExport,
+ testRenderedHtmlMount,
testServe,
testStemmer,
testTexOutput "sample-doc" SampleDoc.doc,
diff --git a/src/tests/Tests.lean b/src/tests/Tests.lean
index 5bcdd422c..9b5ca24be 100644
--- a/src/tests/Tests.lean
+++ b/src/tests/Tests.lean
@@ -38,6 +38,9 @@ import Tests.ParserRegression
import Tests.Paths
import Tests.PorterStemmer
import Tests.Refs
+import Tests.RenderedHtml
+import Tests.RenderedHtmlExport
+import Tests.RenderedHtmlMount
import Tests.SearchJs
import Tests.ExtensionResolution
import Tests.Serialization
diff --git a/src/tests/Tests/Arbitrary.lean b/src/tests/Tests/Arbitrary.lean
index bfe69e9a8..9be16145b 100644
--- a/src/tests/Tests/Arbitrary.lean
+++ b/src/tests/Tests/Arbitrary.lean
@@ -11,8 +11,7 @@ import Lean.Data.Json.FromToJson
import all MultiVerso.InternalId
public meta import MultiVerso.NameMap
public meta import MultiVerso
-public meta import VersoManual.Html.JsFile
-public meta import VersoManual.Html.CssFile
+public meta import Verso.Output.Html.Files
public meta import VersoManual.Html.Features
public meta import VersoManual.LicenseInfo
public meta import VersoSearch
@@ -21,13 +20,14 @@ public meta import Verso.Output.Html
public meta import MultiVerso.Manifest
public meta import VersoManual.Basic
import all VersoManual.Basic
-import VersoManual.Html.CssFile
+import Verso.Output.Html.Files
open Lean
open Plausible Gen Arbitrary
open Verso Multi
open Shrinkable
open Std
+open Verso.Output.Html.Files
/-!
This module contains Plausible generators for most of the types that Verso regularly serializes or
diff --git a/src/tests/Tests/Html.lean b/src/tests/Tests/Html.lean
index 515cd0150..102af8de9 100644
--- a/src/tests/Tests/Html.lean
+++ b/src/tests/Tests/Html.lean
@@ -123,3 +123,132 @@ info: |
/-- info: "
}},
+ {{}},
+ {{}},
+ {{![]()
}},
+ {{}},
+ {{}},
+ {{}},
+ {{}},
+ {{"ping"}},
+ {{"kept"}}]
+
+/--
+info: |
+link
+link
+link
+link
+link
+link
+link
+link
+link
+
+
+
+![]()
+
+
+
+
+
+ping
+kept
+-/
+#guard_msgs in
+#eval do
+ IO.println "|"
+ for html in (urlDoc.map <| rewriteUrls ("[" ++ · ++ "]")) do
+ IO.println html.asString
+
+/-! ## Tests for the URL-list attribute parsers -/
+
+private def mark (url : String) : String := "<" ++ url ++ ">"
+
+/--
+Cases for `rewriteSrcset`. A candidate's URL ends at whitespace or a trailing comma, never at a
+comma inside the URL, and every separator, descriptor, and piece of whitespace survives untouched.
+-/
+private def srcsetCases : Array String := #[
+ -- ordinary lists
+ "a.png",
+ "a.png 1x",
+ "a.png 1x, b.png 2x",
+ "a.png 480w, b.png 800w, c.png",
+ -- a URL containing a comma is one URL, because only a trailing comma ends a candidate
+ "a,b.png 1x, c.png",
+ "data:image/png;base64,AAAA 1x",
+ -- commas as the only separator, with no space after them
+ "a.png,b.png",
+ "a.png 1x,b.png 2x",
+ -- odd but legal whitespace and separators
+ " a.png 1x , b.png 2x ",
+ ",,, a.png 1x ,,, b.png 2x ,,,",
+ "\na.png\t1x,\nb.png\t2x\n",
+ -- degenerate inputs
+ "",
+ " ",
+ ",",
+ ",,,",
+ -- a descriptor holding a comma inside parentheses
+ "a.png (min-width, 100px), b.png 2x",
+ -- trailing comma with no candidate after it
+ "a.png 1x,",
+ "a.png,"
+]
+
+/--
+info: |
+"a.png" => ""
+"a.png 1x" => " 1x"
+"a.png 1x, b.png 2x" => " 1x, 2x"
+"a.png 480w, b.png 800w, c.png" => " 480w, 800w, "
+"a,b.png 1x, c.png" => " 1x, "
+"data:image/png;base64,AAAA 1x" => " 1x"
+"a.png,b.png" => ""
+"a.png 1x,b.png 2x" => " 1x, 2x"
+" a.png 1x , b.png 2x " => " 1x , 2x "
+",,, a.png 1x ,,, b.png 2x ,,," => ",,, 1x ,,, 2x ,,,"
+"\na.png\t1x,\nb.png\t2x\n" => "\n\t1x,\n\t2x\n"
+"" => ""
+" " => " "
+"," => ","
+",,," => ",,,"
+"a.png (min-width, 100px), b.png 2x" => " (min-width, 100px), 2x"
+"a.png 1x," => " 1x,"
+"a.png," => ","
+-/
+#guard_msgs in
+ #eval IO.println <| "|\n" ++ String.join
+ (srcsetCases.toList.map fun c => s!"{repr c} => {repr (Html.rewriteSrcset mark c)}\n")
+
+/-- Cases for `rewriteUrlList`, which `ping` uses. -/
+private def urlListCases : Array String :=
+ #["a", "a b", " a b ", "", " ", "\ta\nb\t"]
+
+/--
+info: |
+"a" => ""
+"a b" => " "
+" a b " => " "
+"" => ""
+" " => " "
+"\ta\nb\t" => "\t\n\t"
+-/
+#guard_msgs in
+ #eval IO.println <| "|\n" ++ String.join
+ (urlListCases.toList.map fun c => s!"{repr c} => {repr (Html.rewriteUrlList mark c)}\n")
diff --git a/src/tests/Tests/RenderedHtml.lean b/src/tests/Tests/RenderedHtml.lean
new file mode 100644
index 000000000..3fbf73bef
--- /dev/null
+++ b/src/tests/Tests/RenderedHtml.lean
@@ -0,0 +1,351 @@
+/-
+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 VersoRenderedHtml
+
+public section
+
+open Lean (Json ToJson FromJson toJson fromJson?)
+open Verso Multi RenderedHtml
+
+namespace Tests.RenderedHtml
+
+/-- The hand-written format version 1 directory that guards the format contract. -/
+def fixtureDir : System.FilePath := "test-projects/rendered-html-fixture"
+
+/-- A directory whose page paths have a gap. -/
+def sparseFixtureDir : System.FilePath := "test-projects/rendered-html-sparse-fixture"
+
+/-- A directory whose static files claim page destinations. -/
+def conflictFixtureDir : System.FilePath := "test-projects/rendered-html-conflict-fixture"
+
+private abbrev TestM := StateRefT Nat IO
+
+private def fail (message : String) : TestM Unit := do
+ IO.eprintln s!" FAIL: {message}"
+ modify (· + 1)
+
+private def check (condition : Bool) (message : String) : TestM Unit :=
+ unless condition do fail message
+
+private def checkEq [BEq α] [ToString α] (actual expected : α) (what : String) : TestM Unit :=
+ unless actual == expected do
+ fail s!"{what}: expected '{expected}', got '{actual}'"
+
+private def attempt (act : IO α) : IO (Except String α) := do
+ try
+ return .ok (← act)
+ catch e =>
+ return .error (toString e)
+
+private def mentions (message : String) (fragment : String) : Bool :=
+ (message.find? fragment).isSome
+
+private def expectRejected (what : String) (expected : List String) (forbidden : List String := [])
+ (act : IO α) : TestM Unit := do
+ match ← attempt act with
+ | .ok _ => fail s!"{what} was accepted"
+ | .error message =>
+ for e in expected do
+ unless mentions message e do
+ fail s!"{what} was rejected, but the message did not mention '{e}': {message}"
+ for f in forbidden do
+ if mentions message f then
+ fail s!"{what} was rejected, and the message wrongly mentioned '{f}': {message}"
+
+private def expectAccepted (what : String) (act : IO α) : TestM (Option α) := do
+ match ← attempt act with
+ | .ok v => return some v
+ | .error message =>
+ fail s!"{what} was rejected: {message}"
+ return none
+
+/-- A manifest with fields that this version of Verso does not know, at both levels. -/
+private def manifestWithUnknownFields : String := "
+{\"format\": \"verso-rendered-html\",
+ \"formatVersion\": 1,
+ \"futureField\": {\"anything\": [1, 2, 3]},
+ \"generator\": {\"tool\": \"t\", \"version\": \"v\", \"toolchain\": \"tc\", \"futureField\": 1},
+ \"title\": \"Round Trip\",
+ \"titleHtml\": \"Round Trip\",
+ \"stylesheets\": [{\"path\": \"static/a.css\", \"role\": \"variables\"},
+ {\"path\": \"static/b.css\", \"role\": \"content\"},
+ {\"path\": \"static/c.css\", \"role\": \"someday\"}],
+ \"scripts\": [{\"path\": \"static/a.js\", \"defer\": true,
+ \"provides\": {\"name\": \"katex\", \"version\": \"0.16.22\"}}],
+ \"pages\": {\"\": {\"title\": \"Root\", \"titleHtml\": \"Root\", \"futureField\": 7,
+ \"fragments\": {\"content\": {\"file\": \"fragments/content.html\",
+ \"rootToken\": \"%verso:root%\",
+ \"futureField\": \"x\"}}},
+ \"one\": {\"title\": \"One\", \"titleHtml\": \"One\",
+ \"fragments\": {\"content\": {\"file\": \"fragments/one/content.html\",
+ \"rootToken\": \"%verso:root%\"}}}}}
+"
+
+private def parseManifest (text : String) : IO RenderedHtmlContent := do
+ let json ←
+ match Json.parse text with
+ | .ok json => pure json
+ | .error e => throw <| .userError s!"Failed to parse: {e}"
+ match fromJson? json with
+ | .ok (manifest : RenderedHtmlContent) => pure manifest
+ | .error e => throw <| .userError s!"Failed to read: {e}"
+
+private def testRoundTrip : TestM Unit := do
+ let some manifest ← expectAccepted "A manifest with unknown fields"
+ (parseManifest manifestWithUnknownFields)
+ | return
+ checkEq manifest.title "Round Trip" "The title of the round-tripped manifest"
+ checkEq manifest.pages.size 2 "The page count of the round-tripped manifest"
+ checkEq manifest.stylesheets.size 3 "The stylesheet count of the round-tripped manifest"
+ check (manifest.stylesheets[2]!.role == .other "someday")
+ "An unrecognized stylesheet role is kept"
+ check (!manifest.stylesheets[2]!.role.placesAsVariables)
+ "An unrecognized stylesheet role is placed as content"
+ check (manifest.stylesheets[0]!.role.placesAsVariables)
+ "The variables role is placed ahead of the rest"
+ checkEq manifest.stylesheets[0]!.mountPath "a.css" "The mount path of a stylesheet"
+ checkEq manifest.scripts[0]!.mountPath "a.js" "The mount path of a script"
+ checkEq (manifest.scripts[0]!.provides.map (·.name)) (some "katex")
+ "The library that a script is a copy of"
+ checkEq (manifest.stylesheets[0]!.provides.map (·.name)) none
+ "A stylesheet that is no library names none"
+ let again ← parseManifest (toJson manifest).compress
+ checkEq (toJson again).compress (toJson manifest).compress
+ "Serializing and reading a manifest again is the identity"
+
+/-- A manifest that leaves out every field that carries a default. -/
+private def manifestWithoutOptionalFields : String := "
+{\"format\": \"verso-rendered-html\",
+ \"formatVersion\": 1,
+ \"generator\": {\"tool\": \"t\", \"version\": \"v\", \"toolchain\": \"tc\"},
+ \"title\": \"Sparse\",
+ \"titleHtml\": \"Sparse\"}
+"
+
+private def testOptionalFields : TestM Unit := do
+ let some manifest ← expectAccepted "A manifest that leaves out the fields carrying defaults"
+ (parseManifest manifestWithoutOptionalFields)
+ | return
+ checkEq manifest.stylesheets.size 0 "An absent stylesheet list reads as empty"
+ checkEq manifest.scripts.size 0 "An absent script list reads as empty"
+ checkEq manifest.pages.size 0 "An absent page map reads as empty"
+ -- A field that is present but of the wrong type is still an error.
+ expectRejected "A manifest whose stylesheet list is not a list" [] (act := parseManifest <|
+ "{\"format\": \"verso-rendered-html\", \"formatVersion\": 1,
+ \"generator\": {\"tool\": \"t\", \"version\": \"v\", \"toolchain\": \"tc\"},
+ \"title\": \"T\", \"titleHtml\": \"T\", \"stylesheets\": 7}")
+
+private def testFixture : TestM Unit := do
+ let some loaded ← expectAccepted "The checked-in fixture" (load fixtureDir)
+ | return
+ let manifest := loaded.manifest
+ checkEq manifest.formatVersion 1 "The fixture's format version"
+ checkEq manifest.title "Fixture Content" "The fixture's title"
+ checkEq manifest.titleHtml "Fixture Content" "The fixture's HTML title"
+ let paths := manifest.pages.toArray.map (pathToString ·.fst)
+ checkEq (", ".intercalate paths.toList) ", guide, guide/first, guide/step-1"
+ "The fixture's page paths, in order"
+ check (manifest.stylesheets.any (·.role == .other "decoration"))
+ "The fixture carries a stylesheet with an unrecognized role"
+
+ let some rootPage := manifest.pages[(#[] : Multi.Path)]?
+ | fail "The fixture has no root page"
+ checkEq rootPage.title "Fixture Content" "The fixture root page's title"
+ let some rootFragment := rootPage.fragments["content".sluggify]?
+ | fail "The fixture root page has no content fragment"
+ checkEq rootFragment.rootToken defaultRootToken "The fixture root fragment's token"
+ let rootText ← loaded.readFragment rootFragment "../.."
+ check (mentions rootText "href=\"../../guide/\"")
+ s!"Substituting the fixture root fragment's token: {rootText}"
+ check (mentions rootText "href=\"/\"")
+ "A URL that begins with a slash carries no token"
+ check (!mentions rootText defaultRootToken)
+ "Substitution replaces every occurrence of the token"
+
+ let some deepPage := manifest.pages[(#["guide", "first"] : Multi.Path)]?
+ | fail "The fixture has no page at 'guide/first'"
+ checkEq deepPage.titleHtml "First .isNone) s!"'{bad}' is not a slug"
+ check (bad.sluggify.toString != bad) s!"Sluggifying '{bad}' changes it"
+
+private def sampleOutput : Output where
+ generator := { tool := "verso-tests", version := "1", toolchain := "none" }
+ title := "Written Content"
+ titleHtml := "Written Content"
+ stylesheets := #[{ path := "static/-verso-data/x.css", role := .variables }]
+ scripts := #[{ path := "static/-verso-data/x.js", defer := true }]
+ pages := #[
+ { path := #[], title := "Root", titleHtml := "Root",
+ fragments := #[{
+ name := "content".sluggify, rootToken := defaultRootToken,
+ content := s!""
+ }] },
+ { path := #["one"], title := "One", titleHtml := "One",
+ fragments := #[{
+ name := "content".sluggify, rootToken := defaultRootToken,
+ content := ""
+ }] }
+ ]
+
+private def testWrite : TestM Unit := do
+ IO.FS.withTempDir fun tmp => do
+ let first := tmp / "first"
+ let second := tmp / "second"
+ for dir in [first, second] do
+ IO.FS.createDirAll dir
+ writeStaticFile dir "-verso-data/x.css" (.text ":root { --verso-text-color: black; }\n")
+ writeStaticFile dir "-verso-data/x.js" (.text "// nothing\n")
+ let _ ← expectAccepted "Writing a directory" (write dir sampleOutput)
+ let firstManifest ← IO.FS.readBinFile (manifestFile first)
+ let secondManifest ← IO.FS.readBinFile (manifestFile second)
+ check (firstManifest == secondManifest)
+ "Writing unchanged content twice produces identical manifests"
+ let some loaded ← expectAccepted "A directory that was just written" (load first)
+ | return
+ checkEq loaded.manifest.pages.size 2 "The page count of a directory that was just written"
+
+ let third := tmp / "third"
+ IO.FS.createDirAll third
+ writeStaticFile third "-verso-data/x.js" (.text "// nothing\n")
+ expectRejected "Writing a directory that names a stylesheet it did not write"
+ ["x.css"] (act := write third sampleOutput)
+
+ let fourth := tmp / "fourth"
+ IO.FS.createDirAll fourth
+ writeStaticFile fourth "-verso-data/x.css" (.text ":root {}\n")
+ writeStaticFile fourth "-verso-data/x.js" (.text "// nothing\n")
+ expectRejected "Writing a directory with no pages"
+ ["dense"] (act := write fourth { sampleOutput with pages := #[] })
+
+ IO.FS.withTempDir fun tmp => do
+ let dir := tmp / "conflict"
+ IO.FS.createDirAll dir
+ writeStaticFile dir "index.html" (.text " do
+ let dir := tmp / "chrome"
+ let (_, errors) ← exportSite dir sampleSite chromeTheme
+ check (errors.any (mentions ·.text "page chrome"))
+ s!"A theme whose page template carries chrome is reported: {errors.map (·.text)}"
+
+private def testAdHocChromeIsRejected : TestM Unit := do
+ IO.FS.withTempDir fun tmp => do
+ let dir := tmp / "adhoc"
+ let (_, errors) ← exportSite dir sampleSite overriddenChromeTheme
+ check (errors.any fun e => mentions e.text "page chrome" && mentions e.text "guide")
+ s!"Chrome from a replaced page template is reported: {errors.map (·.text)}"
+
+private def testAssetOrderIsStable : TestM Unit := do
+ let two := Template.hashNamedCss "component" (Std.HashSet.ofList [".a {}", ".b {}"])
+ let three := Template.hashNamedCss "component" (Std.HashSet.ofList [".a {}", ".b {}", ".c {}"])
+ check (two.size == 2 && three.size == 3) "Naming assets by a hash of their contents keeps them all"
+ let kept := three.filter fun css => two.any (·.filename == css.filename)
+ check (kept.map (·.filename) == two.map (·.filename))
+ s!"Adding an asset leaves the order of the others unchanged: {two.map (·.filename)} then {kept.map (·.filename)}"
+
+/-- The URLs that rewriting distinguishes, and what the export makes of each. -/
+private def urlTable : List (String × String) := [
+ ("/x", "/x"),
+ ("./x", "TOKEN/./x"),
+ ("../x", "TOKEN/../x"),
+ ("-verso-data/x", "TOKEN/-verso-data/x"),
+ ("guide/", "TOKEN/guide/"),
+ ("#frag", "#frag"),
+ ("https://x", "https://x"),
+ ("//cdn/x", "//cdn/x"),
+ ("mailto:x", "mailto:x"),
+ ("", "")
+]
+
+private def testUrlTable : TestM Unit := do
+ for (url, expected) in urlTable do
+ let actual := RenderedHtml.relocateUrl "TOKEN" url
+ check (actual == expected) s!"Rewriting '{url}': expected '{expected}', got '{actual}'"
+
+ -- The walk itself leaves `{{← Template.param (α := String) "title"}}
+ {{← Template.builtinHeader}}
+
+
+
+ {{← Template.param "content"}}
+
+
+ }},
+ pageTemplate := do
+ match (← Template.param? (α := Html) "fragments.content") with
+ | some content =>
+ let localNav ←
+ if withLocalNav then
+ pure ((← Template.param? (α := Html) "fragments.localNav").getD .empty)
+ else pure .empty
+ return {{{{localNav}}{{content}} }}
+ | none =>
+ return {{" " " darkPage == between "" " " lightPage)
+ "Re-theming leaves the mounted markup alone"
+ check (mentions darkPage "--verso-text-color: white" &&
+ mentions lightPage "--verso-text-color: black")
+ "Each theme's own custom properties reach the page"
+
+ -- The site's own chrome renders on a page that mounts as it does on a page that does not.
+ let mountingPage ← IO.FS.readFile (dark / "fixture" / "index.html")
+ let plainPage ← IO.FS.readFile (dark / "index.html")
+ check (mentions mountingPage "
x
" -/ #guard_msgs in #eval Html.asString {{"x"
}} (breakLines := false) + +/-! ## Tests for URL rewriting -/ + +private def urlCases : Array String := + #["/x", "./x", "../x", "-verso-data/x", "#frag", "https://x", "//cdn/x", "mailto:x", ""] + +private def urlDoc : Array Html := + urlCases.map (fun u => {{"link"}}) ++ + #[{{}},
+ {{}},
+ {{}},
+ {{
}},
+ {{}},
+ {{}},
+ {{}},
+ {{}},
+ {{"ping"}},
+ {{"kept"}}]
+
+/--
+info: |
+link
+link
+link
+link
+link
+link
+link
+link
+link
+
+
+
+
+
+
+
+
+
+ping
+kept
+-/
+#guard_msgs in
+#eval do
+ IO.println "|"
+ for html in (urlDoc.map <| rewriteUrls ("[" ++ · ++ "]")) do
+ IO.println html.asString
+
+/-! ## Tests for the URL-list attribute parsers -/
+
+private def mark (url : String) : String := "<" ++ url ++ ">"
+
+/--
+Cases for `rewriteSrcset`. A candidate's URL ends at whitespace or a trailing comma, never at a
+comma inside the URL, and every separator, descriptor, and piece of whitespace survives untouched.
+-/
+private def srcsetCases : Array String := #[
+ -- ordinary lists
+ "a.png",
+ "a.png 1x",
+ "a.png 1x, b.png 2x",
+ "a.png 480w, b.png 800w, c.png",
+ -- a URL containing a comma is one URL, because only a trailing comma ends a candidate
+ "a,b.png 1x, c.png",
+ "data:image/png;base64,AAAA 1x",
+ -- commas as the only separator, with no space after them
+ "a.png,b.png",
+ "a.png 1x,b.png 2x",
+ -- odd but legal whitespace and separators
+ " a.png 1x , b.png 2x ",
+ ",,, a.png 1x ,,, b.png 2x ,,,",
+ "\na.png\t1x,\nb.png\t2x\n",
+ -- degenerate inputs
+ "",
+ " ",
+ ",",
+ ",,,",
+ -- a descriptor holding a comma inside parentheses
+ "a.png (min-width, 100px), b.png 2x",
+ -- trailing comma with no candidate after it
+ "a.png 1x,",
+ "a.png,"
+]
+
+/--
+info: |
+"a.png" => "Steps" "The fixture deep page's HTML title"
+ let some deepFragment := deepPage.fragments["content".sluggify]?
+ | fail "The fixture page at 'guide/first' has no content fragment"
+ check (deepFragment.rootToken != defaultRootToken)
+ "A fragment whose prose spells the default token declares a uniquified one"
+ let deepText ← loaded.readFragment deepFragment "../../.."
+ check (mentions deepText defaultRootToken)
+ "Uniquifying a fragment's token leaves the prose that spells the default token alone"
+ check (mentions deepText "href=\"../../../files/example.txt\"")
+ s!"Substituting a uniquified token: {deepText}"
+
+private def testTokens : TestM Unit := do
+ check (hasToken defaultRootToken s!"a {defaultRootToken} b") "A token in the text is found"
+ check (!hasToken defaultRootToken "a b") "A token that is absent is not found"
+ checkEq (chooseToken "nothing to see here") defaultRootToken
+ "Text without the default token gets the default token"
+ let chosen := chooseToken s!"prose that spells {defaultRootToken}"
+ check (chosen != defaultRootToken) "Text with the default token gets a uniquified token"
+ check (!hasToken chosen s!"prose that spells {defaultRootToken}")
+ "The uniquified token does not occur in the text"
+ checkEq (substitute defaultRootToken "x" s!"{defaultRootToken}/a {defaultRootToken}/b")
+ "x/a x/b" "Substitution replaces every occurrence"
+
+private def testRejections : TestM Unit := do
+ expectRejected "A sparse page path set" ["guide"] (act := load sparseFixtureDir)
+ expectRejected "A directory whose static files claim page destinations"
+ ["index.html", "guide"] (forbidden := ["'ab'", "static/ab"])
+ (act := load conflictFixtureDir)
+
+ IO.FS.withTempDir fun tmp => do
+ let dir := tmp / "newer"
+ IO.FS.createDirAll dir
+ IO.FS.writeFile (manifestFile dir)
+ "{\"format\": \"verso-rendered-html\", \"formatVersion\": 99,
+ \"generator\": {\"tool\": \"t\", \"version\": \"v\", \"toolchain\": \"tc\"},
+ \"title\": \"T\", \"titleHtml\": \"T\", \"stylesheets\": [], \"scripts\": [],
+ \"pages\": {}}"
+ expectRejected "A newer format version" ["newer Verso"] (act := load dir)
+
+ IO.FS.withTempDir fun tmp => do
+ let dir := tmp / "missing-asset"
+ IO.FS.createDirAll (dir / "fragments")
+ IO.FS.writeFile (dir / "fragments" / "content.html") "%verso:root%
"
+ IO.FS.writeFile (manifestFile dir)
+ "{\"format\": \"verso-rendered-html\", \"formatVersion\": 1,
+ \"generator\": {\"tool\": \"t\", \"version\": \"v\", \"toolchain\": \"tc\"},
+ \"title\": \"T\", \"titleHtml\": \"T\",
+ \"stylesheets\": [{\"path\": \"static/gone.css\", \"role\": \"content\"}],
+ \"pages\": {\"\": {\"title\": \"T\", \"titleHtml\": \"T\",
+ \"fragments\": {\"content\": {\"file\": \"fragments/content.html\",
+ \"rootToken\": \"%verso:root%\"}}}}}"
+ expectRejected "A stylesheet that is not there" ["static/gone.css"] (act := load dir)
+
+ IO.FS.withTempDir fun tmp => do
+ let dir := tmp / "no-pages"
+ IO.FS.createDirAll dir
+ IO.FS.writeFile (manifestFile dir)
+ "{\"format\": \"verso-rendered-html\", \"formatVersion\": 1,
+ \"generator\": {\"tool\": \"t\", \"version\": \"v\", \"toolchain\": \"tc\"},
+ \"title\": \"T\", \"titleHtml\": \"T\", \"pages\": {}}"
+ expectRejected "A manifest with no pages" ["dense"] (act := load dir)
+
+ for (what, path) in [("absolute", "/etc/passwd"), ("dotted", "fragments/../../secret.html")] do
+ IO.FS.withTempDir fun tmp => do
+ let dir := tmp / what
+ IO.FS.createDirAll dir
+ IO.FS.writeFile (manifestFile dir) <|
+ "{\"format\": \"verso-rendered-html\", \"formatVersion\": 1,
+ \"generator\": {\"tool\": \"t\", \"version\": \"v\", \"toolchain\": \"tc\"},
+ \"title\": \"T\", \"titleHtml\": \"T\", \"stylesheets\": [], \"scripts\": [],
+ \"pages\": {\"\": {\"title\": \"T\", \"titleHtml\": \"T\",
+ \"fragments\": {\"content\": {\"file\": \"" ++ path ++
+ "\", \"rootToken\": \"%verso:root%\"}}}}}"
+ expectRejected s!"A fragment file with an {what} path" [path] (act := load dir)
+
+ for badPath in ["a/b c", "a//b", "a/./b", "a/../b"] do
+ expectRejected s!"A page path '{badPath}'" [] (act := parseManifest <|
+ "{\"format\": \"verso-rendered-html\", \"formatVersion\": 1,
+ \"generator\": {\"tool\": \"t\", \"version\": \"v\", \"toolchain\": \"tc\"},
+ \"title\": \"T\", \"titleHtml\": \"T\", \"stylesheets\": [], \"scripts\": [],
+ \"pages\": {\"" ++ badPath ++
+ "\": {\"title\": \"T\", \"titleHtml\": \"T\", \"fragments\": {}}}}")
+
+private def testSlugs : TestM Unit := do
+ for good in ["abc", "a-b_c", "ABC123", "-", "_"] do
+ check (Slug.isSlug? good |>.isSome) s!"'{good}' is a slug"
+ for bad in ["a b", "a.b", "a/b", "aOne.
Claims the root page's destination.
\n") + writeStaticFile dir "-verso-data/x.css" (.text ":root { }\n") + writeStaticFile dir "-verso-data/x.js" (.text "// nothing\n") + expectRejected "Writing a directory whose static files claim a page destination" + ["index.html"] (act := write dir sampleOutput) + + IO.FS.withTempDir fun tmp => do + let dir := tmp / "sparse" + IO.FS.createDirAll dir + expectRejected "Writing a sparse page path set" ["deep"] (act := write dir { sampleOutput with + pages := #[ + { path := #[], title := "Root", titleHtml := "Root", fragments := #[] }, + { path := #["deep", "page"], title := "Deep", titleHtml := "Deep", fragments := #[] } + ] }) + + IO.FS.withTempDir fun tmp => do + let dir := tmp / "asset" + IO.FS.createDirAll dir + expectRejected "Writing an asset path outside the static directory" ["elsewhere"] + (act := write dir { sampleOutput with + stylesheets := #[{ path := "elsewhere/x.css", role := .content }] }) + +/-- +Runs the rendered HTML content format tests, returning the number of failures. +-/ +def runRenderedHtmlTests : IO Nat := do + let ((), failures) ← + (do + testRoundTrip + testOptionalFields + testFixture + testTokens + testRejections + testSlugs + testWrite : TestM Unit).run 0 + return failures + +end Tests.RenderedHtml diff --git a/src/tests/Tests/RenderedHtmlExport.lean b/src/tests/Tests/RenderedHtmlExport.lean new file mode 100644 index 000000000..ef84d4a22 --- /dev/null +++ b/src/tests/Tests/RenderedHtmlExport.lean @@ -0,0 +1,244 @@ +/- +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 VersoBlog +public import VersoRenderedHtml + +public section + +open Lean +open Verso Genre Blog +open Verso.Output (Html) +open Verso.Output.Html +open Verso.RenderedHtml (load manifestFile staticDir) + +namespace Tests.RenderedHtmlExport + +private abbrev TestM := StateRefT Nat IO + +private def fail (message : String) : TestM Unit := do + IO.eprintln s!" FAIL: {message}" + modify (· + 1) + +private def check (condition : Bool) (message : String) : TestM Unit := + unless condition do fail message + +private def mentions (text : String) (fragment : String) : Bool := + (text.find? fragment).isSome + +/-- A logger that accumulates messages without printing them. -/ +def quietLogger : IO (Verso.Logger IO) := do + let errorsRef ← IO.mkRef #[] + let warningsRef ← IO.mkRef #[] + return { + log severity text loc := do + let msg : Verso.LogMessage := { severity, text, loc } + match severity with + | .error => errorsRef.modify (·.push msg) + | .warning => warningsRef.modify (·.push msg) + errors := errorsRef.get + warnings := warningsRef.get + } + +/-- A part with a plain-text title. -/ +def part (title : String) (content : Array (Verso.Doc.Block Page)) + (subParts : Array (Verso.Doc.Part Page) := #[]) : Verso.Doc.Part Page := + Verso.Doc.Part.mk #[Verso.Doc.Inline.text title] title none content subParts + +/-- A site whose links cover the cases that URL rewriting distinguishes. -/ +def sampleSite : Site := + .page `sample + (part "Sample Content" #[ + Verso.Doc.Block.para #[ + .link #[.text "the guide"] "guide/", .text " ", + .link #[.text "elsewhere"] "https://lean-lang.org", .text " ", + .link #[.text "the serving site"] "/", .text " ", + .link #[.text "mail"] "mailto:nobody@example.com", .text " ", + .math .inline "x^2"]]) + #[.page "guide" `sample.guide + (part "The Guide" #[Verso.Doc.Block.para #[.text "Guide text."]]) #[]] + +/-- A theme with a stylesheet of its own. -/ +def sampleTheme : Theme := + { Theme.default with + cssFiles := #[ + { filename := "sample.css", + contents := ".sample { color: var(--verso-text-color); }\n" }] } + +/-- A theme whose page template carries page chrome. -/ +def chromeTheme : Theme := + { Theme.default with + pageTemplate := do + return {{"Chrome where a fragment belongs."
}} } + +/-- A theme whose page template is replaced, for one path, by one that carries page chrome. -/ +def overriddenChromeTheme : Theme := + sampleTheme.override #["guide"] + ⟨(do return {{"Chrome from an ad hoc template."
}}), id⟩ + +/-- A site whose title needs an element that a title may not hold. -/ +def imageTitleSite : Site := + .page `image + (Verso.Doc.Part.mk #[Verso.Doc.Inline.image "alt" "picture.png"] "A picture" none #[] #[]) + #[] + +private def exportOptions : RenderedHtmlOptions where + generator := { tool := "verso-tests", version := "1", toolchain := "none" } + +/-- +Exports a site to `dir`, returning the manifest and the errors that were reported. +-/ +def exportSite (dir : System.FilePath) (site : Site) (theme : Theme := sampleTheme) : + IO (Verso.RenderedHtmlContent × Array Verso.LogMessage) := do + let logger ← quietLogger + let cfg : Config := {} + let wrapper := exportOptions.wrapperClass site + let (site, xref) ← site.traverse cfg {} |>.run logger + let ctxt : Generate.Context := { + theme, site, + ctxt := { path := .root, config := cfg, components := {} }, + xref, dir, config := cfg, header := Html.doctype, + linkTargets := {}, components := {} + } + let (((manifest, _), _)) ← + Site.writeRenderedHtml dir theme site exportOptions wrapper |>.run ctxt .empty {} |>.run logger + return (manifest, ← logger.errors) + +private def testExport : TestM Unit := do + IO.FS.withTempDir fun tmp => do + let first := tmp / "first" + let second := tmp / "second" + let (manifest, errors) ← exportSite first sampleSite + check errors.isEmpty s!"Exporting a site reported errors: {errors.map (·.text)}" + check (manifest.pages.size == 2) s!"An exported site has 2 pages, got {manifest.pages.size}" + check (manifest.title == "Sample Content") s!"The exported title is '{manifest.title}'" + check (manifest.stylesheets[0]!.role == .variables) + "The variables stylesheet comes first" + check (manifest.stylesheets.any (·.path.endsWith "verso-vars.css")) + "An exported directory ships the custom property definitions" + check (manifest.scripts.any (·.path.endsWith "math.js")) + "An exported directory ships the math script" + + let some loaded ← (do + try + return some (← load first) + catch e => + fail s!"An exported directory did not load: {e}" + return none) + | return + let some rootPage := loaded.manifest.pages[(#[] : Multi.Path)]? + | fail "An exported directory has no root page" + let some fragment := rootPage.fragments["content".sluggify]? + | fail "An exported page has no content fragment" + let text ← loaded.readFragmentText fragment + check (mentions text s!"class=\"verso-content content verso-content-") + s!"A fragment is wrapped: {text}" + check (mentions text "data-verso-docs=") + s!"The content fragment names its hover data: {text}" + check (mentions text s!"href=\"{fragment.rootToken}/guide/\"") + s!"A site-relative URL becomes relative to the token: {text}" + check (mentions text "href=\"https://lean-lang.org\"") + s!"An absolute URL is left alone: {text}" + check (mentions text "href=\"/\"") + s!"A root-relative URL is left alone: {text}" + check (mentions text "href=\"mailto:nobody@example.com\"") + s!"A URL with a scheme is left alone: {text}" + check (!mentions text "