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

@@ -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