Skip to content

Fix/relative urls#835

Open
NicolasRouquette wants to merge 3 commits intoleanprover:mainfrom
NicolasRouquette:fix/relative-img-urls
Open

Fix/relative urls#835
NicolasRouquette wants to merge 3 commits intoleanprover:mainfrom
NicolasRouquette:fix/relative-img-urls

Conversation

@NicolasRouquette
Copy link
Copy Markdown

Fixes #834

Problem

Two classes of URLs are broken in multi-page HTML output:

  1. Relative image URLs (from Markdown ![alt](path)) resolve from the site root instead of the page directory, because <base href="./../../"> shifts resolution.
  2. Absolute internal asset URLs (/-verso-data/katex/...) are converted by path.relativize to ../../-verso-data/..., which overshoots the root when combined with the <base> tag.

Changes

VersoManual/Html.lean

  • rwAttr: Replace path.relativize with simple /-stripping ((attr.snd.drop 1).toString). Since <base> already points to the site root, root-relative paths resolve correctly without ../ sequences.
  • rwTag: For <img> tags with relative src paths, prefix with the page path before calling rwAttr. This distinguishes user-authored relative URLs (need page-path prefix) from absolute URLs (just need / stripped). Adds isRelativeContentUrl helper.

VersoManual.lean

  • relativizeLinks: Now accepts a Path parameter and passes it to Html.relativize, so the page path is available for image URL adjustment.
  • Updated all three call sites: emitFindHtml (#["find"]), single-page emitter, and emitPart.

Result

URL type Before After
Image (graphs/foo.svg on page Verification/Key-Theorems/) src="graphs/foo.svg" → resolves to {root}/graphs/foo.svg (404) src="Verification/Key-Theorems/graphs/foo.svg" → correct
KaTeX asset src="../../-verso-data/katex/katex.js" → overshoots root (404) src="-verso-data/katex/katex.js" → correct
Internal links href="../../Overview/" → correct unchanged
CSS/JS (book.css, -verso-search/*) correct unchanged

NicolasRouquette and others added 3 commits April 11, 2026 17:36
Markdown image references like ![alt](graphs/foo.svg) produce
<img src="graphs/foo.svg"> in the HTML output. In multi-page mode,
the <base> tag causes the browser to resolve these relative URLs
from the site root instead of the page's directory, resulting in
broken image links.

Fix:
- Html.relativize now detects <img> tags with relative src attributes
  and prefixes them with the current page path
- relativizeLinks accepts the page Path instead of hardcoding #[]
- All three call sites pass the actual page path
Replaces complex path relativization logic with simple leading slash removal for absolute URLs. Since the base tag already points to the site root, root-relative paths resolve correctly without needing traversal sequences.

Reorders attribute processing to handle image source prefixing before general URL rewriting. This ensures originally-relative paths can still be distinguished from originally-absolute paths, allowing correct prefixing of user-authored image references.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

BUG: Relative URLs broken by <base> tag in multi-page HTML output

1 participant