From 71af8db54b6b246077940d76a6f7c7423cebd6fc Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Thu, 21 Jul 2022 21:05:19 +0200
Subject: [PATCH] feat: Declaration data into separate directory

---
 DocGen4/Output.lean        | 11 +++++++----
 static/declaration-data.js |  4 ++--
 2 files changed, 9 insertions(+), 6 deletions(-)

diff --git a/DocGen4/Output.lean b/DocGen4/Output.lean
index c690c04..0776f61 100644
--- a/DocGen4/Output.lean
+++ b/DocGen4/Output.lean
@@ -21,14 +21,16 @@ open Lean IO System Output Process Std
 
 def basePath := FilePath.mk "." / "build" / "doc"
 def srcBasePath := basePath / "src"
+def declarationsBasePath := basePath / "declarations"
 
 def htmlOutputSetup (config : SiteBaseContext) : IO Unit := do
   let findBasePath := basePath / "find"
 
   -- Base structure
   FS.createDirAll basePath
-  FS.createDirAll (basePath / "find")
+  FS.createDirAll findBasePath
   FS.createDirAll srcBasePath
+  FS.createDirAll declarationsBasePath
 
   -- All the doc-gen static stuff
   let indexHtml := ReaderT.run index config |>.toString
@@ -86,6 +88,7 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (
   }
 
   FS.createDirAll basePath
+  FS.createDirAll declarationsBasePath
 
   -- Rendering the entire lean compiler takes time....
   --let sourceSearchPath := ((←Lean.findSysroot) / "src" / "lean") :: ws.root.srcDir :: ws.leanSrcPath
@@ -99,7 +102,7 @@ def htmlOutputResults (baseConfig : SiteBaseContext) (result : AnalyzerResult) (
     declMap := declMap.insert topLevelMod (currentModDecls ++ jsonDecls)
 
   for (topLevelMod, decls) in declMap.toList do
-    FS.writeFile (basePath / s!"declaration-data-{topLevelMod}.bmp") (Json.arr decls).compress
+    FS.writeFile (declarationsBasePath / s!"declaration-data-{topLevelMod}.bmp") (Json.arr decls).compress
 
   for (modName, module) in result.moduleInfo.toArray do
     let fileDir := moduleNameToDirectory basePath modName
@@ -133,13 +136,13 @@ def htmlOutputFinalize (baseConfig : SiteBaseContext) : IO Unit := do
   htmlOutputSetup baseConfig
 
   let mut topLevelModules := #[]
-  for entry in ←System.FilePath.readDir basePath do
+  for entry in ←System.FilePath.readDir declarationsBasePath do
     if entry.fileName.startsWith "declaration-data-" && entry.fileName.endsWith ".bmp" then
       let module := entry.fileName.drop "declaration-data-".length |>.dropRight ".bmp".length
       topLevelModules := topLevelModules.push (Json.str module)
 
   -- The root JSON for find
-  FS.writeFile (basePath / "declaration-data.bmp") (Json.arr topLevelModules).compress
+  FS.writeFile (declarationsBasePath / "declaration-data.bmp") (Json.arr topLevelModules).compress
 
 /--
 The main entrypoint for outputting the documentation HTML based on an
diff --git a/static/declaration-data.js b/static/declaration-data.js
index 0c284dc..6a74bee 100644
--- a/static/declaration-data.js
+++ b/static/declaration-data.js
@@ -10,7 +10,7 @@ const CACHE_DB_KEY = "DECLARATIONS_KEY";
 
 async function fetchModuleData(module) {
   const moduleDataUrl = new URL(
-    `${SITE_ROOT}declaration-data-${module}.bmp`,
+    `${SITE_ROOT}/declarations/declaration-data-${module}.bmp`,
     window.location
   );
   const moduleData = await fetch(moduleDataUrl);
@@ -53,7 +53,7 @@ export class DeclarationDataCenter {
   static async init() {
     if (!DeclarationDataCenter.singleton) {
       const dataListUrl = new URL(
-        `${SITE_ROOT}declaration-data.bmp`,
+        `${SITE_ROOT}/declarations/declaration-data.bmp`,
         window.location
       );