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 f49eae42c..a6773f9b4 100644 --- a/lake-manifest.json +++ b/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", 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