diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 06f7cb0bc..07bf39f3e 100644
--- a/.github/workflows/ci.yml
+++ b/.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
diff --git a/.github/workflows/merge-main-nightly.yml b/.github/workflows/merge-main-nightly.yml
index 38185f9b1..358c53d13 100644
--- a/.github/workflows/merge-main-nightly.yml
+++ b/.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
diff --git a/.github/workflows/update-nightly.yml b/.github/workflows/update-nightly.yml
index 58e1295c7..d87450e47 100644
--- a/.github/workflows/update-nightly.yml
+++ b/.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
diff --git a/doc/UsersGuide/Basic.lean b/doc/UsersGuide/Basic.lean
index a45f572ed..d31c8da0e 100644
--- a/doc/UsersGuide/Basic.lean
+++ b/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
%%%
diff --git a/doc/UsersGuide/Markup.lean b/doc/UsersGuide/Markup.lean
index 149d530e5..ec5cbdcfe 100644
--- a/doc/UsersGuide/Markup.lean
+++ b/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,14 +130,26 @@ 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.
@@ -133,17 +157,26 @@ Similarly, Markdown specifies that unmatched delimiters (such as `*` or `_`) sho
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.
diff --git a/examples/anchor-examples/lake-manifest.json b/examples/anchor-examples/lake-manifest.json
index 59203533a..373a7b1f8 100644
--- a/examples/anchor-examples/lake-manifest.json
+++ b/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",
diff --git a/examples/custom-genre/SimplePage.lean b/examples/custom-genre/SimplePage.lean
index 883b258ab..f7495a314 100644
--- a/examples/custom-genre/SimplePage.lean
+++ b/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 {{ {{← contents.mapM recur}} }}
-
/--
The main function to be called to produce HTML output
-/
diff --git a/examples/documented-package/lake-manifest.json b/examples/documented-package/lake-manifest.json
index ed12671b8..316dac986 100644
--- a/examples/documented-package/lake-manifest.json
+++ b/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",
diff --git a/examples/website-examples/lake-manifest.json b/examples/website-examples/lake-manifest.json
index 59203533a..373a7b1f8 100644
--- a/examples/website-examples/lake-manifest.json
+++ b/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",
diff --git a/examples/website-literate/lake-manifest.json b/examples/website-literate/lake-manifest.json
index 039ec8178..0e34ec32b 100644
--- a/examples/website-literate/lake-manifest.json
+++ b/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",
diff --git a/examples/website/DemoSiteMain.lean b/examples/website/DemoSiteMain.lean
index b78e456fb..edbc44e81 100644
--- a/examples/website/DemoSiteMain.lean
+++ b/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)
diff --git a/lake-manifest.json b/lake-manifest.json
index d8dd6dfdd..9b23a65e6 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,7 +15,7 @@
"type": "git",
"subDir": null,
"scope": "",
- "rev": "8d780d556de7ed7b1006805bcbc64959b8173e1d",
+ "rev": "b7042025a7e0c445b7bb11c062ce2af997cf64cb",
"name": "subverso",
"manifestFile": "lake-manifest.json",
"inputRev": "main",
diff --git a/lakefile.lean b/lakefile.lean
index 2b6a4e8d6..5a45b574b 100644
--- a/lakefile.lean
+++ b/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
diff --git a/src/verso-blog/VersoBlog.lean b/src/verso-blog/VersoBlog.lean
index 7c635b9d1..31af60388 100644
--- a/src/verso-blog/VersoBlog.lean
+++ b/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
diff --git a/src/verso-blog/VersoBlog/Generate.lean b/src/verso-blog/VersoBlog/Generate.lean
index ede6dcf06..c077e0d59 100644
--- a/src/verso-blog/VersoBlog/Generate.lean
+++ b/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)
diff --git a/src/verso-blog/VersoBlog/Template.lean b/src/verso-blog/VersoBlog/Template.lean
index 140ce1329..41a168610 100644
--- a/src/verso-blog/VersoBlog/Template.lean
+++ b/src/verso-blog/VersoBlog/Template.lean
@@ -147,7 +147,7 @@ def blockHtml (g : Genre)
pure {{
{{ content.toHtml }}
}}
| .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 {{ {{summary}} {{← contents.mapM goB}}}}
| .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 {{ {{ content.toHtml }} }}
| .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
diff --git a/src/verso-blog/VersoBlog/Traverse.lean b/src/verso-blog/VersoBlog/Traverse.lean
index c234e2283..0d939dbc2 100644
--- a/src/verso-blog/VersoBlog/Traverse.lean
+++ b/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
diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean
index 9adeeae4b..27875985e 100644
--- a/src/verso-manual/VersoManual.lean
+++ b/src/verso-manual/VersoManual.lean
@@ -41,6 +41,8 @@ import VersoManual.Table
open Lean (Name NameMap Json ToJson FromJson quote)
+open Std (HashMap)
+
open Verso.FS
open Verso.Doc Elab
@@ -212,7 +214,7 @@ structure Config where
/--
How to insert links in rendered code
-/
- linkTargets : TraverseState → LinkTargets := TraverseState.localTargets
+ linkTargets : TraverseState → LinkTargets Manual.TraverseContext := TraverseState.localTargets
def ensureDir (dir : System.FilePath) : IO Unit := do
@@ -270,7 +272,9 @@ def traverse (logError : String → IO Unit) (text : Part Manual) (config : Conf
if config.verbose then
IO.println "Initializing extensions"
let extensionImpls ← readThe ExtensionImpls
- state := state.setDomainTitle sectionDomain "Sections or chapters of the manual"
+ state := state
+ |>.setDomainTitle sectionDomain "Sections or chapters of the manual"
+ |>.addQuickJumpMapper sectionDomain sectionDomainMapper
for ⟨_, b⟩ in extensionImpls.blockDescrs do
if let some descr := b.get? BlockDescr then
state := descr.init state
@@ -337,7 +341,7 @@ partial def toc (depth : Nat) (opts : Html.Options IO)
(ctxt : TraverseContext)
(state : TraverseState)
(definitionIds : NameMap String)
- (linkTargets : LinkTargets) :
+ (linkTargets : LinkTargets Manual.TraverseContext) :
Part Manual → StateT (State Html) (ReaderT ExtensionImpls IO) Html.Toc
| .mk title sTitle «meta» _ sub => do
let titleHtml ← Html.seq <$> title.mapM (Manual.toHtml (m := ReaderT ExtensionImpls IO) opts.lift ctxt state definitionIds linkTargets {} ·)
@@ -439,7 +443,7 @@ def emitXrefs (toc : List Html.Toc) (dir : System.FilePath) (state : TraverseSta
section
open Search
-def addSearchIndex (state : TraverseState) (ctx : TraverseContext) (logError : String → IO Unit) (doc : Part Manual) : IO TraverseState := do
+def emitSearchIndex (dir : System.FilePath) (state : TraverseState) (ctx : TraverseContext) (logError : String → IO Unit) (doc : Part Manual) : IO Unit := do
have : Indexable Manual := {
partHeader p := do
let ctxt ← IndexM.traverseContext
@@ -461,12 +465,46 @@ def addSearchIndex (state : TraverseState) (ctx : TraverseContext) (logError : S
}
match Verso.Search.mkIndex doc ctx with
- | .error e => logError e; return state
+ | .error e => logError e; return ()
| .ok index =>
+ -- Split the index into roughly 150k chunks for faster loading
+ let (index, docs) := index.extractDocs
+ let size := docs.foldl (init := 0) (fun s _ v => s + v.size)
+ let mut docBuckets : HashMap UInt8 (HashMap String Doc) := {}
+ for (ref, content) in docs do
+ let h := bucket ref
+ docBuckets := docBuckets.alter h fun v =>
+ v.getD {} |>.insert ref content
+
+ for (bucket, docs) in docBuckets do
+ let docJson := docs.fold (init := Json.mkObj []) fun json k v => json.setObjVal! k (v.foldr (init := Json.mkObj []) fun k v js => js.setObjVal! k (Json.str v))
+ IO.FS.writeFile (dir / s!"searchIndex_{bucket}.js") s!"window.docContents[{bucket}].resolve({docJson.compress});"
+
let indexJs := "const __verso_searchIndexData = " ++ index.toJson.compress ++ ";\n\n"
let indexJs := indexJs ++ "const __versoSearchIndex = elasticlunr ? elasticlunr.Index.load(__verso_searchIndexData) : null;\n"
+ let indexJs := indexJs ++ "window.docContents = {};\n"
let indexJs := indexJs ++ "window.searchIndex = elasticlunr ? __versoSearchIndex : null;\n"
- return { state with extraJsFiles := state.extraJsFiles.push { filename := "searchIndex.js", contents := indexJs } }
+ IO.FS.writeFile (dir / "searchIndex.js") indexJs
+
+ IO.FS.writeFile (dir / "elasticlunr.min.js") Verso.Output.Html.elasticlunr.js
+
+where
+ -- Not using a proper hash because this needs to be implemented identically in JS
+ bucket (s : String) : UInt8 := Id.run do
+ let mut hash := 0
+ let mut n := 0
+ while h : n < s.utf8ByteSize do
+ hash := hash + s.getUtf8Byte n h
+ n := n + 1
+ return hash
+
+
+def emitSearchBox (dir : System.FilePath) (domains : DomainMappers) : IO Unit := do
+ ensureDir dir
+ for (file, contents) in searchBoxCode do
+ IO.FS.writeBinFile (dir / file) contents
+ IO.FS.writeFile (dir / "domain-mappers.js") (domains.toJs.pretty (width := 70))
+ IO.FS.writeFile (dir / "domain-display.css") domains.quickJumpCss
end
@@ -485,19 +523,20 @@ def emitHtmlSingle
(text : Part Manual) : ReaderT ExtensionImpls IO (Part Manual × TraverseState) := do
let dir := config.destination.join "html-single"
ensureDir dir
- let (traverseOut, st) ← emitContent dir .empty
- IO.FS.writeFile (dir.join "-verso-docs.json") (toString st.dedup.docJson)
- pure traverseOut
+ let ((text, state), htmlState) ← emitContent dir .empty
+ IO.FS.writeFile (dir.join "-verso-docs.json") (toString htmlState.dedup.docJson)
+ emitSearchBox (dir / "-verso-search") state.quickJump
+ emitSearchIndex (dir / "-verso-search") state {logError, draft := config.draft} logError text
+ pure (text, state)
where
emitContent (dir : System.FilePath) : StateT (State Html) (ReaderT ExtensionImpls IO) (Part Manual × TraverseState) := do
let (text, state) ← traverse logError text {config with htmlDepth := 0}
- let state ← addSearchIndex state {logError, draft := config.draft} logError text
let authors := text.metadata.map (·.authors) |>.getD []
let authorshipNote := text.metadata.bind (·.authorshipNote)
let _date := text.metadata.bind (·.date) |>.getD "" -- TODO
let opts : Html.Options IO := {logError := fun msg => logError msg}
let ctxt := {logError}
- let definitionIds := state.definitionIds
+ let definitionIds := state.definitionIds ctxt
let linkTargets := config.linkTargets state
let titleHtml ← Html.seq <$> text.title.mapM (Manual.toHtml opts.lift ctxt state definitionIds linkTargets {})
let introHtml ← Html.seq <$> text.content.mapM (Manual.toHtml opts.lift ctxt state definitionIds linkTargets {})
@@ -562,9 +601,11 @@ def emitHtmlMulti (logError : String → IO Unit) (config : Config)
(text : Part Manual) : ReaderT ExtensionImpls IO (Part Manual × TraverseState) := do
let root := config.destination.join "html-multi"
ensureDir root
- let (traverseOut, st) ← emitContent root {}
- IO.FS.writeFile (root.join "-verso-docs.json") (toString st.dedup.docJson)
- pure traverseOut
+ let ((text, state), htmlState) ← emitContent root {}
+ IO.FS.writeFile (root.join "-verso-docs.json") (toString htmlState.dedup.docJson)
+ emitSearchBox (root / "-verso-search") state.quickJump
+ emitSearchIndex (root / "-verso-search") state {logError, draft := config.draft} logError text
+ pure (text, state)
where
/--
Emits the data used by all pages in the site, such as JS and CSS, and then emits the root page
@@ -572,13 +613,12 @@ where
-/
emitContent (root : System.FilePath) : StateT (State Html) (ReaderT ExtensionImpls IO) (Part Manual × TraverseState) := do
let (text, state) ← traverse logError text config
- let state ← addSearchIndex state {logError, draft := config.draft} logError text
let authors := text.metadata.map (·.authors) |>.getD []
let authorshipNote := text.metadata >>= (·.authorshipNote)
let _date := text.metadata.bind (·.date) |>.getD "" -- TODO
let opts : Html.Options IO := {logError := fun msg => logError msg}
let ctxt := {logError}
- let definitionIds := state.definitionIds
+ let definitionIds := state.definitionIds ctxt
let linkTargets := config.linkTargets state
let toc ← text.subParts.toList.mapM fun p =>
toc config.htmlDepth opts (ctxt.inPart p) state definitionIds linkTargets p
@@ -690,14 +730,13 @@ def Config.addKaTeX (config : Config) : Config :=
licenseInfo := Licenses.KaTeX :: config.licenseInfo
}
-open Verso.Output.Html in
+
/--
-Adds a bundled version of elasticlunr.js to the config.
+Adds search dependencies to the configuration
-/
def Config.addSearch (config : Config) : Config :=
{ config with
- extraJsFiles := config.extraJsFiles.push {filename := "elasticlunr.min.js", contents := elasticlunr.js}
- licenseInfo := Licenses.elasticlunr.js :: config.licenseInfo
+ licenseInfo := [Licenses.fuzzysort, Licenses.w3Combobox, Licenses.elasticlunr.js] ++ config.licenseInfo
}
diff --git a/src/verso-manual/VersoManual/Basic.lean b/src/verso-manual/VersoManual/Basic.lean
index ea19d6d80..85317d7b5 100644
--- a/src/verso-manual/VersoManual/Basic.lean
+++ b/src/verso-manual/VersoManual/Basic.lean
@@ -11,12 +11,14 @@ import Verso.Doc.Html
import Verso.Doc.TeX
import MultiVerso
import MultiVerso.Slug
+import VersoSearch
import VersoManual.LicenseInfo
import VersoManual.Ext
import Verso.Output.Html
import Verso.Output.TeX
import Verso.BEq
+
open Lean (Name Json NameMap ToJson FromJson)
open Std (HashSet HashMap TreeSet)
open Verso.Doc
@@ -35,6 +37,91 @@ inductive Output where
html (depth : Nat)
deriving DecidableEq, BEq, Hashable
+/--
+The font families used when rendering documents.
+
+These font families are specified using CSS variables, so they can be overridden.
+-/
+inductive FontFamily where
+ | /--
+ The font used for ordinary text, customized with the `--verso-text-font-family` CSS variable.
+ -/
+ text
+ | /--
+ The font used for “structural” text, such as headers. Customized with the `--verso-structure-font-family` CSS variable.
+ -/
+ structure
+ | /--
+ The font used for monospace code, customized with the `--verso-code-font-family` CSS variable.
+ -/
+ code
+deriving DecidableEq, Repr, Hashable
+
+namespace FontFamily
+/--
+The CSS variable that is used to style this font.
+-/
+def toCssVar : FontFamily → String
+ | .text => "--verso-text-font-family"
+ | .structure => "--verso-structure-font-family"
+ | .code => "--verso-code-font-family"
+
+/--
+Returns CSS code that styles text using the font family.
+-/
+def toCss (family : FontFamily) : String := s!"font-family: var({family.toCssVar});"
+
+end FontFamily
+
+inductive FontStyle where
+ | normal
+ | italic
+deriving DecidableEq, Repr, Hashable
+
+def FontStyle.toCss (s : FontStyle) : String :=
+ "font-style: " ++
+ match s with
+ | .normal => "normal;"
+ | .italic => "italic;"
+
+inductive FontWeight where
+ | lighter
+ | light
+ | normal
+ | bold
+ | bolder
+ | numeric (weight : Nat) (ok : weight > 0 ∧ weight < 1000 := by omega)
+deriving DecidableEq, Repr, Hashable
+
+def FontWeight.toCss (w : FontWeight) : String :=
+ "font-weight: " ++
+ match w with
+ | .lighter => "lighter;"
+ | .light => "light;"
+ | .normal => "normal;"
+ | .bold => "bold;"
+ | .bolder => "bolder;"
+ | .numeric n _ => s!"{n};"
+
+/-- A specification of a font. -/
+structure Font where
+ family : FontFamily := .text
+ style : FontStyle := .normal
+ weight : FontWeight := .normal
+deriving DecidableEq, Repr, Hashable
+
+/-- CSS code for a font. -/
+def Font.toCss (font : Font) : String :=
+ " " ++ font.family.toCss ++ "\n" ++
+ " " ++ font.style.toCss ++ "\n" ++
+ " " ++ font.weight.toCss ++ "\n"
+
+open Verso.Search in
+defmethod DomainMapper.setFont (mapper : DomainMapper) (font : Font) : DomainMapper :=
+ { mapper with
+ quickJumpCss :=
+ s!"#search-wrapper .{mapper.className} " ++ "{\n" ++ font.toCss ++ "}\n"
+ }
/--
Tags are used to refer to parts through tables of contents, cross-references, and the like.
@@ -147,6 +234,7 @@ instance : ForIn m Domains (Name × Domain) :=
def StringSet := HashSet String
+open Verso.Search in
structure TraverseState where
tags : HashMap Tag InternalId := {}
externalTags : HashMap InternalId Link := {}
@@ -157,6 +245,7 @@ structure TraverseState where
extraJs : HashSet String := {}
extraJsFiles : Array JsFile := #[]
extraCssFiles : Array (String × String) := #[]
+ quickJump : DomainMappers := {}
licenseInfo : HashSet LicenseInfo := {}
private contents : NameMap Json := {}
@@ -191,6 +280,8 @@ local instance [BEq α] [Hashable α] : BEq (HashSet α) where
local instance [BEq α] [Ord α] : BEq (TreeSet α) where
beq := ptrEqThen fun xs ys => xs.size == ys.size && xs.all (ys.contains ·)
+local instance [BEq α] [Hashable α] [BEq β] : BEq (HashMap α β) where
+ beq := ptrEqThen fun xs ys => xs.size == ys.size && xs.all (ys[·]?.isEqSome ·)
instance : BEq TraverseState where
beq := ptrEqThen fun x y =>
@@ -208,6 +299,7 @@ instance : BEq TraverseState where
x.extraJs == y.extraJs &&
x.extraJsFiles == y.extraJsFiles &&
x.extraCssFiles == y.extraCssFiles &&
+ x.quickJump == y.quickJump &&
ptrEqThen' x.contents y.contents (fun c1 c2 =>
c1.size == c2.size &&
c1.all (c2.find? · |>.isEqSome ·)) &&
@@ -246,6 +338,10 @@ def setDomainTitle (state : TraverseState) (domain : Name) (title : String) : Tr
def setDomainDescription (state : TraverseState) (domain : Name) (description : String) : TraverseState :=
{state with domains := state.domains.insert domain {state.domains.find? domain |>.getD {} with description := some description}}
+open Verso.Search in
+def addQuickJumpMapper (state : TraverseState) (domain : Name) (domainMapper : DomainMapper) : TraverseState :=
+ { state with quickJump := state.quickJump.insert domain.toString domainMapper }
+
def htmlId (state : TraverseState) (id : InternalId) : Array (String × String) :=
if let some {htmlId, ..} := state.externalTags[id]? then
#[("id", htmlId.toString)]
@@ -261,7 +357,33 @@ structure Block where
name : Name := by exact decl_name%
id : Option InternalId := none
data : Json := Json.null
-deriving BEq, Hashable, ToJson, FromJson
+ /--
+ A registry for properties that can be used to create ad-hoc protocols for coordination between
+ block elements in extensions.
+ -/
+ properties : Lean.NameMap String := {}
+deriving ToJson, FromJson
+
+section
+local instance : Repr Json := ⟨fun v _ => s!"json%" ++ v.render ⟩
+deriving instance Repr for Block
+end
+
+
+instance : BEq Block where
+ beq
+ | ⟨n1, i1, d1, p1⟩, ⟨n2, i2, d2, p2⟩ =>
+ n1 == n2 &&
+ i1 == i2 &&
+ ptrEqThen' d1 d2 (· == ·) &&
+ ptrEqThen' p1 p2 fun x y =>
+ x.size == y.size && x.all (fun k v => y.find? k |>.isEqSome v)
+
+instance : Hashable Block where
+ hash
+ | ⟨n, i, d, p⟩ =>
+ have : Ord (Name × String) := Ord.lex ⟨Name.quickCmp⟩ inferInstance
+ mixHash (hash n) <| mixHash (hash i) <| mixHash (hash d) (hash p.toArray.qsortOrd)
structure Inline where
name : Name := by exact decl_name%
@@ -307,11 +429,24 @@ structure PartHeader where
metadata : Option PartMetadata
deriving Repr
+inductive BlockContext where
+ | para
+ | code
+ | ul
+ | ol (start : Int)
+ | dl
+ | blockquote
+ | concat
+ | other (container : Manual.Block)
+deriving Repr
+
structure TraverseContext where
/-- The current URL path - will be [] for non-HTML output or in the root -/
path : Path := #[]
/-- The path from the root to the current header -/
headers : Array PartHeader := #[]
+ /-- The path from the current header to the current block -/
+ blockContext : Array BlockContext := #[]
/-- Whether the current build is a draft (used for hiding TODOs, etc from public builds) -/
draft : Bool := false
logError : String → IO Unit
@@ -380,12 +515,26 @@ instance : FromJson (Genre.Inline Manual) := inferInstanceAs (FromJson Manual.In
namespace Manual
+def BlockContext.ofBlock (block : Doc.Block Manual) : BlockContext :=
+ match block with
+ | .para .. => .para
+ | .code .. => .code
+ | .ul .. => .ul
+ | .ol start .. => .ol start
+ | .dl .. => .dl
+ | .blockquote .. => .blockquote
+ | .concat .. => .concat
+ | .other container .. => .other container
+
def PartHeader.ofPart (part : Part Manual) : PartHeader :=
{titleString := part.titleString, metadata := part.metadata}
def TraverseContext.inPart (self : TraverseContext) (part : Part Manual) : TraverseContext :=
{self with headers := self.headers.push <| .ofPart part}
+def TraverseContext.inBlock (self : TraverseContext) (block : Doc.Block Manual) : TraverseContext :=
+ { self with blockContext := self.blockContext.push (.ofBlock block) }
+
def TraverseContext.sectionNumber (self : TraverseContext) : Array (Option Numbering) :=
self.headers.map (·.metadata |>.getD {} |>.assignedNumber)
@@ -687,6 +836,8 @@ def doc.syntaxKind : Domain := {}
def doc.option : Domain := {}
def doc.tactic.conv : Domain := {}
+
+/-- Names defined as examples -/
-- Protected to avoid taking up good namespace
protected def «example» : Domain := {}
@@ -698,15 +849,121 @@ def optionDomain := ``Verso.Genre.Manual.doc.option
def convDomain := ``Verso.Genre.Manual.doc.tactic.conv
def exampleDomain := ``Verso.Genre.Manual.example
-def TraverseState.definitionIds (state : TraverseState) : NameMap String := Id.run do
+def TraverseState.definitionIds (state : TraverseState) (ctxt : TraverseContext) : NameMap String := Id.run do
+ let exampleBlock := ctxt.blockContext.findSomeRev? fun
+ | .other x => x.properties.find? `Verso.Genre.Manual.exampleDefContext
+ | _ => none
+ let exampleDeco := exampleBlock.map (s!" (in {·})")
if let some examples := state.domains.find? exampleDomain then
let mut idMap := {}
for (x, _) in examples.objects do
- if let .ok { htmlId := slug, .. } := state.resolveDomainObject exampleDomain x then
- idMap := idMap.insert x.toName slug.toString
+ let afterSpace := x.dropWhile (· != ' ')
+ if exampleDeco.isEqSome afterSpace then
+ if let .ok { htmlId := slug, .. } := state.resolveDomainObject exampleDomain x then
+ idMap := idMap.insert (x.takeWhile (· != ' ') |>.toName) slug.toString
+ else if afterSpace.isEmpty then
+ if let .ok { htmlId := slug, .. } := state.resolveDomainObject exampleDomain x then
+ idMap := idMap.insert x.toName slug.toString
return idMap
else return {}
+open Verso.Search in
+/--
+Quick jump configuration for definitions in examples
+-/
+def exampleDomainMapper : DomainMapper := {
+ displayName := "Example Definition",
+ className := "example-def",
+ -- This is a bit of a hack. Examples with repeated names should really get differing canonical
+ -- names, but it's unclear what to use for them. Perhaps it should be the concatenated tags of the
+ -- containing sections, with a sequence number in case of further duplication? For now, this
+ -- fairly complicated mapper does the job. It'd also be good to have a way to show metadata in the
+ -- quick-jump box, with different styling.
+ dataToSearchables :=
+ "(domainData) => {
+ const byName = Object.entries(domainData.contents).flatMap(([key, value]) =>
+ value.map(v => ({
+ context: v.data[`${v.address}#${v.id}`].context,
+ name: v.data[`${v.address}#${v.id}`].display,
+ address: `${v.address}#${v.id}`
+ }))).reduce((acc, obj) => {
+ const key = obj.name;
+ if (!acc.hasOwnProperty(key)) acc[key] = [];
+ acc[key].push(obj);
+ return acc;
+ }, {})
+ return Object.entries(byName).flatMap(([key, value]) => {
+ if (value.length === 0) { return []; }
+ const firstCtxt = value[0].context;
+ let prefixLength = 0;
+ for (let i = 0; i < firstCtxt.length; i++) {
+ if (value.every(v => i < v.context.length && v.context[i] === firstCtxt[i])) {
+ prefixLength++;
+ } else break;
+ }
+ return value.map((v) => ({
+ searchKey: v.context.slice(prefixLength).concat(v.name).join(' › '),
+ address: v.address,
+ domainId: 'Verso.Genre.Manual.example',
+ ref: value
+ }));
+ });
+}"
+ : DomainMapper }.setFont { family := .code }
+
+section
+
+open SubVerso.Highlighting
+
+/--
+Extracts all names that are marked as definition sites, with both their occurrence in the source and
+the underlying name.
+-/
+partial def definedNames : Highlighted → Array (Name × String)
+ | .token ⟨.const n _ _ true, s⟩ => #[(n, s)]
+ | .token _ => #[]
+ | .span _ hl | .tactics _ _ _ hl => definedNames hl
+ | .seq hls => hls.map definedNames |>.foldl (· ++ ·) #[]
+ | .text .. | .point .. | .unparsed .. => #[]
+
+variable [Monad m] [MonadReader TraverseContext m] [MonadStateOf TraverseState m]
+
+/--
+Saves a set of example definitions to the xref database with the expected metadata.
+-/
+def saveExampleDefs (id : InternalId) (definedNames : Array (Name × String)) : m Unit := do
+ let key := (ToJson.toJson id).compress
+ let assignedIds : Option (Except String Json) := (← get).get? `Verso.Genre.Manual.saveExampleDefs
+ let assignedIds := assignedIds.bind (·.toOption) |>.getD (Json.mkObj [])
+ let mut theseIds := if let .ok v@(.obj _) := assignedIds.getObjVal? key then v else Json.mkObj []
+
+ let exampleBlock := (← read).blockContext.findSomeRev? fun
+ | .other x => x.properties.find? `Verso.Genre.Manual.exampleDefContext
+ | _ => none
+ let context := (← read).headers.map (·.titleString)
+ let context := exampleBlock.map context.push |>.getD context
+ for (d, s) in definedNames do
+ if d.isAnonymous then continue
+ let thisId := theseIds.getObjValAs? InternalId d.toString |>.toOption
+ let thisId ←
+ if let some i := thisId then pure i
+ else
+ let i ← freshId
+ theseIds := theseIds.setObjValAs! d.toString i
+ pure i
+ let d :=
+ if let some ex := exampleBlock then s!"{d} (in {ex})" else d.toString
+ let path ← (·.path) <$> read
+ let _ ← externalTag thisId path d
+ modify (·.saveDomainObject exampleDomain d thisId)
+ if let some link := (← get).externalTags[thisId]? then
+ modify (·.modifyDomainObjectData exampleDomain d fun v =>
+ let v := if let .obj _ := v then v else .obj {}
+ v.setObjVal! link.link (json%{"context": $context, "display": $s}))
+ let assignedIds := assignedIds.setObjVal! key theseIds
+ modify (·.set `Verso.Genre.Manual.saveExampleDefs assignedIds)
+end
+
def TraverseState.linksFromDomain
(domain : Name) (canonicalName : String)
(shortDescription description : String)
@@ -714,23 +971,30 @@ def TraverseState.linksFromDomain
state.resolveDomainObject domain canonicalName |>.toOption |>.toArray |>.map fun l =>
{ shortDescription, description, href := l.link }
-def TraverseState.localTargets (state : TraverseState) : Code.LinkTargets where
- const := fun x =>
+def TraverseState.exampleLinks (name : String) (state : TraverseState) (ctxt? : Option TraverseContext) : Array Code.CodeLink := Id.run do
+ let exampleBlock := ctxt?.bind (·.blockContext.findSomeRev? fun
+ | .other x => x.properties.find? `Verso.Genre.Manual.exampleDefContext
+ | _ => none)
+ let name := exampleBlock.map (s!"{name} (in {·})") |>.getD name
+ -- There's no `x` in the tooltip on the next line to avoid revealing suppressed namespaces
+ state.linksFromDomain exampleDomain name "def" s!"Definition of example"
+
+def TraverseState.localTargets (state : TraverseState) : Code.LinkTargets Manual.TraverseContext where
+ const := fun x ctxt? =>
state.linksFromDomain docstringDomain x.toString "doc" s!"Documentation for {x}" ++
- state.linksFromDomain exampleDomain x.toString "def" s!"Definition of example {x}"
- option := fun x =>
+ state.exampleLinks x.toString ctxt?
+ option := fun x _ctxt? =>
state.linksFromDomain optionDomain x.toString "doc" s!"Documentation for option {x}"
- keyword := fun k =>
+ keyword := fun k _ctxt? =>
state.linksFromDomain tacticDomain k.toString "doc" "Documentation for tactic" ++
state.linksFromDomain syntaxKindDomain k.toString "doc" "Documentation for syntax"
-
-def TraverseState.remoteTargets (state : TraverseState) : Code.LinkTargets where
- const := fun x =>
+def TraverseState.remoteTargets (state : TraverseState) : Code.LinkTargets Manual.TraverseContext where
+ const := fun x _ctxt? =>
fromRemoteDomain docstringDomain x.toString (s!"doc ({·})") (s!"Documentation for {x} in {·}")
- option := fun x =>
+ option := fun x _ctxt? =>
fromRemoteDomain optionDomain x.toString (s!"doc ({·})") (s!"Documentation for option {x} in {·}")
- keyword := fun k =>
+ keyword := fun k _ctxt? =>
fromRemoteDomain tacticDomain k.toString (s!"doc ({·})") (s!"Documentation for tactic in {·}") ++
fromRemoteDomain syntaxKindDomain k.toString (s!"doc ({·})") (s!"Documentation for syntax in {·}")
where
@@ -759,9 +1023,26 @@ def sectionString (ctxt : TraverseContext) : Option String :=
def sectionDomain := `Verso.Genre.Manual.section
+open Verso.Search in
+def sectionDomainMapper : DomainMapper := {
+ displayName := "Section",
+ className := "section-domain",
+ dataToSearchables :=
+ "(domainData) =>
+ Object.entries(domainData.contents).map(([key, value]) => ({
+ searchKey: `${value[0].data.sectionNum} ${value[0].data.title}`,
+ address: `${value[0].address}#${value[0].id}`,
+ domainId: 'Verso.Genre.Manual.section',
+ ref: value,
+ }))"
+ : DomainMapper }.setFont { family := .structure, weight := .bold }
+
instance : TraversePart Manual where
inPart p := (·.inPart p)
+instance : TraverseBlock Manual where
+ inBlock b := (·.inBlock b)
+
instance : Traverse Manual TraverseM where
part p :=
if p.metadata.isNone then pure (some {}) else pure none
@@ -854,7 +1135,7 @@ instance : Traverse Manual TraverseM where
else pure (part |>.withMetadata «meta» |>.withSubparts subs)
genreBlock
- | ⟨name, id?, data⟩, content => do
+ | ⟨name, id?, data, props⟩, content => do
if let some id := id? then
if let some impl := (← readThe ExtensionImpls).getBlock? name then
for js in impl.extraJs do
@@ -877,7 +1158,7 @@ instance : Traverse Manual TraverseM where
else
-- Assign a fresh ID if there is none. It can then be used on the next traversal pass.
let id ← freshId
- pure <| some <| Block.other ⟨name, some id, data⟩ content
+ pure <| some <| Block.other ⟨name, some id, data, props⟩ content
genreInline
| ⟨name, id?, data⟩, content => do
if let some id := id? then
diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean
index ab65ce9e7..3a1abdf67 100644
--- a/src/verso-manual/VersoManual/Docstring.lean
+++ b/src/verso-manual/VersoManual/Docstring.lean
@@ -673,9 +673,9 @@ def internalSignature.descr : BlockDescr where
return {{
- {{← name.toHtml}}
+ {{← name.toHtml (g := Manual)}}
{{← if let some s := signature then do
- pure {{" : " {{← s.toHtml}} }}
+ pure {{" : " {{← s.toHtml (g := Manual)}} }}
else pure .empty}}
@@ -704,7 +704,7 @@ def inheritance.descr : BlockDescr where
pure {{
{{← if inheritedFrom.isSome then do
pure {{
@@ -738,7 +738,7 @@ def fieldSignature.descr : BlockDescr where
"Inherited from "
{{ ← parents.mapM fun p => do
- pure {{