Convert to static export for free hosting

.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/out/
 
 # misc
 .vscode

.wrangler/cache/pages.json

@@ -0,0 +1,4 @@
+{
+  "account_id": "174ed3333f8cdd4b7e7896557584d89c",
+  "project_name": "mathlib-changelog"
+}

.wrangler/cache/wrangler-account.json

@@ -0,0 +1,6 @@
+{
+  "account": {
+    "id": "174ed3333f8cdd4b7e7896557584d89c",
+    "name": "Chanindav@gmail.com's Account"
+  }
+}

website/components/ClientCommitPage.tsx

@@ -0,0 +1,158 @@
+import { CodeIcon, MinusIcon, PlusIcon } from "@heroicons/react/solid";
+import Link from "next/link";
+import { FC } from "react";
+import { useQuery } from "react-query";
+import { fetchCommit } from "../data/clientDatabase";
+import { ChangeType, DiffData, LeanVersion } from "../data/types";
+import formatTimestamp from "../util/formatTimestamp";
+import Layout from "./Layout";
+import MathlibGithubMarkdown from "./MathlibGithubMarkdown";
+import Spinner from "./Spinner";
+
+interface Props {
+  version: LeanVersion;
+  sha: string;
+}
+
+const getLabel = (changeType: ChangeType) => {
+  if (changeType === "add") {
+    return (
+      <span className="text-sm text-green-400">
+        <PlusIcon className="w-4 h-4 inline" /> added
+      </span>
+    );
+  }
+  if (changeType === "del") {
+    return (
+      <span className="text-sm text-red-400">
+        <MinusIcon className="w-4 h-4 inline" /> deleted
+      </span>
+    );
+  }
+  return (
+    <span className="text-sm text-blue-400">
+      <CodeIcon className="w-4 h-4 inline" /> modified
+    </span>
+  );
+};
+
+const getFileChangeLabel = (diff: DiffData) => {
+  if (diff.oldPath && diff.newPath && diff.oldPath !== diff.newPath) {
+    return (
+      <span>
+        Renamed <span className="italic">{diff.oldPath}</span> to{" "}
+        <span className="italic">{diff.newPath}</span>
+      </span>
+    );
+  }
+  if (diff.oldPath && diff.newPath) {
+    return (
+      <span>
+        Modified <span className="italic">{diff.oldPath}</span>
+      </span>
+    );
+  }
+  if (diff.oldPath && !diff.newPath) {
+    return (
+      <span>
+        Deleted <span className="italic">{diff.oldPath}</span>
+      </span>
+    );
+  }
+  if (!diff.oldPath && diff.newPath) {
+    return (
+      <span>
+        Created <span className="italic">{diff.newPath}</span>
+      </span>
+    );
+  }
+};
+
+const repoName = (version: LeanVersion) =>
+  version === "v3" ? "mathlib" : "mathlib4";
+
+const ClientCommitPage: FC<Props> = ({ version, sha }) => {
+  const { data: commit, isLoading } = useQuery(
+    ["commit", version, sha],
+    () => fetchCommit(version, sha),
+    { staleTime: Infinity }
+  );
+
+  if (isLoading) {
+    return (
+      <Layout version={version}>
+        <div className="flex justify-center py-12">
+          <Spinner size={10} />
+        </div>
+      </Layout>
+    );
+  }
+
+  if (!commit) {
+    return (
+      <Layout version={version}>
+        <h1 className="text-xl">Commit not found</h1>
+        <p className="text-gray-500 mt-2">
+          No commit found with SHA {sha}.
+        </p>
+      </Layout>
+    );
+  }
+
+  return (
+    <Layout version={version}>
+      <h1 className="text-xl">
+        <span className="text-gray-400">Commit</span>{" "}
+        {formatTimestamp(commit.timestamp)}{" "}
+        <span className="text-gray-400">{commit.sha}</span>
+      </h1>
+      <a
+        href={`https://github.com/leanprover-community/${repoName(version)}/commit/${commit.sha}`}
+        className="text-blue-600 text-xs"
+      >
+        View on Github →
+      </a>
+
+      <div>
+        <MathlibGithubMarkdown contents={commit.message} version={version} />
+      </div>
+      <h4 className="mt-4 mb-2 font-bold text-sm">Estimated changes</h4>
+      <div>
+        {commit.changes.map((diff, i) => (
+          <div className="my-1" key={i}>
+            <div>
+              <a
+                className="text-gray-800 hover:underline"
+                href={`https://github.com/leanprover-community/${repoName(version)}/commit/${commit.sha}#diff-${diff.pathSha}`}
+              >
+                {getFileChangeLabel(diff)}
+              </a>
+            </div>
+            <div className="pl-2 text-sm">
+              {diff.changes.map(
+                ([changeType, itemType, itemName, namespace], j) => {
+                  const fullName = [...namespace, itemName].join(".");
+                  return (
+                    <div key={j}>
+                      <span className="inline-block min-w-[100px] text-right">
+                        {getLabel(changeType)}
+                      </span>{" "}
+                      <span className="font-semibold">{itemType}</span>{" "}
+                      <Link
+                        href={`/${version}/${itemType}/${encodeURIComponent(fullName)}`}
+                      >
+                        {fullName}
+                      </Link>
+                    </div>
+                  );
+                }
+              )}
+            </div>
+          </div>
+        ))}
+      </div>
+    </Layout>
+  );
+};
+
+export default ClientCommitPage;

website/components/ClientItemPage.tsx

@@ -0,0 +1,66 @@
+import { FC } from "react";
+import { useQuery } from "react-query";
+import { fetchItem } from "../data/clientDatabase";
+import { ItemType, LeanVersion } from "../data/types";
+import { ItemChangeHistory } from "./ItemChangeHistory";
+import Layout from "./Layout";
+import Spinner from "./Spinner";
+
+interface Props {
+  version: LeanVersion;
+  itemType: ItemType;
+  name: string;
+}
+
+const typeLabel: Record<ItemType, string> = {
+  theorem: "Theorem",
+  def: "Def",
+  structure: "Structure",
+  inductive: "Inductive",
+};
+
+const ClientItemPage: FC<Props> = ({ version, itemType, name }) => {
+  const { data: item, isLoading } = useQuery(
+    ["item", version, itemType, name],
+    () => fetchItem(version, itemType, name),
+    { staleTime: Infinity }
+  );
+
+  if (isLoading) {
+    return (
+      <Layout version={version}>
+        <div className="flex justify-center py-12">
+          <Spinner size={10} />
+        </div>
+      </Layout>
+    );
+  }
+
+  if (!item) {
+    return (
+      <Layout version={version}>
+        <h1 className="text-xl">
+          <span className="text-gray-400">{typeLabel[itemType]}</span> not found
+        </h1>
+        <p className="text-gray-500 mt-2">
+          No {itemType} found with name {name}.
+        </p>
+      </Layout>
+    );
+  }
+
+  return (
+    <Layout version={version}>
+      <h1 className="text-xl">
+        <span className="text-gray-400">{typeLabel[itemType]}</span>{" "}
+        {item.name}
+      </h1>
+      <h4 className="text-sm mt-4">Modification history</h4>
+      <div>
+        <ItemChangeHistory item={item} version={version} />
+      </div>
+    </Layout>
+  );
+};
+
+export default ClientItemPage;

website/data/clientDatabase.ts

@@ -0,0 +1,61 @@
+import { ChangelogItemData } from "./extractDataFromChangelog";
+import { CommitData, ItemType, LeanVersion } from "./types";
+
+async function sha256Prefix(input: string): Promise<string> {
+  const encoder = new TextEncoder();
+  const data = encoder.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);
+}
+
+const chunkCache: Record<string, unknown> = {};
+
+async function fetchChunk<T>(url: string): Promise<T> {
+  if (chunkCache[url]) return chunkCache[url] as T;
+  const res = await fetch(url);
+  if (!res.ok) throw new Error(`Failed to fetch ${url}: ${res.status}`);
+  const data = await res.json();
+  chunkCache[url] = data;
+  return data as T;
+}
+
+export async function fetchCommit(
+  version: LeanVersion,
+  sha: string
+): Promise<CommitData | null> {
+  const prefix = sha.slice(0, 2).toLowerCase();
+  const url = `/data/${version}/commits/${prefix}.json`;
+  try {
+    const bucket = await fetchChunk<Record<string, CommitData>>(url);
+    // Try full SHA match first, then 8-char prefix match
+    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 fetchItem(
+  version: LeanVersion,
+  itemType: ItemType,
+  name: string
+): Promise<ChangelogItemData | null> {
+  const prefix = await sha256Prefix(name);
+  const url = `/data/${version}/items/${prefix}.json`;
+  try {
+    const bucket = await fetchChunk<Record<string, ChangelogItemData>>(url);
+    const item = bucket[name];
+    if (!item || item.type !== itemType) return null;
+    return item;
+  } catch {
+    return null;
+  }
+}

website/next.config.js

@@ -1,50 +1,10 @@
 /** @type {import('next').NextConfig} */
 const nextConfig = {
+  output: "export",
   reactStrictMode: true,
   swcMinify: true,
-  async redirects() {
-    return [
-      {
-        source: "/",
-        destination: "/v4",
-        permanent: false,
-      },
-      {
-        source: "/changelog",
-        destination: "/v4/changelog/1",
-        permanent: false,
-      },
-      {
-        source: "/commit/:sha",
-        destination: "/v3/commit/:sha",
-        permanent: false,
-      },
-      {
-        source: "/def/:name",
-        destination: "/v3/def/:name",
-        permanent: false,
-      },
-      {
-        source: "/inductive/:name",
-        destination: "/v3/inductive/:name",
-        permanent: false,
-      },
-      {
-        source: "/structure/:name",
-        destination: "/v3/structure/:name",
-        permanent: false,
-      },
-      {
-        source: "/theorem/:name",
-        destination: "/v3/theorem/:name",
-        permanent: false,
-      },
-      {
-        source: "/changelog/:page",
-        destination: "/v3/changelog/:page",
-        permanent: false,
-      },
-    ];
+  images: {
+    unoptimized: true,
   },
 };
 

website/package.json

@@ -4,11 +4,12 @@
   "private": true,
   "scripts": {
     "dev": "next dev",
+    "prebuild": "ts-node scripts/buildStaticData.ts && ts-node scripts/buildSearchItems.ts",
     "build": "next build",
-    "postbuild": "yarn build:search && yarn build:sitemap",
+    "postbuild": "next-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"
   },

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;