feat: incorporate upstream search page

.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

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,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "06759f86fe54122ba3c081f40ed1cd24cffb8832",
+   "rev": "3d9cfe72945a378de142bd332691f12a932c6b57",
    "name": "verso",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "search-page",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/illuminate",

lakefile.lean

@@ -10,7 +10,7 @@ open System (FilePath)
 
 require versowebcomponents from git "https://github.com/leanprover/verso-web-components"@"main"
 require illuminate from git "https://github.com/leanprover/illuminate"@"main"
-require verso from git "https://github.com/leanprover/verso.git"@"main"
+require verso from git "https://github.com/leanprover/verso.git"@"search-page"
 
 
 package "verso-manual" where