diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index ffd1ab7..5384d43 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -104,7 +104,7 @@ jobs:
 
       - name: Upload docs to artifact storage
         if: github.ref != 'refs/heads/main'
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: "Verso manual (PDF and HTML)"
           path: |
diff --git a/doc/UsersGuide/Basic.lean b/doc/UsersGuide/Basic.lean
index 5ecdfcd..05801c0 100644
--- a/doc/UsersGuide/Basic.lean
+++ b/doc/UsersGuide/Basic.lean
@@ -17,7 +17,7 @@ Documentation can take many forms:
  * Tutorials
  * Etc
 
-{include UsersGuide.Markup}
+{include 0 UsersGuide.Markup}
 
 # Genres
 %%%
@@ -97,3 +97,13 @@ number := false
 %%%
 
 {theIndex}
+
+
+# Dependencies
+%%%
+number := false
+%%%
+
+This document contains the following open-source libraries, or code derived from them:
+
+{licenseInfo}
diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean
index b2ab603..085b1f0 100644
--- a/src/verso-manual/VersoManual.lean
+++ b/src/verso-manual/VersoManual.lean
@@ -21,6 +21,7 @@ import VersoManual.Html
 import VersoManual.Html.Style
 import VersoManual.Draft
 import VersoManual.Index
+import VersoManual.License
 import VersoManual.Glossary
 import VersoManual.Docstring
 import VersoManual.WebAssets
@@ -120,6 +121,7 @@ structure Config where
   extraFiles : List (System.FilePath × String) := []
   extraCss : List String := []
   extraJs : List String := []
+  licenseInfo : List LicenseInfo := []
   /-- Extra elements to add to every page's `head` tag -/
   extraHead : Array Output.Html := #[]
   draft : Bool := false
@@ -170,7 +172,7 @@ where
 
 def traverse (logError : String → IO Unit) (text : Part Manual) (config : Config) : ReaderT ExtensionImpls IO (Part Manual × TraverseState) := do
   let topCtxt : Manual.TraverseContext := {logError, draft := config.draft}
-  let mut state : Manual.TraverseState := {}
+  let mut state : Manual.TraverseState := {licenseInfo := .ofList config.licenseInfo}
   let mut text := text
   if config.verbose then
     IO.println "Initializing extensions"
diff --git a/src/verso-manual/VersoManual/Basic.lean b/src/verso-manual/VersoManual/Basic.lean
index 35a3b54..0aa6dee 100644
--- a/src/verso-manual/VersoManual/Basic.lean
+++ b/src/verso-manual/VersoManual/Basic.lean
@@ -1,5 +1,5 @@
 /-
-Copyright (c) 2024 Lean FRO LLC. All rights reserved.
+Copyright (c) 2024-2025 Lean FRO LLC. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: David Thrane Christiansen
 -/
@@ -9,6 +9,7 @@ import Verso.Doc
 import Verso.Doc.Html
 import Verso.Doc.TeX
 import VersoManual.Slug
+import VersoManual.LicenseInfo
 import Verso.Output.Html
 import Verso.Output.TeX
 
@@ -292,6 +293,7 @@ structure TraverseState where
   extraJs : HashSet String := {}
   extraJsFiles : Array (String × String) := #[]
   extraCssFiles : Array (String × String) := #[]
+  licenseInfo : HashSet LicenseInfo := {}
   private contents : NameMap Json := {}
 
 def freshId [Monad m] [MonadStateOf TraverseState m] : m InternalId := do
@@ -347,7 +349,8 @@ instance : BEq TraverseState where
     x.contents.all fun k v =>
       match y.contents.find? k with
       | none => false
-      | some v' => v == v'
+      | some v' => v == v' &&
+    x.licenseInfo == y.licenseInfo
 
 namespace TraverseState
 
@@ -386,6 +389,10 @@ def htmlId (state : TraverseState) (id : InternalId) : Array (String × String)
   if let some (_, htmlId) := state.externalTags[id]? then
     #[("id", htmlId.toString)]
   else #[]
+
+/-- Add an open-source license used in the generated HTML/JavaScript -/
+def addLicenseInfo (state : TraverseState) (licenseInfo : LicenseInfo) : TraverseState :=
+  {state with licenseInfo := state.licenseInfo.insert licenseInfo}
 end TraverseState
 
 
@@ -539,12 +546,13 @@ structure InlineDescr where
   extraJsFiles : List (String × String) := []
   extraCss : List String := []
   extraCssFiles : List (String × String) := []
+  licenseInfo : List LicenseInfo := []
 
   toTeX : Option (InlineToTeX Manual (ReaderT ExtensionImpls IO))
 
 deriving TypeName
 
-instance : Inhabited InlineDescr := ⟨⟨id, default, default, default, default, default, default, default⟩⟩
+instance : Inhabited InlineDescr := ⟨⟨id, default, default, default, default, default, default, default, default⟩⟩
 
 structure BlockDescr where
   init : TraverseState → TraverseState := id
@@ -556,11 +564,12 @@ structure BlockDescr where
   extraJsFiles : List (String × String) := []
   extraCss : List String := []
   extraCssFiles : List (String × String) := []
+  licenseInfo : List LicenseInfo := []
 
   toTeX : Option (BlockToTeX Manual (ReaderT ExtensionImpls IO))
 deriving TypeName
 
-instance : Inhabited BlockDescr := ⟨⟨id, default, default, default, default, default, default, default⟩⟩
+instance : Inhabited BlockDescr := ⟨⟨id, default, default, default, default, default, default, default, default⟩⟩
 
 open Lean in
 initialize inlineExtensionExt
@@ -887,6 +896,8 @@ instance : Traverse Manual TraverseM where
           for (name, js) in impl.extraCssFiles do
             unless (← get).extraCssFiles.any (·.1 == name) do
               modify fun s => {s with extraCssFiles := s.extraCssFiles.push (name, js)}
+          for licenseInfo in impl.licenseInfo do
+            modify (·.addLicenseInfo licenseInfo)
 
           impl.traverse id data content
         else
@@ -910,6 +921,8 @@ instance : Traverse Manual TraverseM where
           for (name, js) in impl.extraCssFiles do
             unless (← get).extraCssFiles.any (·.1 == name) do
               modify fun s => {s with extraCssFiles := s.extraCssFiles.push (name, js)}
+          for licenseInfo in impl.licenseInfo do
+            modify (·.addLicenseInfo licenseInfo)
 
           impl.traverse id data content
         else
diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean
index 8dc61f8..10c37c2 100644
--- a/src/verso-manual/VersoManual/Docstring.lean
+++ b/src/verso-manual/VersoManual/Docstring.lean
@@ -6,6 +6,7 @@ Author: David Thrane Christiansen
 import Std.Data.HashSet
 
 import VersoManual.Basic
+import VersoManual.HighlightedCode
 import VersoManual.Index
 import VersoManual.Markdown
 import VersoManual.Docstring.Config
@@ -684,7 +685,7 @@ def constructorSignature.descr : BlockDescr where
 
 open Verso.Genre.Manual.Markdown in
 @[block_extension Block.docstring]
-def docstring.descr : BlockDescr where
+def docstring.descr : BlockDescr := withHighlighting {
   init st := st
     |>.setDomainTitle docstringDomain "Lean constant reference"
     |>.setDomainDescription docstringDomain "Documentation for Lean constants"
@@ -751,10 +752,8 @@ def docstring.descr : BlockDescr where
         </div>
       }}
   toTeX := some <| fun _goI goB _id _info contents => contents.mapM goB
-  extraCss := [highlightingStyle, docstringStyle]
-  extraJs := [highlightingJs]
-  extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)]
-  extraCssFiles := [("tippy-border.css", tippy.border.css)]
+  extraCss := [docstringStyle]
+}
 where
   saveRef
       (id : InternalId) (name : Name)
@@ -783,16 +782,12 @@ def Block.leanFromMarkdown (hls : Highlighted) : Block where
 
 
 @[inline_extension leanFromMarkdown]
-def leanFromMarkdown.inlinedescr : InlineDescr where
+def leanFromMarkdown.inlinedescr : InlineDescr := withHighlighting {
   traverse _id _data _ := pure none
   toTeX :=
     some <| fun go _ _ content => do
       pure <| .seq <| ← content.mapM fun b => do
         pure <| .seq #[← go b, .raw "\n"]
-  extraCss := [highlightingStyle]
-  extraJs := [highlightingJs]
-  extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)]
-  extraCssFiles := [("tippy-border.css", tippy.border.css)]
   toHtml :=
     open Verso.Output Html in
     open Verso.Doc.Html in
@@ -803,18 +798,15 @@ def leanFromMarkdown.inlinedescr : InlineDescr where
         pure .empty
       | .ok (hl : Highlighted) =>
         hl.inlineHtml "docstring-examples"
+}
 
 @[block_extension leanFromMarkdown]
-def leanFromMarkdown.blockdescr : BlockDescr where
+def leanFromMarkdown.blockdescr : BlockDescr := withHighlighting {
   traverse _id _data _ := pure none
   toTeX :=
     some <| fun goI goB _ _ content => do
       pure <| .seq <| ← content.mapM fun b => do
         pure <| .seq #[← goB b, .raw "\n"]
-  extraCss := [highlightingStyle]
-  extraJs := [highlightingJs]
-  extraJsFiles := [("popper.js", popper), ("tippy.js", tippy)]
-  extraCssFiles := [("tippy-border.css", tippy.border.css)]
   toHtml :=
     open Verso.Output Html in
     open Verso.Doc.Html in
@@ -825,6 +817,7 @@ def leanFromMarkdown.blockdescr : BlockDescr where
         pure .empty
       | .ok (hl : Highlighted) =>
         hl.blockHtml "docstring-examples"
+}
 
 open Lean Elab Term in
 def tryElabCodeTermWith (mk : Highlighted → String → DocElabM α) (str : String) (ignoreElabErrors := false) (identOnly := false) : DocElabM α := do
@@ -1555,7 +1548,7 @@ def tactic : DirectiveExpander
 open Verso.Genre.Manual.Markdown in
 open Lean Elab Term Parser Tactic Doc in
 @[block_extension tactic]
-def tactic.descr : BlockDescr where
+def tactic.descr : BlockDescr := withHighlighting {
   init st := st
     |>.setDomainTitle tacticDomain "Tactic Documentation"
     |>.setDomainDescription tacticDomain "Detailed descriptions of tactics"
@@ -1594,9 +1587,8 @@ def tactic.descr : BlockDescr where
         </div>
       }}
   toTeX := some <| fun _goI goB _id _info contents => contents.mapM goB
-  extraCss := [highlightingStyle, docstringStyle]
-  extraJs := [highlightingJs]
-
+  extraCss := [docstringStyle]
+}
 
 def Inline.tactic : Inline where
   name := `Verso.Genre.Manual.tacticInline
@@ -1632,15 +1624,14 @@ where
 
 
 @[inline_extension tacticInline]
-def tacticInline.descr : InlineDescr where
+def tacticInline.descr : InlineDescr := withHighlighting {
   traverse _ _ _ := do
     pure none
   toTeX :=
     some <| fun go _ _ content => do
       pure <| .seq <| ← content.mapM fun b => do
         pure <| .seq #[← go b, .raw "\n"]
-  extraCss := [highlightingStyle, docstringStyle]
-  extraJs := [highlightingJs]
+  extraCss := [docstringStyle]
   toHtml :=
     open Verso.Output.Html Verso.Doc.Html in
     some <| fun _ _ data _ => do
@@ -1650,6 +1641,7 @@ def tacticInline.descr : InlineDescr where
         pure .empty
       | .ok (hl : Highlighted) =>
         hl.inlineHtml "examples"
+}
 
 -- TODO implement a system upstream like the one for normal tactics
 def Block.conv (name : Name) («show» : String) (docs? : Option String) : Block where
@@ -1691,7 +1683,7 @@ def conv : DirectiveExpander
 open Verso.Genre.Manual.Markdown in
 open Lean Elab Term Parser Tactic Doc in
 @[block_extension conv]
-def conv.descr : BlockDescr where
+def conv.descr : BlockDescr := withHighlighting {
   init st := st
     |>.setDomainTitle convDomain "Conversion Tactics"
     |>.setDomainDescription convDomain "Tactics for performing targeted rewriting of subterms"
@@ -1728,9 +1720,8 @@ def conv.descr : BlockDescr where
         </div>
       }}
   toTeX := some <| fun _goI goB _id _info contents => contents.mapM goB
-  extraCss := [highlightingStyle, docstringStyle]
-  extraJs := [highlightingJs]
-
+  extraCss := [docstringStyle]
+}
 /--
 A progress tracker that shows how many symbols are documented.
 
diff --git a/src/verso-manual/VersoManual/HighlightedCode.lean b/src/verso-manual/VersoManual/HighlightedCode.lean
new file mode 100644
index 0000000..9ef8c41
--- /dev/null
+++ b/src/verso-manual/VersoManual/HighlightedCode.lean
@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
+import Verso
+
+import VersoManual.Basic
+import VersoManual.License
+
+namespace Verso.Genre.Manual
+
+open Verso.Code
+open Verso.Code.Highlighted.WebAssets
+
+open Licenses
+
+class CanHighlightCode (α : Type) where
+  addDependencies : α → α
+
+/--
+Add the necessary frontend dependencies for showing Verso-highlighted Lean code
+-/
+def withHighlighting [CanHighlightCode α] (blockOrInline : α) : α :=
+  CanHighlightCode.addDependencies blockOrInline
+
+instance : CanHighlightCode BlockDescr where
+  addDependencies b :=
+    {b with
+      extraCss := highlightingStyle :: b.extraCss
+      extraJs := highlightingJs :: b.extraJs
+      extraJsFiles := ("popper.js", popper) :: ("tippy.js", tippy) :: b.extraJsFiles
+      extraCssFiles := ("tippy-border.css", tippy.border.css) :: b.extraCssFiles
+      licenseInfo := b.licenseInfo |>.insert tippy.js |>.insert popper.js
+      }
+
+instance : CanHighlightCode InlineDescr where
+  addDependencies i :=
+    {i with
+      extraCss := highlightingStyle :: i.extraCss
+      extraJs := highlightingJs :: i.extraJs
+      extraJsFiles := ("popper.js", popper) :: ("tippy.js", tippy) :: i.extraJsFiles
+      extraCssFiles := ("tippy-border.css", tippy.border.css) :: i.extraCssFiles
+      licenseInfo := i.licenseInfo |>.insert tippy.js |>.insert popper.js
+      }
diff --git a/src/verso-manual/VersoManual/License.lean b/src/verso-manual/VersoManual/License.lean
new file mode 100644
index 0000000..54952ff
--- /dev/null
+++ b/src/verso-manual/VersoManual/License.lean
@@ -0,0 +1,165 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
+import Verso
+import Verso.Doc.ArgParse
+
+import VersoManual.LicenseInfo
+import VersoManual.Basic
+
+/-!
+
+This module contains information about all the open-source licenses that are used as part of the
+HTML versions of Lean documentation.
+
+-/
+
+
+open Lean (ToJson FromJson)
+
+open Verso ArgParse Doc Elab
+
+namespace Verso.Genre.Manual
+namespace Licenses
+
+def popper.js : LicenseInfo where
+  identifier := "MIT"
+  dependency := "Popper.js"
+  howUsed := some "Popper.js is used (as a dependency of Tippy.js) to show information (primarily in Lean code) when hovering the mouse over an item of interest."
+  link := some "https://popper.js.org/docs/v2/"
+  text := #[
+  (some "The MIT License",
+r#"
+Copyright (c) 2019 Federico Zivolo
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of
+this software and associated documentation files (the "Software"), to deal in
+the Software without restriction, including without limitation the rights to
+use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of
+the Software, and to permit persons to whom the Software is furnished to do so,
+subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR
+COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER
+IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN
+CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+"#)]
+
+def tippy.js : LicenseInfo where
+  identifier := "MIT"
+  dependency := "Tippy.js"
+  howUsed := some "Tippy.js is used together with Popper.js to show information (primarily in Lean code) when hovering the mouse over an item of interest."
+  link := some "https://atomiks.github.io/tippyjs/"
+  text := #[
+  (some "The MIT License",
+r#"
+Copyright (c) 2017-present atomiks
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.
+
+"#)]
+
+end Licenses
+
+def Block.licenseInfo : Block where
+  name := `Verso.Genre.Manual.licenseInfo
+
+@[block_role_expander licenseInfo]
+def licenseInfo : BlockRoleExpander
+  | args, contents => do
+    if let some first := contents[0]? then
+      throwErrorAt first "Unexpected contents"
+    ArgParse.done.run args
+    return #[← ``(Block.other Block.licenseInfo #[])]
+
+open Verso.Output Html
+
+private def paragraphed (text : String) : Array String := Id.run do
+  let lines := text.splitOn "\n"
+  let mut paras := #[]
+  let mut thisPara := #[]
+  for l in lines do
+    if l.all (·.isWhitespace) then
+      if !thisPara.isEmpty then
+        paras := paras.push (" ".intercalate thisPara.toList)
+        thisPara := #[]
+    else
+      thisPara := thisPara.push l
+  if !thisPara.isEmpty then
+    paras := paras.push (" ".intercalate thisPara.toList)
+
+  paras
+
+/-- info: #["One paragraph with lines", "and another", "and more more"] -/
+#guard_msgs in
+#eval paragraphed r#"
+
+One paragraph
+with lines
+
+and another
+
+and more
+more
+
+"#
+
+private def paragraphedHtml (text : String) : Html :=
+  paragraphed text |>.map (fun (s : String) => {{<p>{{s}}</p>}})
+
+def LicenseInfo.toHtml (license : LicenseInfo) (headerLevel : Nat) : Html :=
+  let {identifier, dependency, howUsed, link, text} := license
+  {{<section class="license-info">
+      {{.tag s!"h{headerLevel}" #[] dependency }}
+      {{link.map (fun url => {{<a class="link" href={{url}}>{{url}}</a>}}) |>.getD .empty}}
+      {{howUsed.map paragraphedHtml |>.getD .empty}}
+      <code class="spdx">{{identifier}}</code>
+      {{text.map textHtml}}
+    </section>}}
+where
+  textHtml
+    | (hdr?, txt) =>
+      let hdrHtml :=
+        if let some hdr := hdr? then
+          Html.tag s!"h{headerLevel+1}" #[] hdr
+        else
+          .empty
+      {{<section>{{hdrHtml}}{{paragraphedHtml txt}}</section>}}
+
+@[block_extension licenseInfo]
+def lean.descr : BlockDescr where
+  traverse _ _ _ := do
+    pure none
+  toTeX := some <| fun _ _ _ _ _ => pure .empty
+  toHtml :=
+    open Verso.Output.Html in
+    some <| fun _ _ _ _ _ => do
+      let headerLevel := (← read).traverseContext.headers.size + 1
+      let allLicenses := (← read).traverseState.licenseInfo.toArray
+      let allLicenses := allLicenses.qsort (·.dependency.trim.toLower < ·.dependency.trim.toLower)
+
+      return allLicenses.map (·.toHtml headerLevel)
diff --git a/src/verso-manual/VersoManual/LicenseInfo.lean b/src/verso-manual/VersoManual/LicenseInfo.lean
new file mode 100644
index 0000000..0bef865
--- /dev/null
+++ b/src/verso-manual/VersoManual/LicenseInfo.lean
@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2025 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: David Thrane Christiansen
+-/
+
+import Lean.Data.Json
+
+open Lean (ToJson FromJson)
+
+namespace Verso.Genre.Manual
+
+/--
+A description of an open-source license used by a frontend component that's included in
+generated HTML. This is used to create an attribution page.
+-/
+structure LicenseInfo where
+  /-- SPDX license identifier -/
+  identifier : String
+
+  /-- Dependency name. This is used in a header, and for alphabetical sorting. -/
+  dependency : String
+
+  /--
+  How is the dependency used? This can give better credit.
+
+  Examples:
+    * "The display of mathematical formulae is powered by KaTeX."
+    * "The graphs are rendered using Chart.js."
+  -/
+  howUsed : Option String
+
+  /-- A link target used to credit the dependency's author -/
+  link : Option String
+
+  /--
+  The license or notice text in plain text, divided into sections with optional headers.
+   -/
+  text : Array (Option String × String)
+
+deriving Repr, DecidableEq, ToJson, FromJson, Hashable, Inhabited
diff --git a/src/verso/Verso/Output/TeX.lean b/src/verso/Verso/Output/TeX.lean
index ce386c7..2c7615e 100644
--- a/src/verso/Verso/Output/TeX.lean
+++ b/src/verso/Verso/Output/TeX.lean
@@ -29,6 +29,8 @@ instance : Append TeX where
 
 namespace TeX
 
+def empty : TeX := .seq #[]
+
 partial def asString (doc : TeX) : String :=
   match doc with
   | .text str => escape str