From 112fd7dfc74bd1dc16aa07fd5f37d619ca9a56a9 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Tue, 18 Aug 2026 15:17:52 +0200 Subject: [PATCH 1/7] feat: static content archives This allows tutorials to export static content archives, and websites to consume them. These static archives contain the content of Verso pages, but not the surrounding site structure, allowing them to be incorporated in other sites without requiring the re-generation of old content when the site structure changes. --- .github/workflows/ci.yml | 29 ++ .gitignore | 5 + .../mount-site/test_mounted_content.py | 57 +++ doc/UsersGuide/Basic.lean | 3 + doc/UsersGuide/Output/HTML.lean | 6 +- doc/UsersGuide/Releases/Entries.lean | 1 + .../Releases/Entries/RenderedHtmlContent.lean | 52 +++ doc/UsersGuide/RenderedHtml.lean | 315 +++++++++++++++ doc/UsersGuide/Websites.lean | 20 + lakefile.lean | 22 + scripts/check-url-prefix.sh | 85 ++++ src/multi-verso/MultiVerso/Slug.lean | 39 +- src/tests/TestMain.lean | 21 + src/tests/Tests.lean | 3 + src/tests/Tests/Arbitrary.lean | 6 +- src/tests/Tests/Html.lean | 129 ++++++ src/tests/Tests/RenderedHtml.lean | 351 ++++++++++++++++ src/tests/Tests/RenderedHtmlExport.lean | 244 +++++++++++ src/tests/Tests/RenderedHtmlMount.lean | 266 ++++++++++++ src/tests/Tests/Serialization.lean | 6 +- src/verso-blog/VersoBlog.lean | 27 +- src/verso-blog/VersoBlog/Basic.lean | 24 +- src/verso-blog/VersoBlog/Generate.lean | 148 +++++-- .../VersoBlog/RenderedHtml/Export.lean | 378 ++++++++++++++++++ src/verso-blog/VersoBlog/Site.lean | 149 +++++++ src/verso-blog/VersoBlog/Site/Syntax.lean | 33 ++ src/verso-blog/VersoBlog/Template.lean | 186 +++++++-- src/verso-blog/VersoBlog/Theme.lean | 78 +++- src/verso-blog/VersoBlog/Traverse.lean | 65 +-- src/verso-html/VersoHtmlMain.lean | 4 +- src/verso-literate-html/LiterateHtmlMain.lean | 6 +- src/verso-manual/VersoManual.lean | 16 +- src/verso-manual/VersoManual/Basic.lean | 1 + src/verso-manual/VersoManual/Docstring.lean | 14 +- .../VersoManual/HighlightedCode.lean | 3 +- src/verso-manual/VersoManual/Html.lean | 23 +- src/verso-manual/VersoManual/Html/Basic.lean | 79 ---- src/verso-manual/VersoManual/Html/Config.lean | 2 +- .../VersoManual/Html/CssFile.lean | 28 -- .../VersoManual/Html/Features.lean | 6 +- src/verso-manual/VersoManual/Html/JsFile.lean | 42 -- src/verso-manual/VersoManual/Index.lean | 8 +- .../VersoRenderedHtml.lean | 11 + .../VersoRenderedHtml/Format.lean | 360 +++++++++++++++++ .../VersoRenderedHtml/Read.lean | 227 +++++++++++ .../VersoRenderedHtml/Tokens.lean | 54 +++ .../VersoRenderedHtml/Write.lean | 178 +++++++++ src/verso-tutorial/VersoTutorial.lean | 236 ++++++++--- src/verso/Verso/Code/Highlighted.lean | 81 ++-- .../Verso/Code/Highlighted/WebAssets.lean | 9 + src/verso/Verso/Output/Html.lean | 118 ++++++ src/verso/Verso/Output/Html/Files.lean | 154 +++++++ src/verso/Verso/Output/Html/KaTeX.lean | 14 +- src/verso/Verso/Output/Html/Wrappers.lean | 21 + static-web/math.js | 27 +- test-projects/mount-site/MountSite.lean | 9 + test-projects/mount-site/MountSite/Front.lean | 33 ++ .../mount-site/MountSite/Guides.lean | 13 + .../mount-site/MountSite/Tutorials.lean | 14 + test-projects/mount-site/MountSiteMain.lean | 154 +++++++ .../mount-site/static_files/style.css | 26 ++ .../fragments/abc/content.html | 3 + .../fragments/content.html | 3 + .../fragments/guide/content.html | 3 + .../fragments/guide/first/content.html | 3 + .../rendered-html-conflict-fixture/static/ab | 1 + .../static/guide | 1 + .../static/index.html | 1 + .../verso-rendered-html.json | 23 ++ .../fragments/content.html | 9 + .../fragments/guide/content.html | 4 + .../fragments/guide/first/content.html | 4 + .../fragments/guide/localNav.html | 8 + .../fragments/guide/step-1/content.html | 3 + .../static/-verso-data/fixture-docs.json | 1 + .../static/-verso-data/fixture-extra.css | 3 + .../static/-verso-data/fixture-vars.css | 5 + .../static/-verso-data/fixture.css | 8 + .../static/-verso-data/fixture.js | 9 + .../static/files/example.txt | 1 + .../verso-rendered-html.json | 29 ++ .../fragments/content.html | 3 + .../fragments/guide/first/content.html | 3 + .../verso-rendered-html.json | 15 + .../TutorialExample/HashMap.lean | 2 +- .../tutorial-test/TutorialExample/Site.lean | 34 ++ .../tutorial-test/TutorialExampleMain.lean | 27 +- .../TutorialRenderedHtmlMain.lean | 11 + 88 files changed, 4464 insertions(+), 472 deletions(-) create mode 100644 browser-tests/mount-site/test_mounted_content.py create mode 100644 doc/UsersGuide/Releases/Entries/RenderedHtmlContent.lean create mode 100644 doc/UsersGuide/RenderedHtml.lean create mode 100755 scripts/check-url-prefix.sh create mode 100644 src/tests/Tests/RenderedHtml.lean create mode 100644 src/tests/Tests/RenderedHtmlExport.lean create mode 100644 src/tests/Tests/RenderedHtmlMount.lean create mode 100644 src/verso-blog/VersoBlog/RenderedHtml/Export.lean delete mode 100644 src/verso-manual/VersoManual/Html/Basic.lean delete mode 100644 src/verso-manual/VersoManual/Html/CssFile.lean delete mode 100644 src/verso-manual/VersoManual/Html/JsFile.lean create mode 100644 src/verso-rendered-html/VersoRenderedHtml.lean create mode 100644 src/verso-rendered-html/VersoRenderedHtml/Format.lean create mode 100644 src/verso-rendered-html/VersoRenderedHtml/Read.lean create mode 100644 src/verso-rendered-html/VersoRenderedHtml/Tokens.lean create mode 100644 src/verso-rendered-html/VersoRenderedHtml/Write.lean create mode 100644 src/verso/Verso/Output/Html/Files.lean create mode 100644 src/verso/Verso/Output/Html/Wrappers.lean create mode 100644 test-projects/mount-site/MountSite.lean create mode 100644 test-projects/mount-site/MountSite/Front.lean create mode 100644 test-projects/mount-site/MountSite/Guides.lean create mode 100644 test-projects/mount-site/MountSite/Tutorials.lean create mode 100644 test-projects/mount-site/MountSiteMain.lean create mode 100644 test-projects/mount-site/static_files/style.css create mode 100644 test-projects/rendered-html-conflict-fixture/fragments/abc/content.html create mode 100644 test-projects/rendered-html-conflict-fixture/fragments/content.html create mode 100644 test-projects/rendered-html-conflict-fixture/fragments/guide/content.html create mode 100644 test-projects/rendered-html-conflict-fixture/fragments/guide/first/content.html create mode 100644 test-projects/rendered-html-conflict-fixture/static/ab create mode 100644 test-projects/rendered-html-conflict-fixture/static/guide create mode 100644 test-projects/rendered-html-conflict-fixture/static/index.html create mode 100644 test-projects/rendered-html-conflict-fixture/verso-rendered-html.json create mode 100644 test-projects/rendered-html-fixture/fragments/content.html create mode 100644 test-projects/rendered-html-fixture/fragments/guide/content.html create mode 100644 test-projects/rendered-html-fixture/fragments/guide/first/content.html create mode 100644 test-projects/rendered-html-fixture/fragments/guide/localNav.html create mode 100644 test-projects/rendered-html-fixture/fragments/guide/step-1/content.html create mode 100644 test-projects/rendered-html-fixture/static/-verso-data/fixture-docs.json create mode 100644 test-projects/rendered-html-fixture/static/-verso-data/fixture-extra.css create mode 100644 test-projects/rendered-html-fixture/static/-verso-data/fixture-vars.css create mode 100644 test-projects/rendered-html-fixture/static/-verso-data/fixture.css create mode 100644 test-projects/rendered-html-fixture/static/-verso-data/fixture.js create mode 100644 test-projects/rendered-html-fixture/static/files/example.txt create mode 100644 test-projects/rendered-html-fixture/verso-rendered-html.json create mode 100644 test-projects/rendered-html-sparse-fixture/fragments/content.html create mode 100644 test-projects/rendered-html-sparse-fixture/fragments/guide/first/content.html create mode 100644 test-projects/rendered-html-sparse-fixture/verso-rendered-html.json create mode 100644 test-projects/tutorial-test/TutorialExample/Site.lean create mode 100644 test-projects/tutorial-test/TutorialRenderedHtmlMain.lean diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index d68f78520..9aa1c6c75 100644 --- a/.github/workflows/ci.yml +++ b/.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. diff --git a/.gitignore b/.gitignore index 88efe9519..ebf56d547 100644 --- a/.gitignore +++ b/.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 diff --git a/browser-tests/mount-site/test_mounted_content.py b/browser-tests/mount-site/test_mounted_content.py new file mode 100644 index 000000000..e11d8a1bf --- /dev/null +++ b/browser-tests/mount-site/test_mounted_content.py @@ -0,0 +1,57 @@ +"""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) diff --git a/doc/UsersGuide/Basic.lean b/doc/UsersGuide/Basic.lean index b22cab944..6f20ba549 100644 --- a/doc/UsersGuide/Basic.lean +++ b/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} diff --git a/doc/UsersGuide/Output/HTML.lean b/doc/UsersGuide/Output/HTML.lean index adb7d31ec..8943cc427 100644 --- a/doc/UsersGuide/Output/HTML.lean +++ b/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 `\frac{1}{2}`. 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} diff --git a/doc/UsersGuide/Releases/Entries.lean b/doc/UsersGuide/Releases/Entries.lean index d2dd7cd0d..f1a887760 100644 --- a/doc/UsersGuide/Releases/Entries.lean +++ b/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 diff --git a/doc/UsersGuide/Releases/Entries/RenderedHtmlContent.lean b/doc/UsersGuide/Releases/Entries/RenderedHtmlContent.lean new file mode 100644 index 000000000..55f502998 --- /dev/null +++ b/doc/UsersGuide/Releases/Entries/RenderedHtmlContent.lean @@ -0,0 +1,52 @@ +/- +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 + +open Verso.Genre Manual InlineLean UsersGuide.Releases + +release_note + version := ⟨4, 34, 0⟩ + breaking := true + tag := "rendered-html-content" + prs := [] + +#doc (Manual) "Rendered HTML Content" => + +A site can now emit its pages as a directory of rendered HTML content, and another site can mount that directory and render it with its own theme. + +A directory of rendered HTML content holds page bodies, head requirements, and assets, with no page chrome. +Documentation that is authored in one repository, deployed from another, and kept online for every released version can therefore be themed from one place: a rebuilt site picks up the current navigation bar and colors for content that was built long ago and is never rebuilt. + +`Site.toRenderedHtml` and `Site.writeRenderedHtml` produce a directory, `tutorialsRenderedHtmlMain` produces one from a set of tutorials, and the `mount` form of the site configuration language mounts one. +`Site.resolveMounts` reads the manifest of every mount, and `Site.insertMount` inserts a mount from an assembly function that runs in `IO`. + +Several changes reach every site rather than only mounted content: + +* 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. +* 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 carries the scripts of several Verso releases without any of them reaching each other's markup. The math script marks what it has rendered. +* KaTeX and `marked` are served from the site itself rather than from a CDN, so a page depends on nothing on the network. This adds roughly a megabyte of KaTeX fonts to every website. +* 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 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 change: the types that describe a genre's stylesheets and scripts now live in `Verso.Output.Html`, where every genre that emits HTML can reach them. +`CSS`, `JS`, `StaticCssFile`, `CssFile`, `StaticJsFile`, `JsSourceMap`, and `JsFile` moved there from `Verso.Genre.Manual`, and the modules `VersoManual.Html.Basic`, `VersoManual.Html.CssFile`, and `VersoManual.Html.JsFile` were replaced by `Verso.Output.Html.Files`. +Code that named these through the manual genre opens `Verso.Output.Html` instead. +The website genre orders its scripts with `Verso.Output.Html.sortByAfter`, so it honors the `after` field that until now only the manual genre respected, and it places `highlighting.js` after `popper.js` and `tippy.js`. +That sort now takes the leftmost script whose named files are already placed, so a script that names nothing keeps the position it had. + +Breaking change: `Blog.Theme.cssFiles` and `Blog.Theme.jsFiles` hold `CssFile` and `JsFile` rather than tuples, as do `Blog.TraverseState.cssFiles` and `Blog.TraverseState.jsFiles`. +A theme that wrote `cssFiles := #[("x.css", contents)]` writes `cssFiles := #[{filename := "x.css", contents}]`, and a script can now carry `after` and `defer`. + +Breaking change: the `path` parameter that the website genre passes to the `post` and `archiveEntry` templates is a link, ending in `/`, so a template appends a name to it directly. +`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. + +Breaking change: a theme invokes `Blog.Template.builtinHeader` before defining its own custom properties, so that its definitions override the ones that the header emits. +`Blog.Theme.default` has been changed accordingly. +`Verso.Genre.Blog.Traverse.renderMathJs` has been replaced by `Verso.Output.Html.mathJs`, and `Verso.Output.Html.math.js` by the same function. +`mathJs` and `Verso.Code.highlightingJs` take the selector for the elements their script belongs to, which is `"body"` for a whole page. diff --git a/doc/UsersGuide/RenderedHtml.lean b/doc/UsersGuide/RenderedHtml.lean new file mode 100644 index 000000000..759e8eda5 --- /dev/null +++ b/doc/UsersGuide/RenderedHtml.lean @@ -0,0 +1,315 @@ +/- +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 +-/ +import Lean.DocString.Syntax +import VersoManual +import VersoBlog +import VersoRenderedHtml +import VersoTutorial + +open Verso Genre Manual + +open Verso.Genre.Blog (Page Post) + +open InlineLean +open Verso.Doc + +#doc (Manual) "Rendered HTML Content" => +%%% +tag := "rendered-html" +htmlSplit := .never +%%% + +To make it easier to combine documents written in multiple genres, as well as to host historical content such as prior versions of documentation, Verso provides a format for pre-rendered HTML snippets with their associated CSS and JavaScript that can be incorporated into another document. +In particular, this archived content can be placed into the URL hierarchy and site design {ref "website"}[of a Verso-based website]. +Pre-rendered content is saved in a directory with a specific structure. +Within a Verso-based website, it can be {deftech}[mounted] at a specific path in the site. + +For each page, pre-rendered content provides a set of named {deftech}[fragments] of HTML. +The site in which the content is displayed should place these fragments in the proper places for its design. + +# The Directory +%%% +tag := "rendered-html-directory" +%%% + +:::paragraph +Saved rendered content is in a directory with the following contents: + +: `verso-rendered-html.json` + + This manifest maps page paths to their titles and HTML fragments, and it lists the stylesheets and scripts that the pages need. + +: `fragments/` + + This directory contains the HTML fragments that the manifest references. + +: `static/` + + This directory contains files that are referenced from the fragments, to be served as-is. +::: + + +A consumer copies the static directory to its mount point, so, for example, `static/images/screenshot.png` is served at the +mount point followed by `images/screenshot.png`. +It also renders one page per manifest entry. + +The static directory includes Verso's CSS and JavaScript along with bundled versions of third-party dependencies, so pages continue to render correctly as Verso changes. +The scripts are confined to the content's own markup, so a page may carry the scripts of several Verso releases alongside those of the consuming site. + +{docstring Verso.RenderedHtmlContent} + +{docstring Verso.RenderedHtmlContent.Page} + +{docstring Verso.RenderedHtmlContent.Fragment} + +{docstring Verso.RenderedHtmlContent.Generator} + +{docstring Verso.RenderedHtmlContent.Stylesheet} + +{docstring Verso.RenderedHtmlContent.Stylesheet.mountPath} + +{docstring Verso.RenderedHtmlContent.StylesheetRole} + +{docstring Verso.RenderedHtmlContent.Script} + +{docstring Verso.RenderedHtmlContent.Library} + +{docstring Verso.RenderedHtmlContent.Script.mountPath} + +# Page Paths +%%% +tag := "rendered-html-page-paths" +%%% + +Page paths are {deftech}_dense_: every proper prefix of a page path is itself a page path, so a directory +always has an index and the root page is always present. +A page keyed `a/b` is served at `a/b/` under the mount point. + +{docstring Verso.RenderedHtml.pathToString} + +{docstring Verso.RenderedHtml.pathOfString} + +{docstring Verso.RenderedHtml.checkDense} + +{docstring Verso.RenderedHtml.checkDestinations} + +# Fragments +%%% +tag := "rendered-html-fragments" +%%% + +Fragments are separate files, and the consuming template places the ones that it knows by name, so neither the producer nor the consumer parses HTML. +Every fragment belongs in the document body. +A fragment that the template does not reference is not rendered, and a consumer should warn about any fragments that it does not place. + +:::paragraph +Every fragment is wrapped in a `
` with the following classes: + * `verso-content` + * The fragment's name + * The wrapper identifier that the content's scripts use to target their effects + +For example: +``` +
+ ... +
+``` + +`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 ``, ``, ``, ``, or page navigation features. + Fragments reach a consumer as text, so a consumer relies on this without checking it. + +* A title contains only text nodes and the following tags: `em`, `strong`, `code`, `sub`, `sup`, `span` and `br`. + Additionally, it contains no URLs. + This makes it safe to be emitted in a heading, link, or list item without being rewritten. + The title is the one piece of content that a consumer renders on pages other than the content's own, where the content's stylesheets and scripts are absent. + +* A fragment's declared token is the only token in its text, and no further substitutions are expected. + Files under the static directory are served verbatim and are never substituted, so nothing in them refers to a path outside the static + directory, CSS `url()` included. + +* Verso's content stylesheets read `--verso-*` custom properties and hardcode no colors or fonts, and the content ships its own definitions of those properties on `:root`. + Third-party stylesheets that ship alongside, KaTeX in particular, may set their own colors and fonts. + +* A `--verso-*` property keeps its meaning across Verso releases. + +* A page keyed `a/b` is served at `a/b/` under the mount point, and `static/foo` at `foo`. + Conflicts are with respect to the tree that the mount writes, so they involve nothing outside the directory. + +* Pages depend on nothing outside the static directory and nothing on the network. + +* The format describes one directory. + How directories are named, where they are found, and what order a site presents them in are decisions of the consumer. + +# Producing a Directory +%%% +tag := "rendered-html-producing" +%%% + +{docstring Verso.Genre.Blog.Site.toRenderedHtml} + +{docstring Verso.Genre.Blog.Site.writeRenderedHtml} + +{docstring Verso.Genre.Blog.RenderedHtmlOptions} + +{docstring Verso.Genre.Blog.RenderedHtmlOptions.wrapperClass} + +{docstring Verso.Genre.Tutorial.tutorialsRenderedHtmlMain} + +A producer that writes files into the static directory itself uses these: + +{docstring Verso.RenderedHtml.write} + +{docstring Verso.RenderedHtml.writeStaticFile} + +{docstring Verso.RenderedHtml.Output} + +{docstring Verso.RenderedHtml.OutputPage} + +{docstring Verso.RenderedHtml.OutputFragment} + +# Mounting a Directory +%%% +tag := "rendered-html-mounting" +%%% + +In the {ref "website"}[website genre], a site mounts a directory with the `mount` form of the site configuration language. +For example, this site mounds a content directory under `/page/` and another under `/guides/archive/`: +```lean -show +open Verso.Genre.Blog Site Syntax +opaque MySite.Front : Part Page +opaque MySite.Guides : Part Page +``` +```lean +def mountingSite : Site := site MySite.Front / + mount "page" ← "path/to/content" + "guides" MySite.Guides / + mount "archive" ← "path/to/older/content" with { + showInNav := false + } +``` + +A mount may appear wherever a directory may: beneath any page, whether at the top level of the site or nested. + +{docstring Verso.Genre.Blog.MountSettings} + +{docstring Verso.Genre.Blog.Site.resolveMounts} + +{docstring Verso.Genre.Blog.Site.insertDir} + +{docstring Verso.Genre.Blog.Site.insertMount} + +{docstring Verso.Genre.Blog.Dir.mount?} + +{docstring Verso.RenderedHtml.load} + +{docstring Verso.RenderedHtml.Loaded} + +Page IDs are namespaced by the mount, because a site that mounts several versions of the same content holds every internal page path once per version. +An author links to a mounted page with the `page_link` role, writing the segments that are not valid Lean identifier components in guillemets, as in `{page_link tutorials.«getting-started»}`. + +{docstring Verso.Genre.Blog.mountPageId} + +A mount's fragments are provided to the site's template as ordinary template parameters, prefixed by {lean}`"fragments."`. +A per-path override may be used if a special template is required. +The main content of the page is in the `content` fragment, as the parameter `fragments.content`. +{name Verso.Genre.Blog.Template.builtinHeader}`builtinHeader` places the stylesheets and scripts of a mount in the ``. +All themes should use this; if they do, no further support is required in the `` element. diff --git a/doc/UsersGuide/Websites.lean b/doc/UsersGuide/Websites.lean index 116214076..23e4c5902 100644 --- a/doc/UsersGuide/Websites.lean +++ b/doc/UsersGuide/Websites.lean @@ -61,12 +61,32 @@ The URL layout of a site is specified via a {name Blog.Site}`Site`: {docstring Blog.Dir} These are usually constructed using a small embedded configuration language. +A page is written as its URL segment followed by the name of the document that it renders, further +pages are indented beneath a `/`, a blog is introduced by `with`, a directory of files that are +served verbatim by `static`, and a directory of {ref "rendered-html"}[rendered HTML content] by +`mount`: + +``` +def mySite : Site := site MySite.Front / + static "static" ← "static_files" + "about" MySite.About + "blog" MySite.Blog with + MySite.Blog.FirstPost + "tutorials" MySite.Tutorials / + mount "v1" ← "content/v1" + mount "v0" ← "content/v0" with {showInNav := false} +``` + +The settings after `with` in a `mount` form are a {name Blog.MountSettings}`MountSettings`. A blog is rendered using a theme, which is a collection of templates. Templates are monadic functions that construct {name Verso.Output.Html}`Html` from a set of dynamically-typed parameters. {docstring Blog.Theme} +A theme that is used to produce {ref "rendered-html"}[rendered HTML content] keeps its chrome in its +primary template, because the export renders the page template alone. + {docstring Blog.Template} {docstring Blog.TemplateM} diff --git a/lakefile.lean b/lakefile.lean index ade9bbabd..da9f31ba6 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -39,6 +39,11 @@ lean_lib VersoSearch where -- Rebuild search when JS on disk changes needs := #[staticWeb] +@[default_target] +lean_lib VersoRenderedHtml where + srcDir := "src/verso-rendered-html" + roots := #[`VersoRenderedHtml] + @[default_target] lean_lib VersoBlog where srcDir := "src/verso-blog" @@ -215,6 +220,23 @@ lean_exe «tutorial-example» where root := `TutorialExampleMain supportInterpreter := true +-- A site that mounts directories of rendered HTML content and renders them with its own theme +lean_lib MountSite where + srcDir := "test-projects/mount-site" + roots := #[`MountSite] + +@[default_target] +lean_exe «mount-site» where + srcDir := "test-projects/mount-site" + root := `MountSiteMain + supportInterpreter := true + +@[default_target] +lean_exe «tutorial-example-rendered-html» where + srcDir := "test-projects/tutorial-test" + root := `TutorialRenderedHtmlMain + supportInterpreter := true + private def leanOptionArgs (m : Module) : Array String := Id.run do let opts := Module.leanOptions m let vals := Lean.LeanOptions.values opts diff --git a/scripts/check-url-prefix.sh b/scripts/check-url-prefix.sh new file mode 100755 index 000000000..ca83847ae --- /dev/null +++ b/scripts/check-url-prefix.sh @@ -0,0 +1,85 @@ +#!/usr/bin/env bash +# +# Copies a generated site under a URL prefix, rejects the URLs that break there, and link-checks the +# copy. +# +# A site is served from wherever its root is mounted, so every URL that Verso emits is relative to +# the document rather than to the origin. A URL that begins with a single slash addresses the origin +# instead, so it breaks as soon as the site is served under a prefix. Content may hold one on +# purpose, which is what `--allow` is for. +# +# usage: scripts/check-url-prefix.sh [--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: "

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"}}) ++ + #[{{}}, + {{"remote"}}, + {{}}, + {{}}, + {{}}, + {{}}, + {{}}, + {{
}}, + {{}}, + {{
}}, + {{"ping"}}, + {{"kept"}}] + +/-- +info: | +link +link +link +link +link +link +link +link +link + +remote + + + + + + +
+ +
+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 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", "a.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!"
One
" + }] }, + { path := #["one"], title := "One", titleHtml := "One", + fragments := #[{ + name := "content".sluggify, rootToken := defaultRootToken, + content := "

One.

" + }] } + ] + +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 "

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 " 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 `` and remote content alone. + let doc : Html := {{ +
+ + "remote" + "here" +
+ }} + let rewritten := (doc.rewriteUrls ("[" ++ · ++ "]")).asString + check ((rewritten.find? "").isSome) + s!"A base element keeps its own URL: {rewritten}" + check ((rewritten.find? "href=\"/remote/x\"").isSome) + s!"An element carrying data-verso-remote keeps its own URL: {rewritten}" + check ((rewritten.find? "href=\"[x]\"").isSome) + s!"Every other URL-valued attribute is rewritten: {rewritten}" + check ((rewritten.find? "title=\"/not-a-url\"").isSome) + s!"An attribute that holds no URL is left alone: {rewritten}" + +private def testTitleIsChecked : TestM Unit := do + IO.FS.withTempDir fun tmp => do + let dir := tmp / "title" + let (_, errors) ← exportSite dir imageTitleSite + check (errors.any (mentions ·.text "title")) + s!"A title that needs more than inline markup is reported: {errors.map (·.text)}" + +/-- +Runs the rendered HTML content export tests, returning the number of failures. +-/ +def runRenderedHtmlExportTests : IO Nat := do + let ((), failures) ← + (do + testExport + testChromeIsRejected + testAdHocChromeIsRejected + testAssetOrderIsStable + testUrlTable + testTitleIsChecked : TestM Unit).run 0 + return failures + +end Tests.RenderedHtmlExport diff --git a/src/tests/Tests/RenderedHtmlMount.lean b/src/tests/Tests/RenderedHtmlMount.lean new file mode 100644 index 000000000..c9aefad1b --- /dev/null +++ b/src/tests/Tests/RenderedHtmlMount.lean @@ -0,0 +1,266 @@ +/- +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 import Tests.RenderedHtmlExport + +public section + +open Lean +open Verso Genre Blog +open Verso.Output (Html) +open Verso.Output.Html +open Verso.RenderedHtml (load) +open Tests.RenderedHtmlExport (quietLogger part) + +namespace Tests.RenderedHtmlMount + +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 + +/-- 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" + +/-- The directory that `tutorial-example-rendered-html` writes. -/ +def tutorialContent : System.FilePath := "_out/tutorial-content/v1" + +/-- A page that a mount can sit under. -/ +private def holder (title : String) : Verso.Doc.Part Page := + part title #[Verso.Doc.Block.para #[.text "A page that holds mounts."]] + +/-- A site that mounts `dirs`, each under the name it is paired with, at the top level. -/ +def mountingSite (dirs : Array (String × System.FilePath)) : Site := + .page `mounting (holder "Mounting") <| + dirs.map fun (name, dir) => Dir.mkMount name dir + +/-- A site whose root is a blog, so it holds no directories. -/ +def blogRootedSite : Site := + .blog `blogRoot (holder "A Blog") #[] + +/-- The custom property definitions of one theme. -/ +private def themeVars (color : String) : String := + ":root { --verso-text-color: " ++ color ++ "; }" + +/-- A theme that places the fragments that a mount contributes. -/ +def mountingTheme (color : String) (withLocalNav : Bool := true) : Theme := + { Theme.default with + primaryTemplate := do + return {{ + + + {{← 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 {{

{{← Template.param "title"}}

{{← Template.param "content"}}
}} } + +/-- +Traverses and generates a site into `dir`, returning the errors and warnings that were reported. +-/ +def generate (dir : System.FilePath) (site : Site) (theme : Theme) : + IO (Array Verso.LogMessage × Array Verso.LogMessage) := do + let logger ← quietLogger + let cfg : Config := { destination := dir } + 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 (((), _), components) ← site.generate theme |>.run ctxt .empty {} |>.run logger + Template.writeBuiltinAssets dir "body" + Template.writeHeadAssets dir (theme.headAssets xref components) + return (← logger.errors, ← logger.warnings) + +/-- +Traverses a site, returning its traversal state and the errors that were reported. + +Traversal reports a conflict through the logger, not through the state, so a test that asserts no +conflict was reported has to read the logger. +-/ +def traverseOnly (site : Site) : IO (TraverseState × Array Verso.LogMessage) := do + let logger ← quietLogger + let (_, xref) ← site.traverse {} {} |>.run logger + return (xref, ← logger.errors) + +private def attempt (act : IO α) : IO (Except String α) := do + try + return .ok (← act) + catch e => + return .error (toString e) + +private def expectRejected (what : String) (expected : 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}" + +private def testPageIds : TestM Unit := do + let site := mountingSite #[("fixture", fixtureDir), ("fixture-again", fixtureDir)] + let (xref, errors) ← traverseOnly site + for name in ["fixture", "fixture.guide", "fixture.guide.first", "fixture.guide.«step-1»", + "«fixture-again»", "«fixture-again».guide", "«fixture-again».guide.«step-1»"] do + let id := (Syntax.decodeNameLit s!"`{name}").getD .anonymous + check (xref.pageIds.find? id |>.isSome) + s!"Mounting registers the page ID '{name}': {xref.pageIds.toList.map (·.fst)}" + check errors.isEmpty + s!"Mounting the same directory twice reports no conflict: {errors.map (·.text)}" + +private def testRejections : TestM Unit := do + expectRejected "A mount of a sparse directory" ["guide"] <| + traverseOnly (mountingSite #[("sparse", sparseFixtureDir)]) + expectRejected "A mount whose static files claim a page destination" ["index.html"] <| + traverseOnly (mountingSite #[("conflicting", conflictFixtureDir)]) + expectRejected "Inserting a mount under a blog-rooted path" ["blog"] <| + blogRootedSite.insertMount [] "fixture" fixtureDir + expectRejected "Inserting a mount under a static directory" ["not a page"] <| + (Site.page `s (holder "S") #[.static "files" "test-projects"]).insertMount + ["files"] "fixture" fixtureDir + expectRejected "Inserting a mount under a mount" ["not a page"] <| + (mountingSite #[("fixture", fixtureDir)]).insertMount ["fixture"] "inner" fixtureDir + expectRejected "Inserting a mount whose name is not a slug" ["slug"] <| + (Site.page `s (holder "S") #[]).insertMount [] "not a slug" fixtureDir + -- An empty name would put the mount's root page where its holder's own page goes. + expectRejected "Inserting a mount whose name is empty" ["slug"] <| + (Site.page `s (holder "S") #[]).insertMount [] "" fixtureDir + -- Two directories of the same name would generate into the same place. + expectRejected "Inserting a mount whose name is taken" ["already holds"] <| + (mountingSite #[("fixture", fixtureDir)]).insertMount [] "fixture" fixtureDir + expectRejected "Inserting a mount whose name a static directory holds" ["already holds"] <| + (Site.page `s (holder "S") #[.static "files" "test-projects"]).insertMount + [] "files" fixtureDir + +private def testExportRejectsMounts : TestM Unit := do + IO.FS.withTempDir fun tmp => do + let exported := Tests.RenderedHtmlExport.exportSite (tmp / "mounts") + (mountingSite #[("fixture", fixtureDir)]) (mountingTheme "black") + match ← attempt exported with + | .error message => + check (mentions message "mount") + s!"Exporting a site that holds a mount is rejected: {message}" + | .ok (_, errors) => + check (errors.any fun e => mentions e.text "mount" && mentions e.text "fixture") + s!"Exporting a site that holds a mount is rejected: {errors.map (·.text)}" + +private def testFragmentReports : TestM Unit := do + IO.FS.withTempDir fun tmp => do + let site := mountingSite #[("fixture", fixtureDir)] + let (errors, warnings) ← + generate (tmp / "dropped") site (mountingTheme "black" (withLocalNav := false)) + check errors.isEmpty s!"Generating a mounting site reported errors: {errors.map (·.text)}" + check (warnings.any fun w => mentions w.text "localNav" && mentions w.text "fixture") + s!"A fragment that no template placed is reported: {warnings.map (·.text)}" + + let dropping := + Site.page `mounting (holder "Mounting") + #[Dir.mkMount "fixture" fixtureDir + { droppedFragments := #["localNav".sluggify] }] + let (_, warnings) ← + generate (tmp / "silent") dropping (mountingTheme "black" (withLocalNav := false)) + check (!warnings.any (mentions ·.text "localNav")) + s!"A mount that drops a fragment on purpose is silent: {warnings.map (·.text)}" + +/-- The text between the first occurrence of `before` and the next occurrence of `after`. -/ +private def between (before after : String) (text : String) : String := + match text.splitOn before with + | _ :: rest :: _ => (rest.splitOn after).headD "" + | _ => "" + +private def testRetheming : TestM Unit := do + IO.FS.withTempDir fun tmp => do + let site := mountingSite #[("fixture", fixtureDir)] + let dark := tmp / "dark" + let light := tmp / "light" + let _ ← generate dark site (mountingTheme "white") + let _ ← generate light site (mountingTheme "black") + let darkPage ← IO.FS.readFile (dark / "fixture" / "guide" / "index.html") + let lightPage ← IO.FS.readFile (light / "fixture" / "guide" / "index.html") + check (darkPage != lightPage) + "Two themes whose custom properties differ produce different output" + check (between "
" "
" 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 "