Phase 2 of the durable fix for #20984 (architect proposal: #20984 (comment)). Blocked by phase 1 (#20992) — do not start until phase 1 has landed and proven out the static-data + fetch pattern.
Goal
Collapse the remaining ~7300 data modules (2435 index.ts shims + 2435 meta.json + 2435 annotations.json) to a few hundred app modules by moving JSON to public/ and deleting the import.meta.glob machinery. Returns the build toward its ~35s baseline and makes it O(1) in gallery size.
Implementation (per architect proposal §1–3)
- Emit step: copy each proof's
meta.json + annotations.json → public/data/proofs/<slug>/ (alongside source.lean from phase 1). Compute sha8 hashes.
- Hashed manifest: emit
src/data/proofs/data-manifest.json = { slug: { meta: <sha8>, ann: <sha8>, src: <sha8> } }. This is the ONLY per-proof data still imported into the graph (one small module). Bundled with content hashing, so any proof change busts the importing chunk.
- Rewrite
getProofAsync to fetch meta.json/annotations.json/source.lean by slug with ?v=<sha8> query params from the manifest (see proposal loader sketch). Keep the public signature.
- Delete the ~2435 per-proof
src/data/proofs/<slug>/index.ts shims and the import.meta.glob('./**/index.ts') + proofModules map. Also delete dead code getProof/getAllProofs (0 external consumers per architect grep).
listings.json stays an in-graph static import (1.8MB, single module, needed eagerly by HomePage/ErdosPage/ProfileModal — not part of the O(N) blowup).
Acceptance
Follow-up
Phase 3 (#FOLLOWUP): apply the identical pattern to src/data/research/index.ts (1982 research problems, import('./problems/${slug}.json') — same disease).
Phase 2 of the durable fix for #20984 (architect proposal: #20984 (comment)). Blocked by phase 1 (#20992) — do not start until phase 1 has landed and proven out the static-data + fetch pattern.
Goal
Collapse the remaining ~7300 data modules (2435
index.tsshims + 2435meta.json+ 2435annotations.json) to a few hundred app modules by moving JSON topublic/and deleting theimport.meta.globmachinery. Returns the build toward its ~35s baseline and makes it O(1) in gallery size.Implementation (per architect proposal §1–3)
meta.json+annotations.json→public/data/proofs/<slug>/(alongsidesource.leanfrom phase 1). Compute sha8 hashes.src/data/proofs/data-manifest.json={ slug: { meta: <sha8>, ann: <sha8>, src: <sha8> } }. This is the ONLY per-proof data still imported into the graph (one small module). Bundled with content hashing, so any proof change busts the importing chunk.getProofAsyncto fetchmeta.json/annotations.json/source.leanby slug with?v=<sha8>query params from the manifest (see proposal loader sketch). Keep the public signature.src/data/proofs/<slug>/index.tsshims and theimport.meta.glob('./**/index.ts')+proofModulesmap. Also delete dead codegetProof/getAllProofs(0 external consumers per architect grep).listings.jsonstays an in-graph static import (1.8MB, single module, needed eagerly by HomePage/ErdosPage/ProfileModal — not part of the O(N) blowup).Acceptance
pnpm buildvite buildstage back near ~35s baseline; report wall-clock.--debugconfirms).?v=and the manifest chunk hash.getProof/getAllProofs/proofModulesremoved; no remainingimport.meta.globfor proofs.Follow-up
Phase 3 (#FOLLOWUP): apply the identical pattern to
src/data/research/index.ts(1982 research problems,import('./problems/${slug}.json')— same disease).