From 16afbe81256141892d4ab22ea74e4837c88d9de1 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 24 Apr 2026 10:38:55 +0200 Subject: [PATCH 1/4] feat: incorporate upstream search page --- lake-manifest.json | 4 ++-- lakefile.lean | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/lake-manifest.json b/lake-manifest.json index f49eae42c..f07096c38 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,10 +5,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "06759f86fe54122ba3c081f40ed1cd24cffb8832", + "rev": "e6b8172cb1814726965c92f157e33bce8f93cc1f", "name": "verso", "manifestFile": "lake-manifest.json", - "inputRev": "main", + "inputRev": "search-page", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover/illuminate", diff --git a/lakefile.lean b/lakefile.lean index 94ba07876..0dee63596 100644 --- a/lakefile.lean +++ b/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 From 36e1f83d4eeaf31aa28fab2d4f57502ce07650c9 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 24 Apr 2026 11:05:50 +0200 Subject: [PATCH 2/4] try next --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index f07096c38..9ad31f5b7 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "e6b8172cb1814726965c92f157e33bce8f93cc1f", + "rev": "0b68d8d80d9550b7a0392ea2de9ee069f89e7938", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "search-page", From 36188376e9916e0331510fbb71819ad5aa5ad3fa Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 24 Apr 2026 13:28:49 +0200 Subject: [PATCH 3/4] Try smaller index --- lake-manifest.json | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lake-manifest.json b/lake-manifest.json index 9ad31f5b7..e2c867c1e 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "0b68d8d80d9550b7a0392ea2de9ee069f89e7938", + "rev": "8e66840b8efa5b32abbc09e252351f0eff223671", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "search-page", From 9d7c94860848ba622330b4d5edeb619bc3068ca3 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 24 Apr 2026 13:45:44 +0200 Subject: [PATCH 4/4] try smarter search index cache --- .github/workflows/ci.yml | 11 +++++++++++ deploy/netlify-headers | 17 +++++++++++++++++ lake-manifest.json | 2 +- 3 files changed, 29 insertions(+), 1 deletion(-) create mode 100644 deploy/netlify-headers diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 1cdd25af5..240af187c 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/deploy/netlify-headers b/deploy/netlify-headers new file mode 100644 index 000000000..ff3a74abd --- /dev/null +++ b/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_..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 diff --git a/lake-manifest.json b/lake-manifest.json index e2c867c1e..a6773f9b4 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "8e66840b8efa5b32abbc09e252351f0eff223671", + "rev": "3d9cfe72945a378de142bd332691f12a932c6b57", "name": "verso", "manifestFile": "lake-manifest.json", "inputRev": "search-page",