From 0962df69ad92e9a715723147fe37ad4f120c7fb9 Mon Sep 17 00:00:00 2001
From: Danila Fedorin <danila.fedorin@gmail.com>
Date: Fri, 24 May 2024 20:33:34 +0000
Subject: [PATCH] Factor out building Agda HTML from building the blog

This saves a lot of time since typechecking Agda is slow.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
---
 build/builder.sh | 20 +++++++-------------
 flake.lock       |  8 ++++----
 lib.nix          | 36 +++++++++++++++++++++++++++++++-----
 3 files changed, 42 insertions(+), 22 deletions(-)

diff --git a/build/builder.sh b/build/builder.sh
index befd8df..bf0a1ea 100644
--- a/build/builder.sh
+++ b/build/builder.sh
@@ -6,12 +6,12 @@ export RUBYOPT="-KU -E utf-8:utf-8"
 # Copy files to a mutable directory.
 cp -r $src/* .
 # We'll generate some static files so make static writable
-mkdir -p static && chmod -R u+w static
+# We also store the code HTML files alongside Agda code, so make 'code' writable too
+mkdir -p static && chmod -R u+w static code
 
 # We host some static files (KaTeX CSS in production) on
 # static.danilafe.com. However, we can just bundle them here instead!
-# Also, since we're generating and adding a resume further down, add it to
-# the configuration here as well.
+# Configure Hugo to do so by writing the expected final paths to config-urls.toml
 echo '[params]' >> config-urls.toml
 echo 'katexCssUrl = "/katex/katex.min.css"' >> config-urls.toml
 echo 'normalizeCssUrl = "/normalize/normalize.css"' >> config-urls.toml
@@ -20,22 +20,16 @@ echo 'bergamotJsUrl = "/bergamot/bergamot.js"' >> config-urls.toml
 echo 'katexJsUrl = "/katex/katex.min.js"' >> config-urls.toml
 echo 'resumeStaticFile = "/Resume-Danila-Fedorin.pdf"' >> config-urls.toml
 
-cp -r $webFiles/* static/
-
 # Build site with Hugo
 hugo $hugoFlags --config=config.toml,config-urls.toml
 
-# Run Agda to generate HTML files for all Agda projects
-# Agda will write interface files, so make .code/ writable
-chmod -R u+w code
-agdaCommand="agda -l standard-library -i . "
-ruby ./build-agda-html.rb "$agdaCommand"
-
-# Create generated files
+# Create/copy generated files
 # Can't do submodules because nix flake inputs get their .git deleted
 mkdir -p static/graph && ruby ./analyze.rb > static/graph/graph.gen.js # Graph files
 stork build --input public/index.toml --output static/index.st # Search index
 cp $resume/Resume-Danila-Fedorin.pdf static/Resume-Danila-Fedorin.pdf
+cp -r $webFiles/* static/
+cp -r $agdaHtml/* code/
 
 # Static folder changed, re-run Hugo
 hugo $hugoFlags --config=config.toml,config-urls.toml
@@ -44,7 +38,7 @@ hugo $hugoFlags --config=config.toml,config-urls.toml
 mkdir $out
 cp -r public/$publicPath/* $out/
 
-# Render math in HTML and XML files.
+# Do post-processing of HTML files: render math and link up Agda code
 htmlfiles=$(find $out/ -regex "$out/.*\.html")
 echo $htmlfiles | xargs ${gems}/bin/bundle exec ${ruby}/bin/ruby ./convert.rb --katex-js-file static/katex/katex.min.js
 echo $htmlfiles | xargs ${gems}/bin/bundle exec ${ruby}/bin/ruby ./agda.rb
diff --git a/flake.lock b/flake.lock
index 5ddb9a7..029c46a 100644
--- a/flake.lock
+++ b/flake.lock
@@ -23,11 +23,11 @@
     "blog-source": {
       "flake": false,
       "locked": {
-        "lastModified": 1716524089,
-        "narHash": "sha256-bqYW4a8Cn3AbbxLGDSUs+qOVMTXQ0gFrT7mPDThh2+I=",
+        "lastModified": 1716582093,
+        "narHash": "sha256-2CWN9UaMJo+Dii/yLx+BQHtjVPlvQPCwBdKbY3enyNE=",
         "ref": "refs/heads/master",
-        "rev": "06ee998d5411cbc4b1b1188711ba582e5fcc6c33",
-        "revCount": 778,
+        "rev": "60ba43378a7cdfd30b8abb8ef77db74e8c319a22",
+        "revCount": 781,
         "submodules": true,
         "type": "git",
         "url": "https://dev.danilafe.com/Web-Projects/blog-static.git"
diff --git a/lib.nix b/lib.nix
index b2d88d0..3a91d94 100644
--- a/lib.nix
+++ b/lib.nix
@@ -5,18 +5,42 @@ with lib;
 
 let
   protocol = ssl: if ssl then "https://" else "http://";
-  gems = bundlerEnv {
+  gems = settings: bundlerEnv {
     inherit ruby;
 
     name = "blog-static-flake";
-    gemfile = "${blog-source}/Gemfile";
-    lockfile = "${blog-source}/Gemfile.lock";
+    gemfile = "${settings.src}/Gemfile";
+    lockfile = "${settings.src}/Gemfile.lock";
     gemset = ./gemset.nix;
   };
 
+  # --- Building Agda HTML ---
+  agdaEnv = agda.withPackages [ agdaPackages.standard-library ];
+  agdaHtml = settings:
+    let
+      # Create content-addresed versions of the scripts in the Nix store to
+      # avoid throwing off memoization for unrelated changes.
+      agdaBuildScript = builtins.toFile "build-agda-html.rb" (builtins.readFile "${settings.src}/build-agda-html.rb");
+      submoduleDataFile = builtins.toFile "submodules.json" (builtins.readFile "${settings.src}/data/submodules.json");
+      codeRoot = pkgs.lib.cleanSource "${settings.src}/code";
+      agdaCommand = pkgs.lib.escapeShellArg "agda -l standard-library -i . ";
+    in
+      stdenv.mkDerivation {
+        name = "blog-static-agda-html";
+        version = settings.src.rev or "dirty";
+        buildInputs = [ ruby agdaEnv ];
+        builder = builtins.toFile "builder.sh" "
+        source $stdenv/setup
+        mkdir -p code $out
+        cp -r ${codeRoot}/* code/
+        chmod -R u+w code
+        ruby ${agdaBuildScript} --data-file=${submoduleDataFile} --target-dir=$out ${agdaCommand}
+        ";
+      };
+
   website = settings: stdenv.mkDerivation {
     inherit (settings) src ssl host;
-    inherit resume gems ruby;
+    inherit resume ruby;
     name = "blog-static";
     version = settings.src.rev or "dirty";
     publicPath = settings.path;
@@ -26,8 +50,10 @@ let
     );
     builder = ./build/builder.sh;
     webFiles = web-files;
+    gems = gems settings;
+    agdaHtml = agdaHtml settings;
     buildInputs = [
-      hugo ruby stork (agda.withPackages [ agdaPackages.standard-library ])
+      hugo ruby stork agdaEnv
     ];
   };
 in