feat: search box (#241)

Adds a search box that uses Verso's internal metadata for a live index.

---------

Co-authored-by: Jakob Vase <[email protected]>

.github/workflows/check-search-tsc.yml

@@ -0,0 +1,19 @@
+name: Check for copyright headers
+
+on: [pull_request]
+
+jobs:
+  check-lean-files:
+    runs-on: ubuntu-latest
+    steps:
+    - name: Install TypeScript
+      run: |
+        sudo apt update && sudo apt install node-typescript
+
+    - uses: actions/checkout@v4
+
+    - name: Type check the search bar code
+      run: |
+        cd static/search
+        tsc --noEmit -p jsconfig.json
+

.vale/scripts/rewrite_html.py

@@ -51,6 +51,10 @@ def process_html_file(filepath, output_filepath):
         for inner in element.contents:
             inner.replace_with(inner.get_text())
 
+    # Delete software license info
+    for element in soup.find_all("section", class_="license-info"):
+        element.decompose()
+
     # Ensure the output directory exists
     os.makedirs(os.path.dirname(output_filepath), exist_ok=True)
 

Main.lean

@@ -9,17 +9,125 @@ import VersoManual
 
 open Verso.Genre.Manual
 
+open Verso.Output.Html in
+def searchModule := {{
+    <script type="module" src="/static/search/search-init.js"></script>
+  }}
+
+
+def KaTeXLicense : LicenseInfo where
+  identifier := "MIT"
+  dependency := "KaTeX"
+  howUsed := "KaTeX is used to render mathematical notation."
+  link := "https://katex.org/"
+  text := #[(some "The MIT License", text)]
+where
+  text := r#"
+Copyright (c) 2013-2020 Khan Academy and other contributors
+
+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 addKaTeX (config : Config) : Config :=
+  {config with
+    extraCss := "/static/katex/katex.min.css" :: config.extraCss,
+    extraJs := "/static/katex/katex.min.js" :: "/static/math.js" :: config.extraJs,
+    licenseInfo := KaTeXLicense :: config.licenseInfo
+  }
+
+
+def fuzzysortLicense : LicenseInfo where
+  identifier := "MIT"
+  dependency := "fuzzysort v3.1.0"
+  howUsed := "The fuzzysort library is used in the search box to quickly filter results."
+  link := "https://github.com/farzher/fuzzysort"
+  text := #[(some "The MIT License", text)]
+where
+  text := r#"
+Copyright (c) 2018 Stephen Kamenar
+
+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 w3ComboboxLicense : LicenseInfo where
+  identifier := "W3C-20150513"
+  dependency := "Editable Combobox With Both List and Inline Autocomplete Example, from the W3C's ARIA Authoring Practices Guide (APG)"
+  howUsed := "The search box component includes code derived from the example code in the linked article from the W3C's ARIA Authoring Practices Guide (APG)."
+  link := "https://www.w3.org/WAI/ARIA/apg/patterns/combobox/examples/combobox-autocomplete-both/"
+  text := #[(some "Software and Document License - 2023 Version", text)]
+where
+  text := r#"Permission to copy, modify, and distribute this work, with or without
+modification, for any purpose and without fee or royalty is hereby granted,
+provided that you include the following on ALL copies of the work or portions
+thereof, including modifications:
+
+ * The full text of this NOTICE in a location viewable to users of the redistributed or derivative work.
+
+ * Any pre-existing intellectual property disclaimers, notices, or terms and conditions. If none exist, the W3C software and document short notice should be included.
+
+ * Notice of any changes or modifications, through a copyright statement on the new code or document such as "This software or document includes material copied from or derived from "Editable Combobox With Both List and Inline Autocomplete Example" at https://www.w3.org/WAI/ARIA/apg/patterns/combobox/examples/combobox-autocomplete-both/. Copyright © 2024 World Wide Web Consortium. https://www.w3.org/copyright/software-license-2023/"
+
+
+"#
 
 def main :=
   manualMain (%doc Manual) (config := config)
 where
-  config := {
+  config := addKaTeX {
     extraFiles := [("static", "static")],
-    extraCss := ["/static/colors.css", "/static/theme.css", "/static/print.css", "/static/fonts/source-serif/source-serif-text.css", "/static/fonts/source-code-pro/source-code-pro.css", "/static/katex/katex.min.css"],
-    extraJs := ["/static/katex/katex.min.js", "/static/math.js", "/static/print.js"],
+    extraCss := [
+      "/static/colors.css",
+      "/static/theme.css",
+      "/static/print.css",
+      "/static/search/search-box.css",
+      "/static/fonts/source-serif/source-serif-text.css",
+      "/static/fonts/source-code-pro/source-code-pro.css",
+    ],
+    extraJs := [
+      -- Search box
+      "/static/search/fuzzysort.js",
+      -- Print stylesheet improvements
+      "/static/print.js"
+    ],
+    extraHead := #[searchModule],
     emitTeX := false,
     emitHtmlSingle := true, -- for proofreading
     logo := some "/static/lean_logo.svg",
     sourceLink := some "https://github.com/leanprover/reference-manual",
     issueLink := some "https://github.com/leanprover/reference-manual/issues"
+    -- Licenses for the search box
+    licenseInfo := [fuzzysortLicense, w3ComboboxLicense]
   }

Manual/BuildTools/Lake/Config.lean

@@ -74,7 +74,7 @@ Field names not used by Lake should not be used to store metadata to be processe
 The top-level contents of `lakefile.toml` specify the options that apply to the package itself, including metadata such as the name and version, the locations of the files in the {tech}[workspace], compiler flags to be used for all {tech}[targets], and
 The only mandatory field is `name`, which declares the package's name.
 
-::::tomlTableDocs "Package Configuration" Lake.PackageConfig skip:=backend skip:=releaseRepo? skip:=buildArchive? skip:=manifestFile skip:=moreServerArgs
+::::tomlTableDocs root "Package Configuration" Lake.PackageConfig skip:=backend skip:=releaseRepo? skip:=buildArchive? skip:=manifestFile skip:=moreServerArgs
 
 :::tomlFieldCategory "Metadata" name version versionTags description keywords homepage license licenseFiles readmeFile reservoir
 These options describe the package.
@@ -294,7 +294,7 @@ There are three kinds of sources:
  * Git repositories, which may be local paths or URLs
  * Local paths
 
-::::tomlTableDocs "Requiring Packages" Lake.Dependency skip:=src? skip := opts skip:=subdir skip:=version?
+::::tomlTableDocs "require" "Requiring Packages" Lake.Dependency skip:=src? skip := opts skip:=subdir skip:=version?
 
 The `path` and `git` fields specify an explicit source for a dependency.
 If neither are provided, then the dependency is fetched from {ref "reservoir"}[Reservoir], or an alternative registry if one has been configured.
@@ -448,7 +448,7 @@ source = {type = "git", url = "https://example.com/example.git"}
 
 Library targets are expected in the `lean_lib` array of tables.
 
-::::tomlTableDocs "Library Targets" Lake.LeanLibConfig skip := backend skip:=globs skip:=nativeFacets
+::::tomlTableDocs "lean_lib" "Library Targets" Lake.LeanLibConfig skip := backend skip:=globs skip:=nativeFacets
 ::::
 
 :::::example "Minimal Library Target"
@@ -522,7 +522,7 @@ If its modules are accessed at elaboration time, they will be compiled to native
 
 ## Executable Targets
 
-:::: tomlTableDocs "Executable Targets" Lake.LeanExeConfig skip := backend skip:=globs skip:=nativeFacets
+:::: tomlTableDocs "lean_exe" "Executable Targets" Lake.LeanExeConfig skip := backend skip:=globs skip:=nativeFacets
 
 ::::
 

Manual/IO.lean

@@ -87,6 +87,9 @@ Without using one of a few clearly-marked unsafe operators, programs have no way
 This ensures that the correct ordering of side effects is preserved, and it ensures that programs that have side effects are clearly marked as such.
 
 ## The `IO`, `EIO` and `BaseIO` Monads
+%%%
+tag := "io-monad"
+%%%
 
 There are two monads that are typically used for programs that interact with the real world:
 
@@ -126,7 +129,10 @@ example : BaseIO = EIO Empty := rfl
 
 {docstring IO.toEIO}
 
-## Errors and Error Handling
+## Errors and Error Handling in `IO`
+%%%
+tag := "io-monad-errors"
+%%%
 
 Error handling in the {lean}`IO` monad uses the same facilities as any other {tech}[exception monad].
 In particular, throwing and catching exceptions uses the methods of the {name}`MonadExceptOf` {tech}[type class].
@@ -193,6 +199,9 @@ Access granted!
 ::::
 
 ### Constructing IO Errors
+%%%
+tag := "io-error-construction"
+%%%
 
 {docstring IO.Error.mkUnsupportedOperation}
 
@@ -248,6 +257,9 @@ Access granted!
 {docstring IO.Error.mkInappropriateTypeFile}
 
 # Control Structures
+%%%
+tag := "io-monad-control"
+%%%
 
 Normally, programs written in {lean}`IO` use {ref "monads-and-do"}[the same control structures as those written in other monads].
 There is one specific {lean}`IO` helper.
@@ -261,10 +273,16 @@ There is one specific {lean}`IO` helper.
 {include 0 Manual.IO.Files}
 
 # Environment Variables
+%%%
+tag := "io-monad-getenv"
+%%%
 
 {docstring IO.getEnv}
 
 # Timing
+%%%
+tag := "io-timing"
+%%%
 
 {docstring IO.sleep}
 
@@ -277,6 +295,9 @@ There is one specific {lean}`IO` helper.
 {docstring IO.addHeartbeats}
 
 # Processes
+%%%
+tag := "io-processes"
+%%%
 
 ## Current Process
 

Manual/Intro.lean

@@ -218,3 +218,11 @@ inductive Even : Nat → Prop where
 {docstring Even}
 
 ::::
+
+# Open-Source Licenses
+%%%
+tag := "dependency-licenses"
+number := false
+%%%
+
+{licenseInfo}

Manual/Language/InductiveTypes.lean

@@ -288,6 +288,13 @@ Instead of writing the constructor's name applied to its arguments, the explicit
 This works in both pattern and expression contexts.
 Providing arguments by name or converting all implicit parameters to explicit parameters with `@` requires using the ordinary constructor syntax.
 
+:::syntax term (title := "Anonymous Constructors")
+Constructors can be invoked anonymously by enclosing their explicit arguments in angle brackets, separated by commas.
+```grammar
+⟨ $_,* ⟩
+```
+:::
+
 ::::example "Anonymous constructors"
 
 :::keepEnv

Manual/Meta/Example.lean

@@ -24,12 +24,12 @@ def Block.example (name : Option String) : Block where
 structure ExampleConfig where
   description : FileMap × Array Syntax
   /-- Name for refs -/
-  name : Option String := none
+  tag : Option String := none
   keep : Bool := false
 
 
 def ExampleConfig.parse [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m] [MonadFileMap m] : ArgParse m ExampleConfig :=
-  ExampleConfig.mk <$> .positional `description .inlinesString <*> .named `name .string true <*> (.named `keep .bool true <&> (·.getD false))
+  ExampleConfig.mk <$> .positional `description .inlinesString <*> .named `tag .string true <*> (.named `keep .bool true <&> (·.getD false))
 
 def prioritizedElab [Monad m] (prioritize : α → m Bool) (act : α  → m β) (xs : Array α) : m (Array β) := do
   let mut out := #[]
@@ -71,7 +71,7 @@ def «example» : DirectiveExpander
         withoutModifyingEnv <| prioritizedElab (isLeanBlock ·) elabBlock contents
     -- Examples are represented using the first block to hold the description. Storing it in the JSON
     -- entails repeated (de)serialization.
-    pure #[← ``(Block.other (Block.example $(quote cfg.name)) #[Block.para #[$description,*], $blocks,*])]
+    pure #[← ``(Block.other (Block.example $(quote cfg.tag)) #[Block.para #[$description,*], $blocks,*])]
 
 @[block_extension «example»]
 def example.descr : BlockDescr where