WIP: upstream search/quickjump bar

.github/workflows/ci.yml

@@ -76,7 +76,7 @@ jobs:
       - name: Install PDF Dependencies
         uses: zauguin/install-texlive@v4
         with:
-          texlive_version: 2024
+          texlive_version: 2025
           packages: |
             scheme-minimal
             l3packages
@@ -115,6 +115,15 @@ jobs:
           cp -r _out/html-single html-single-page
           zip -r html-single-page.zip html-single-page
 
+      - name: Install TypeScript
+        run: |
+          sudo apt update && sudo apt install node-typescript
+
+      - name: Type check the search bar code
+        run: |
+          cd _out/html-multi/-verso-search
+          tsc --noEmit -p jsconfig.json
+
       - name: Upload docs to artifact storage
         if: github.ref != 'refs/heads/main'
         uses: actions/upload-artifact@v4

.github/workflows/merge-main-nightly.yml

@@ -66,7 +66,7 @@ jobs:
       - name: Install PDF Dependencies
         uses: zauguin/install-texlive@v4
         with:
-          texlive_version: 2024
+          texlive_version: 2025
           packages: |
             scheme-minimal
             l3packages

.github/workflows/update-nightly.yml

@@ -123,7 +123,7 @@ jobs:
     - name: Install PDF Dependencies
       uses: zauguin/install-texlive@v4
       with:
-        texlive_version: 2024
+        texlive_version: 2025
         packages: |
           scheme-minimal
           l3packages

doc/UsersGuide/Basic.lean

@@ -59,6 +59,7 @@ results in
 
 ## More Docstring Examples
 %%%
+tag := "more-docstring-examples"
 shortTitle := "More Docstrings"
 %%%
 
@@ -113,6 +114,7 @@ References to technical terms are valid both before and after their definition s
 
 # Index
 %%%
+tag := "index"
 number := false
 %%%
 
@@ -121,6 +123,7 @@ number := false
 
 # Dependencies
 %%%
+tag := "dependencies"
 number := false
 %%%
 

doc/UsersGuide/Markup.lean

@@ -57,6 +57,9 @@ tag := "lean-markup"
 Lean's documentation markup language is a close relative of Markdown, but it's not identical to it.
 
 # Design Principles
+%%%
+tag := "markup-design-principles"
+%%%
 
  1. Syntax errors - fail fast rather than producing unexpected output or having complicated rules
  2. Reduce lookahead - parsing should succeed or fail as locally as possible
@@ -66,6 +69,9 @@ Lean's documentation markup language is a close relative of Markdown, but it's n
  6. Pandoc and Djot compatibility - when Markdown doesn't have a syntax for a feature, attempt to be compatible with Pandoc Markdown or Djot
 
 # Syntax
+%%%
+tag := "markup-syntax"
+%%%
 
 Like Markdown, Lean's markup has three primary syntactic categories:
 
@@ -82,8 +88,14 @@ Like Markdown, Lean's markup has three primary syntactic categories:
  Headers, footnote definitions, and named links give greater structure to a document. They may not be nested inside of blocks.
 
 ## Description
+%%%
+tag := "markup-syntax-description"
+%%%
 
 ### Inline Syntax
+%%%
+tag := "inline-syntax"
+%%%
 
 Emphasis is written with underscores:
 ```markupPreview
@@ -118,32 +130,53 @@ The definition of `main`
 TeX math can be included using a single or double dollar sign followed by code. Two dollar signs results in display-mode math, so `` $`\sum_{i=0}^{10} i` `` results in $`\sum_{i=0}^{10} i` while `` $$`\sum_{i=0}^{10} i` `` results in: $$`\sum_{i=0}^{10} i`
 
 ### Block Syntax
+%%%
+tag := "block-syntax"
+%%%
 
 ### Document Structure
+%%%
+tag := "document-structure"
+%%%
 
 ## Differences from Markdown
+%%%
+tag := "differences-from-markdown"
+%%%
 
 This is a quick "cheat sheet" for those who are used to Markdown, documenting the differences.
 
 ### Syntax Errors
+%%%
+tag := "syntax-errors"
+%%%
 
 While Markdown includes a set of precedence rules to govern the meaning of mismatched delimiters (such as in `what _is *bold_ or emph*?`), these are syntax errors in Lean's markup.
 Similarly, Markdown specifies that unmatched delimiters (such as `*` or `_`) should be included as characters, while Lean's markup requires explicit escaping of delimiters.
 
 This is based on the principle that, for long-form technical writing, it's better to catch typos while writing than while reviewing the text later.
 
 ### Reduced Lookahead
+%%%
+tag := "reduced-lookahead"
+%%%
 
 In Markdown, whether `[this][here]` is a link depends on whether `here` is defined as a link reference target somewhere in the document.
 In Lean's markup, it is always a link, and it is an error if `here` is not defined as a link target.
 
 ### Header Nesting
+%%%
+tag := "header-nesting"
+%%%
 
 In Lean's markup, every document already has a title, so there's no need to use the highest level header (`#`) to specify one.
 Additionally, all documents are required to use `#` for their top-level header, `##` for the next level, and so forth, because a single file may represent a section, a chapter, or even a whole book.
 Authors should not need to maintain a global mapping from header levels to document structures, so Lean's markup automatically assigns these based on the structure of the document.
 
 ### Genre-Specific Extensions
+%%%
+tag := "genre-specific-extensions"
+%%%
 
 Markdown has no standard way for specific tools or styles of writing to express domain- or {ref "genres"}[genre]-specific concepts.
 Lean's markup provides standard syntaxes to use for this purpose, enabling compositional extensions.

examples/anchor-examples/lake-manifest.json

@@ -6,7 +6,7 @@
       "url": "https://github.com/leanprover/subverso",
       "type": "git",
       "subDir": null,
-      "rev": "8d780d556de7ed7b1006805bcbc64959b8173e1d",
+      "rev": "b7042025a7e0c445b7bb11c062ce2af997cf64cb",
       "name": "subverso",
       "manifestFile": "lake-manifest.json",
       "inputRev": "main",

examples/custom-genre/SimplePage.lean

@@ -156,6 +156,8 @@ implement traversal for the provided part metadata, block extensions, and inline
 
 instance : TraversePart SimplePage := {}
 
+instance : TraverseBlock SimplePage := {}
+
 instance : Traverse SimplePage TraverseM where
   part _ := pure none
   block _ := pure ()
@@ -220,7 +222,6 @@ instance : GenreHtml SimplePage IO where
     | .inr ⟨dest, some t⟩, contents => do
       pure {{<a href=s!"#{dest}" id=s!"link-{t}"> {{← contents.mapM recur}} </a>}}
 
-
 /--
 The main function to be called to produce HTML output
 -/

examples/documented-package/lake-manifest.json

@@ -7,7 +7,7 @@
       "type": "git",
       "subDir": null,
       "scope": "",
-      "rev": "8d780d556de7ed7b1006805bcbc64959b8173e1d",
+      "rev": "b7042025a7e0c445b7bb11c062ce2af997cf64cb",
       "name": "subverso",
       "manifestFile": "lake-manifest.json",
       "inputRev": "main",

examples/website-examples/lake-manifest.json

@@ -6,7 +6,7 @@
       "url": "https://github.com/leanprover/subverso",
       "type": "git",
       "subDir": null,
-      "rev": "8d780d556de7ed7b1006805bcbc64959b8173e1d",
+      "rev": "b7042025a7e0c445b7bb11c062ce2af997cf64cb",
       "name": "subverso",
       "manifestFile": "lake-manifest.json",
       "inputRev": "main",

examples/website-literate/lake-manifest.json

@@ -7,7 +7,7 @@
       "type": "git",
       "subDir": null,
       "scope": "",
-      "rev": "8d780d556de7ed7b1006805bcbc64959b8173e1d",
+      "rev": "b7042025a7e0c445b7bb11c062ce2af997cf64cb",
       "name": "subverso",
       "manifestFile": "lake-manifest.json",
       "inputRev": "main",

examples/website/DemoSiteMain.lean

@@ -79,8 +79,8 @@ def demoSite : Site := site DemoSite.Front /
     DemoSite.Blog.FirstPost
 
 
-def linkTargets : Code.LinkTargets where
-  const n := #[{shortDescription := "doc", description := s!"Documentation for {n}", href := s!"http://site.example/constlink/{n}"}]
-  definition d := #[{shortDescription := "def", description := "Definition", href := s!"http://site.example/deflink/{d}"}]
+def linkTargets : Code.LinkTargets TraverseContext where
+  const n _ := #[{shortDescription := "doc", description := s!"Documentation for {n}", href := s!"http://site.example/constlink/{n}"}]
+  definition d _ := #[{shortDescription := "def", description := "Definition", href := s!"http://site.example/deflink/{d}"}]
 
 def main := blogMain theme demoSite (linkTargets := linkTargets)

lake-manifest.json

@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "8d780d556de7ed7b1006805bcbc64959b8173e1d",
+   "rev": "b7042025a7e0c445b7bb11c062ce2af997cf64cb",
    "name": "subverso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.lean

@@ -7,6 +7,11 @@ require MD4Lean from git "https://github.com/acmepjz/md4lean"@"main"
 package verso where
   precompileModules := false -- temporarily disabled to work around an issue with nightly-2025-03-30
 
+@[default_target]
+lean_lib VersoUtil where
+  srcDir := "src/verso-util"
+  roots := #[`VersoUtil]
+
 @[default_target]
 lean_lib Verso where
   srcDir := "src/verso"
@@ -17,9 +22,14 @@ lean_lib MultiVerso where
   srcDir := "src/multi-verso"
   roots := #[`MultiVerso]
 
+input_dir searchJs where
+  path := "static-web/search"
+
 @[default_target]
 lean_lib VersoSearch where
   srcDir := "src/verso-search"
+  -- Rebuild search when JS on disk changes
+  needs := #[searchJs]
 
 @[default_target]
 lean_lib VersoBlog where
@@ -51,6 +61,7 @@ lean_exe «verso-demo» where
 
 lean_lib UsersGuide where
   srcDir := "doc"
+  leanOptions := #[⟨`weak.linter.verso.manual.headerTags, true⟩]
 
 @[default_target]
 lean_exe usersguide where

src/verso-blog/VersoBlog.lean

@@ -799,7 +799,7 @@ private def filterString (p : Char → Bool) (str : String) : String := Id.run <
   pure out
 
 open Template in
-def blogMain (theme : Theme) (site : Site) (relativizeUrls := true) (linkTargets : Code.LinkTargets := {})
+def blogMain (theme : Theme) (site : Site) (relativizeUrls := true) (linkTargets : Code.LinkTargets TraverseContext := {})
     (options : List String) (components : Components := by exact %registered_components) :
     IO UInt32 := do
   let hasError ← IO.mkRef false

src/verso-blog/VersoBlog/Generate.lean

@@ -27,7 +27,7 @@ structure Generate.Context where
   site : Site
   ctxt : TraverseContext
   xref : TraverseState
-  linkTargets : LinkTargets
+  linkTargets : LinkTargets TraverseContext
   /-- The root directory in which to generate the static site -/
   dir : System.FilePath
   config : Config
@@ -77,7 +77,7 @@ def GenerateM.toHtml (g : Genre)
     (bg.context_eq ▸ ctxt)
     (bg.state_eq ▸ state)
     {}
-    linkTargets
+    (bg.context_eq ▸ linkTargets)
     {}
     x
     (← get)
@@ -92,6 +92,7 @@ namespace Params
 
 def forPart [BlogGenre g] [GenreHtml g ComponentM]
     [ToHtml g ComponentM (Part g)]
+    [ToHtml g ComponentM (Block g)]
     (txt : Part g) : GenerateM Params := do
   let titleHtml : Html ← txt.title.mapM (GenerateM.toHtml g)
   let preamble ← txt.content.mapM (GenerateM.toHtml g)

src/verso-blog/VersoBlog/Template.lean

@@ -147,7 +147,7 @@ def blockHtml (g : Genre)
     pure {{ <pre class=s!"lexed {content.name}"> {{ content.toHtml }} </pre> }}
   | .highlightedCode { contextName, showProofStates } hls, _contents =>
     withReader (fun ρ => { ρ with codeOptions.inlineProofStates := showProofStates }) <|
-    hls.blockHtml (toString contextName)
+    hls.blockHtml (toString contextName) (g := g)
   | .htmlDetails classes summary, contents => do
     pure {{ <details class={{classes}}><summary>{{summary}}</summary> {{← contents.mapM goB}}</details>}}
   | .htmlWrapper name attrs, contents => do
@@ -176,11 +176,11 @@ def inlineHtml (g : Genre) [bg : BlogGenre g]
     Blog.InlineExt → Array (Inline g) → HtmlM g Html
   | .highlightedCode { contextName, showProofStates } hls, _contents =>
     withReader (fun ρ => { ρ with codeOptions.inlineProofStates := showProofStates }) <|
-    hls.inlineHtml (some <| toString contextName)
+    hls.inlineHtml (some <| toString contextName) (g := g)
   | .lexedText content, _contents => do
     pure {{ <code class=s!"lexed {content.name}"> {{ content.toHtml }} </code> }}
   | .customHighlight hls, _contents => do
-    hls.inlineHtml none
+    hls.inlineHtml none (g := g)
   | .label x, contents => do
     let contentHtml ← contents.mapM go
     let st ← bg.state_eq ▸ state

src/verso-blog/VersoBlog/Traverse.lean

@@ -109,10 +109,14 @@ def traverser (g : Genre) [bg : BlogGenre g] : Traverse g Blog.TraverseM where
 
 instance : TraversePart Page := {}
 
+instance : TraverseBlock Page := {}
+
 instance : Traverse Page Blog.TraverseM := traverser Page
 
 instance : TraversePart Post := {}
 
+instance : TraverseBlock Post := {}
+
 instance : Traverse Post Blog.TraverseM := traverser Post
 
 end Traverse