feat: automatically track open-source libraries for web frontend (#279)

.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: |

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}

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"

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

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.
 

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