feat: improve cache headers for Verso search page (#839)

This PR adds Netlify header rules that cause the content-addressed parts
of the search index to be permanently cached, so clients don't need to
do an HTTP round-trip after having downloaded them. A profile in Chrome
showed a significant improvement.

Author: david-christiansen

.github/workflows/ci.yml

@@ -147,6 +147,17 @@ jobs:
               run: |
                   ./generate-html.sh --mode preview --draft --output _out/draft-site
 
+            # Drop deploy/netlify-headers as _headers at each possible Netlify
+            # publish-dir root so hashed search-index buckets can be cached
+            # immutably. See deploy/netlify-headers for the rules.
+            - name: Install Netlify cache headers
+              run: |
+                  for dir in _out/site _out/site/reference _out/html-multi _out/draft-site _out/draft/html-multi; do
+                      if [ -d "$dir" ]; then
+                          cp deploy/netlify-headers "$dir/_headers"
+                      fi
+                  done
+
             - name: Report status to Lean PR
               if: always() && github.repository == 'leanprover/reference-manual'
               shell: bash

Manual/Meta/Diagram.lean

@@ -21,214 +21,6 @@ open Verso.Genre.Manual.InlineLean.Scopes (getScopes runWithOpenDecls runWithVar
 
 namespace Manual
 
-section BlockExtension
-
-block_extension Block.diagram (svg : String) (width : String) (inline : Bool) where
-  data := Json.arr #[.str svg, .str width, .bool inline]
-  extraCss := [
-    r#"
-.diagram svg text[font-family="text"] {
-  font-family: var(--verso-text-font-family);
-}
-.diagram svg text[font-family="monospace"] {
-  font-family: var(--verso-code-font-family);
-}
-"#
-  ]
-  traverse _ _ _ := pure none
-  toHtml :=
-    open Verso.Output.Html in
-    some <| fun _ _ _ data _ => do
-      let .arr #[.str svgStr, .str w, .bool inl] := data
-        | HtmlT.logError "Expected three-element JSON for diagram" *> pure .empty
-      let style := "width: " ++ w ++ if inl then "; display: inline-block; vertical-align: middle" else ""
-      pure {{
-        <div class="diagram" style={{style}}>
-          {{Html.text false svgStr}}
-        </div>
-      }}
-  usePackages := ["svg"]
-  toTeX :=
-    some <| fun _ _ id data _ => do
-      let .arr #[.str svgStr, .str w, .bool inl] := data
-        | TeX.logError "Expected three-element JSON for diagram" *> pure .empty
-      let filename := s!"diagram-{id}.svg"
-      IO.FS.writeFile filename svgStr
-      let widthOpt := if w == "100%" then "width=\\textwidth" else s!"width={w}"
-      if inl then
-        pure (.raw s!"\\includesvg[{widthOpt}]\{{filename}}")
-      else
-        pure (.raw s!"\\begin\{center}\\includesvg[{widthOpt}]\{{filename}}\\end\{center}\n")
-
-block_extension Block.row (alignItems : String) where
-  data := Json.str alignItems
-  traverse _ _ _ := pure none
-  toHtml :=
-    open Verso.Output.Html in
-    some <| fun _ blockHtml _ data content => do
-      let .str ai := data | HtmlT.logError "Expected string JSON for row" *> pure .empty
-      let style := s!"display: flex; flex-wrap: wrap; align-items: {ai}; gap: 1em;"
-      pure {{
-        <div class="diagram-row" style={{style}}>
-          {{← content.mapM blockHtml}}
-        </div>
-      }}
-  toTeX :=
-    some <| fun _ go _ _ content => do
-      pure <| .seq <| ← content.mapM go
-
-end BlockExtension
-
-
-/--
-Parses a decimal float string (e.g. `"3.14"`, `"-0.5"`).
-Returns `none` for unrecognized formats.
--/
-private def parseFloatStr (s : String) : Option Float :=
-  let (neg, s) : Bool × String :=
-    if s.startsWith "-" then (true, (s.drop 1).copy) else (false, s)
-  let result : Option Float := match s.splitOn "." with
-    | [intStr] =>
-      intStr.toNat?.map fun n => Float.ofScientific n true 0
-    | [intStr, fracStr] =>
-      intStr.toNat?.bind fun n =>
-        if fracStr.isEmpty then some (Float.ofScientific n true 0)
-        else fracStr.toNat?.map fun frac =>
-          Float.ofScientific n true 0 + Float.ofScientific frac true fracStr.length
-    | _ => none
-  result.map fun f => if neg then -f else f
-
-/--
-A `ValDesc` for float arguments: accepts integer numerals (e.g. `1`) and
-string literals containing decimal numbers (e.g. `"0.08"`).
--/
-private def floatValDesc [Monad m] [MonadError m] : ValDesc m Float where
-  description := doc!"a number"
-  signature := .Num ∪ .String
-  get
-    | .num n => pure (Float.ofScientific n.getNat true 0)
-    | .str s =>
-      match parseFloatStr s.getString with
-      | some f => pure f
-      | none => throwError "Expected a number, got {repr s.getString}"
-    | .name n => throwError "Expected a number, got identifier {n.getId}"
-
-section Config
-
-variable [Monad m] [MonadInfoTree m] [MonadLiftT CoreM m] [MonadEnv m] [MonadError m]
-
-structure DiagramConfig where
-  width : Option String
-  scale : Option Float
-  inline : Bool
-
-def DiagramConfig.parse : ArgParse m DiagramConfig :=
-  DiagramConfig.mk <$> .named' `width true <*> .named `scale floatValDesc true <*> .flag `inline false
-
-instance : FromArgs DiagramConfig m := ⟨DiagramConfig.parse⟩
-
-structure RowConfig where
-  align : String
-
-def RowConfig.parse : ArgParse m RowConfig :=
-  RowConfig.mk <$> .namedD' `align "top"
-
-instance : FromArgs RowConfig m := ⟨RowConfig.parse⟩
-
-end Config
-
-open Illuminate in
-/--
-Returns the viewBox width (in diagram units) of an SVG diagram, using the same
-padding as `Illuminate.diagramToSvg` (padding = 5). Used to compute an em-based
-CSS width when the `scale` parameter is specified. Returns 0 for empty diagrams.
--/
-def diagramViewBoxWidth (d : Diagram SVG) : Float :=
-  match d.getEnvelope with
-  | .empty => 0
-  | .nonempty env => env Vec2.west + env Vec2.east + 10
-
-open Lean.Widget Lean.Elab.Term Lean.Meta Illuminate in
-private meta unsafe def diagramExpanderUnsafe (config : DiagramConfig) (str : StrLit) :
-    DocElabM Term := withoutAsync do
-  if config.width.isSome && config.scale.isSome then
-    throwErrorAt str "Cannot specify both 'width' and 'scale' in a diagram block"
-
-  let altStr ← parserInputString str
-
-  match Parser.runParserCategory (← getEnv) `term altStr (← getFileName) with
-  | .error e => throwErrorAt str e
-  | .ok stx =>
-    let (svgStr, diagramWidth) ← runWithOpenDecls <| runWithVariables fun _vars => do
-      let diaTy ← Meta.mkAppM ``Illuminate.Diagram #[.const ``Illuminate.SVG []]
-      let e ← Elab.Term.elabTerm stx (some diaTy)
-      Term.synthesizeSyntheticMVarsNoPostponing
-      let e ← instantiateMVars e
-
-      -- Don't evaluate if elaboration produced errors
-      if (← Core.getMessageLog).hasErrors then
-        return ("", 0)
-
-      -- Evaluate to get SVG string
-      let svgExpr := mkApp (mkConst ``Illuminate.diagramToSvg) e
-      let svgStr ← evalExpr String (mkConst ``String) svgExpr
-
-      -- Compute diagram width from envelope if scale is needed
-      let diagramWidth : Float ← if config.scale.isSome then do
-        let widthExpr := mkApp (mkConst ``Manual.diagramViewBoxWidth) e
-        evalExpr Float (mkConst ``Float) widthExpr
-      else
-        pure 0
-
-      -- Store diagram for widget RPC re-evaluation
-      let env ← getEnv
-      let opts ← getOptions
-      let id ← Illuminate.nextDiagramId.modifyGet fun n => (n, n + 1)
-      let sd : Illuminate.StoredDiagram := {
-        env, opts, expr := e, gadgets := #[], regions := {}, returnsDwi := false
-      }
-      Illuminate.diagramStore.modify (·.push (id, sd))
-
-      -- Attach widget with CSS variable defaults for the infoview context
-      let widgetSvg := "<div style=\"--verso-text-font-family: sans-serif; --verso-code-font-family: monospace;\">" ++
-        "<style>svg text[font-family=\"text\"] { font-family: var(--verso-text-font-family); } " ++
-        "svg text[font-family=\"monospace\"] { font-family: var(--verso-code-font-family); }</style>" ++
-        svgStr ++ "</div>"
-      let props : Json := .mkObj [
-        ("exprId", toJson id),
-        ("initialSvg", .str widgetSvg),
-        ("parameters", .arr #[])]
-      savePanelWidgetInfo Illuminate.diagramWidget.javascriptHash.val (pure props) str
-
-      pure (svgStr, diagramWidth)
-
-    let cssWidth : String := match config.scale with
-      | none => config.width.getD "100%"
-      | some scale =>
-        if diagramWidth > 0 then s!"{diagramWidth * scale}em" else "100%"
-
-    ``(Block.other (Block.diagram $(quote svgStr) $(quote cssWidth) $(quote config.inline)) #[Block.code $(quote str.getString)])
-
-open Lean.Widget Lean.Elab.Term Lean.Meta Illuminate in
-@[implemented_by diagramExpanderUnsafe]
-private opaque diagramExpanderImpl (config : DiagramConfig) (str : StrLit) : DocElabM Term
-
-@[code_block]
-def diagram : CodeBlockExpanderOf DiagramConfig
-  | config, str => diagramExpanderImpl config str
-
-/-- Arranges the contained blocks in a horizontal row using flexbox. -/
-@[directive]
-def row : DirectiveExpanderOf RowConfig
-  | config, stxs => do
-    let alignItems ← match config.align with
-      | "top"    => pure "flex-start"
-      | "middle" => pure "center"
-      | "bottom" => pure "flex-end"
-      | other    => throwError "Expected 'top', 'middle', or 'bottom' for 'align', got {repr other}"
-    let args ← stxs.mapM elabBlock
-    ``(Block.other (Block.row $(quote alignItems)) #[ $[ $args ],* ])
-
 namespace Diagram
 open Illuminate
 

Manual/RecursiveDefs/CoinductivePredicates.lean

@@ -377,7 +377,7 @@ languageEquivalent.coinduct {Q A Q' : Type}
 
 It can be used to prove that these two DFAs have equivalent languages:
 :::row (align := "top")
-```diagram (scale := "0.1") +inline
+```diagram (cssScale := "0.1") +inline
 open Illuminate in
 let cfg : StateDiagramConfig := {}
 cfg.start 0 |>.atop
@@ -388,7 +388,7 @@ cfg.start 0 |>.atop
 (cfg.edge 0 1 "b")
 ```
 
-```diagram (scale := "0.1") +inline
+```diagram (cssScale := "0.1") +inline
 open Illuminate in
 let cfg : StateDiagramConfig := {}
 cfg.start 0 |>.atop

deploy/netlify-headers

@@ -0,0 +1,17 @@
+# Netlify _headers rules for the reference manual.
+#
+# Hashed search-index bucket files are content-addressed: their
+# filenames include a per-build version string
+# (searchIndex_<bucket>.<version>.js), so every deploy produces fresh
+# filenames and old ones can be cached forever. The entry-point
+# searchIndex.js is deliberately *not* listed here, so it revalidates
+# normally and clients pick up the new version string on each deploy.
+
+/-verso-search/searchIndex_*.*.js
+  Cache-Control: public, max-age=31536000, immutable
+
+/reference/-verso-search/searchIndex_*.*.js
+  Cache-Control: public, max-age=31536000, immutable
+
+/tutorials/-verso-search/searchIndex_*.*.js
+  Cache-Control: public, max-age=31536000, immutable

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "06759f86fe54122ba3c081f40ed1cd24cffb8832",
+   "rev": "8bcbd2b8723307c329c12997a0c16a6ac174d3e9",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "86210d4ad1b08b086d0bd638637a75246523dbb8",
+   "rev": "a456461b368b71d2accd95234832cd9c174b5437",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",