Deploy to Cloudflare Pages (free hosting)

.github/workflows/ci.yaml

@@ -28,10 +28,10 @@ jobs:
   lint_and_test_website:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
-      - uses: actions/setup-node@v3
+      - uses: actions/checkout@v4
+      - uses: actions/setup-node@v4
         with:
-          node-version: 16
+          node-version: 18
       - run: yarn install
         working-directory: ./website
       - run: yarn build

.gitignore

@@ -137,6 +137,8 @@ crawler/parse_cache.*.pkl
 website/public/searchItems.*.json
 website/public/robots.txt
 website/public/sitemap*.xml
+website/public/data/
+website/.vercel/
 
 # misc
 .vscode

website/data/edgeDatabase.ts

@@ -0,0 +1,66 @@
+/**
+ * Edge-compatible data loading for Cloudflare Workers.
+ * Fetches pre-built JSON chunks from static assets via HTTP.
+ */
+import { ChangelogItemData } from "./extractDataFromChangelog";
+import { CommitData, ItemType, LeanVersion } from "./types";
+
+function getSiteUrl(): string {
+  return (
+    process.env.SITE_URL ||
+    process.env.CF_PAGES_URL ||
+    "http://localhost:3000"
+  );
+}
+
+async function sha256Prefix(input: string): Promise<string> {
+  const data = new TextEncoder().encode(input);
+  const hashBuffer = await crypto.subtle.digest("SHA-256", data);
+  const hashArray = Array.from(new Uint8Array(hashBuffer));
+  return hashArray
+    .map((b) => b.toString(16).padStart(2, "0"))
+    .join("")
+    .slice(0, 2);
+}
+
+export async function getCommitEdge(
+  version: LeanVersion,
+  sha: string
+): Promise<CommitData | null> {
+  const prefix = sha.slice(0, 2).toLowerCase();
+  try {
+    const res = await fetch(
+      `${getSiteUrl()}/data/${version}/commits/${prefix}.json`
+    );
+    if (!res.ok) return null;
+    const bucket = (await res.json()) as Record<string, CommitData>;
+    if (bucket[sha]) return bucket[sha];
+    const shortSha = sha.slice(0, 8);
+    for (const [key, commit] of Object.entries(bucket)) {
+      if (key.startsWith(shortSha)) return commit;
+    }
+    return null;
+  } catch {
+    return null;
+  }
+}
+
+export async function getItemEdge(
+  version: LeanVersion,
+  itemType: ItemType,
+  name: string
+): Promise<ChangelogItemData | null> {
+  const prefix = await sha256Prefix(name);
+  try {
+    const res = await fetch(
+      `${getSiteUrl()}/data/${version}/items/${prefix}.json`
+    );
+    if (!res.ok) return null;
+    const bucket = (await res.json()) as Record<string, ChangelogItemData>;
+    const item = bucket[name];
+    if (!item || item.type !== itemType) return null;
+    return item;
+  } catch {
+    return null;
+  }
+}

website/package.json

@@ -8,9 +8,10 @@
     "postbuild": "yarn build:search && yarn build:sitemap",
     "start": "next start",
     "lint": "next lint",
-    "export": "next export",
+    "build:data": "ts-node scripts/buildStaticData.ts",
     "build:sitemap": "next-sitemap",
-    "build:search": "ts-node scripts/buildSearchItems.ts"
+    "build:search": "ts-node scripts/buildSearchItems.ts",
+    "pages:build": "yarn build:data && yarn build:search && npx @cloudflare/next-on-pages"
   },
   "dependencies": {
     "@heroicons/react": "^1.0.6",
@@ -28,6 +29,7 @@
     "remark-gfm": "^3.0.1"
   },
   "devDependencies": {
+    "@cloudflare/next-on-pages": "^1.13.16",
     "@types/lodash": "^4.14.182",
     "@types/node": "18.0.3",
     "@types/react": "18.0.15",
@@ -40,6 +42,7 @@
     "prettier": "^2.7.1",
     "tailwindcss": "^3.1.5",
     "ts-node": "^10.8.2",
-    "typescript": "4.7.4"
+    "typescript": "4.7.4",
+    "vercel": "^50.38.2"
   }
 }

website/pages/v3/changelog/[page].tsx

@@ -11,10 +11,13 @@ import summarizeHeadline from "../../../util/summarizeHeadline";
 
 const PER_PAGE = 50;
 
-export const getStaticPaths: GetStaticPaths = () => ({
-  paths: [],
-  fallback: "blocking",
-});
+export const getStaticPaths: GetStaticPaths = () => {
+  const commitPages = getCommitPages("v3");
+  return {
+    paths: commitPages.map((_, i) => ({ params: { page: String(i + 1) } })),
+    fallback: false,
+  };
+};
 
 interface CommitSummary {
   headline: string;

website/pages/v3/commit/[sha].tsx

@@ -3,10 +3,12 @@ import { GetStaticPaths, GetStaticProps, NextPage } from "next";
 import Link from "next/link";
 import Layout from "../../../components/Layout";
 import MathlibGithubMarkdown from "../../../components/MathlibGithubMarkdown";
-import { getCommit } from "../../../data/database";
+import { getCommitEdge } from "../../../data/edgeDatabase";
 import { ChangeType, CommitData, DiffData } from "../../../data/types";
 import formatTimestamp from "../../../util/formatTimestamp";
 
+export const runtime = "experimental-edge";
+
 export const getStaticPaths: GetStaticPaths = () => ({
   paths: [],
   fallback: "blocking",
@@ -16,11 +18,11 @@ interface CommitProps {
   commit: CommitData;
 }
 
-export const getStaticProps: GetStaticProps<CommitProps> = (context) => {
+export const getStaticProps: GetStaticProps<CommitProps> = async (context) => {
   if (!context.params?.sha || Array.isArray(context.params.sha)) {
     return { notFound: true };
   }
-  const commit = getCommit("v3", context.params.sha);
+  const commit = await getCommitEdge("v3", context.params.sha);
   if (!commit) return { notFound: true };
   return { props: { commit } };
 };

website/pages/v3/def/[name].tsx

@@ -1,9 +1,11 @@
 import { GetStaticPaths, GetStaticProps, NextPage } from "next";
 import { ItemChangeHistory } from "../../../components/ItemChangeHistory";
 import Layout from "../../../components/Layout";
-import { getDef } from "../../../data/database";
+import { getItemEdge } from "../../../data/edgeDatabase";
 import { ChangelogItemData } from "../../../data/extractDataFromChangelog";
 
+export const runtime = "experimental-edge";
+
 export const getStaticPaths: GetStaticPaths = () => ({
   paths: [],
   fallback: "blocking",
@@ -13,11 +15,11 @@ interface DefProps {
   def: ChangelogItemData;
 }
 
-export const getStaticProps: GetStaticProps<DefProps> = (context) => {
+export const getStaticProps: GetStaticProps<DefProps> = async (context) => {
   if (!context.params?.name || Array.isArray(context.params.name)) {
     return { notFound: true };
   }
-  const def = getDef("v3", context.params.name);
+  const def = await getItemEdge("v3", "def", context.params.name);
   if (!def) return { notFound: true };
   return { props: { def } };
 };

website/pages/v3/inductive/[name].tsx

@@ -1,9 +1,11 @@
 import { GetStaticPaths, GetStaticProps, NextPage } from "next";
 import { ItemChangeHistory } from "../../../components/ItemChangeHistory";
 import Layout from "../../../components/Layout";
-import { getInductive } from "../../../data/database";
+import { getItemEdge } from "../../../data/edgeDatabase";
 import { ChangelogItemData } from "../../../data/extractDataFromChangelog";
 
+export const runtime = "experimental-edge";
+
 export const getStaticPaths: GetStaticPaths = () => ({
   paths: [],
   fallback: "blocking",
@@ -13,11 +15,11 @@ interface InductiveProps {
   inductive: ChangelogItemData;
 }
 
-export const getStaticProps: GetStaticProps<InductiveProps> = (context) => {
+export const getStaticProps: GetStaticProps<InductiveProps> = async (context) => {
   if (!context.params?.name || Array.isArray(context.params.name)) {
     return { notFound: true };
   }
-  const inductive = getInductive("v3", context.params.name);
+  const inductive = await getItemEdge("v3", "inductive", context.params.name);
   if (!inductive) return { notFound: true };
   return { props: { inductive } };
 };

website/pages/v3/structure/[name].tsx

@@ -1,9 +1,11 @@
 import { GetStaticPaths, GetStaticProps, NextPage } from "next";
 import { ItemChangeHistory } from "../../../components/ItemChangeHistory";
 import Layout from "../../../components/Layout";
-import { getStructure } from "../../../data/database";
+import { getItemEdge } from "../../../data/edgeDatabase";
 import { ChangelogItemData } from "../../../data/extractDataFromChangelog";
 
+export const runtime = "experimental-edge";
+
 export const getStaticPaths: GetStaticPaths = () => ({
   paths: [],
   fallback: "blocking",
@@ -13,11 +15,11 @@ interface StructureProps {
   structure: ChangelogItemData;
 }
 
-export const getStaticProps: GetStaticProps<StructureProps> = (context) => {
+export const getStaticProps: GetStaticProps<StructureProps> = async (context) => {
   if (!context.params?.name || Array.isArray(context.params.name)) {
     return { notFound: true };
   }
-  const structure = getStructure("v3", context.params.name);
+  const structure = await getItemEdge("v3", "structure", context.params.name);
   if (!structure) return { notFound: true };
   return { props: { structure } };
 };

website/pages/v3/theorem/[name].tsx

@@ -1,9 +1,11 @@
 import { GetStaticPaths, GetStaticProps, NextPage } from "next";
 import { ItemChangeHistory } from "../../../components/ItemChangeHistory";
 import Layout from "../../../components/Layout";
-import { getTheorem } from "../../../data/database";
+import { getItemEdge } from "../../../data/edgeDatabase";
 import { ChangelogItemData } from "../../../data/extractDataFromChangelog";
 
+export const runtime = "experimental-edge";
+
 export const getStaticPaths: GetStaticPaths = () => ({
   paths: [],
   fallback: "blocking",
@@ -13,11 +15,11 @@ interface TheoremProps {
   theorem: ChangelogItemData;
 }
 
-export const getStaticProps: GetStaticProps<TheoremProps> = (context) => {
+export const getStaticProps: GetStaticProps<TheoremProps> = async (context) => {
   if (!context.params?.name || Array.isArray(context.params.name)) {
     return { notFound: true };
   }
-  const theorem = getTheorem("v3", context.params.name);
+  const theorem = await getItemEdge("v3", "theorem", context.params.name);
   if (!theorem) return { notFound: true };
   return { props: { theorem } };
 };

website/pages/v4/changelog/[page].tsx

@@ -11,10 +11,13 @@ import summarizeHeadline from "../../../util/summarizeHeadline";
 
 const PER_PAGE = 50;
 
-export const getStaticPaths: GetStaticPaths = () => ({
-  paths: [],
-  fallback: "blocking",
-});
+export const getStaticPaths: GetStaticPaths = () => {
+  const commitPages = getCommitPages("v4");
+  return {
+    paths: commitPages.map((_, i) => ({ params: { page: String(i + 1) } })),
+    fallback: false,
+  };
+};
 
 interface CommitSummary {
   headline: string;

website/pages/v4/commit/[sha].tsx

@@ -3,10 +3,12 @@ import { GetStaticPaths, GetStaticProps, NextPage } from "next";
 import Link from "next/link";
 import Layout from "../../../components/Layout";
 import MathlibGithubMarkdown from "../../../components/MathlibGithubMarkdown";
-import { getCommit } from "../../../data/database";
+import { getCommitEdge } from "../../../data/edgeDatabase";
 import { ChangeType, CommitData, DiffData } from "../../../data/types";
 import formatTimestamp from "../../../util/formatTimestamp";
 
+export const runtime = "experimental-edge";
+
 export const getStaticPaths: GetStaticPaths = () => ({
   paths: [],
   fallback: "blocking",
@@ -16,11 +18,11 @@ interface CommitProps {
   commit: CommitData;
 }
 
-export const getStaticProps: GetStaticProps<CommitProps> = (context) => {
+export const getStaticProps: GetStaticProps<CommitProps> = async (context) => {
   if (!context.params?.sha || Array.isArray(context.params.sha)) {
     return { notFound: true };
   }
-  const commit = getCommit("v4", context.params.sha);
+  const commit = await getCommitEdge("v4", context.params.sha);
   if (!commit) return { notFound: true };
   return { props: { commit } };
 };

website/pages/v4/def/[name].tsx

@@ -1,9 +1,11 @@
 import { GetStaticPaths, GetStaticProps, NextPage } from "next";
 import { ItemChangeHistory } from "../../../components/ItemChangeHistory";
 import Layout from "../../../components/Layout";
-import { getDef } from "../../../data/database";
+import { getItemEdge } from "../../../data/edgeDatabase";
 import { ChangelogItemData } from "../../../data/extractDataFromChangelog";
 
+export const runtime = "experimental-edge";
+
 export const getStaticPaths: GetStaticPaths = () => ({
   paths: [],
   fallback: "blocking",
@@ -13,11 +15,11 @@ interface DefProps {
   def: ChangelogItemData;
 }
 
-export const getStaticProps: GetStaticProps<DefProps> = (context) => {
+export const getStaticProps: GetStaticProps<DefProps> = async (context) => {
   if (!context.params?.name || Array.isArray(context.params.name)) {
     return { notFound: true };
   }
-  const def = getDef("v4", context.params.name);
+  const def = await getItemEdge("v4", "def", context.params.name);
   if (!def) return { notFound: true };
   return { props: { def } };
 };

website/pages/v4/inductive/[name].tsx

@@ -1,9 +1,11 @@
 import { GetStaticPaths, GetStaticProps, NextPage } from "next";
 import { ItemChangeHistory } from "../../../components/ItemChangeHistory";
 import Layout from "../../../components/Layout";
-import { getInductive } from "../../../data/database";
+import { getItemEdge } from "../../../data/edgeDatabase";
 import { ChangelogItemData } from "../../../data/extractDataFromChangelog";
 
+export const runtime = "experimental-edge";
+
 export const getStaticPaths: GetStaticPaths = () => ({
   paths: [],
   fallback: "blocking",
@@ -13,11 +15,11 @@ interface InductiveProps {
   inductive: ChangelogItemData;
 }
 
-export const getStaticProps: GetStaticProps<InductiveProps> = (context) => {
+export const getStaticProps: GetStaticProps<InductiveProps> = async (context) => {
   if (!context.params?.name || Array.isArray(context.params.name)) {
     return { notFound: true };
   }
-  const inductive = getInductive("v4", context.params.name);
+  const inductive = await getItemEdge("v4", "inductive", context.params.name);
   if (!inductive) return { notFound: true };
   return { props: { inductive } };
 };