From e0ff5bf9105e494e4ff480ab790c9a08370368fd Mon Sep 17 00:00:00 2001
From: Michael Zhang <mail@mzhang.io>
Date: Thu, 27 Jun 2024 00:43:35 -0500
Subject: [PATCH] agda

---
 .../posts/2024-06-26-agda-rendering.lagda.md  | 72 +++++++++++++++++--
 1 file changed, 65 insertions(+), 7 deletions(-)

diff --git a/src/content/posts/2024-06-26-agda-rendering.lagda.md b/src/content/posts/2024-06-26-agda-rendering.lagda.md
index 82d0563..61f9e6d 100644
--- a/src/content/posts/2024-06-26-agda-rendering.lagda.md
+++ b/src/content/posts/2024-06-26-agda-rendering.lagda.md
@@ -1,22 +1,18 @@
 ---
-title: "Agda rendering in my blog!"
+title: "Agda syntax highlighting in my blog!"
 slug: 2024-06-26-agda-rendering
 date: 2024-06-27T04:25:15.332Z
 tags: ["meta", "agda"]
-draft: true
 ---
 
-I finally spent some time today getting Agda syntax highlighting working on my blog.
+I finally spent some time today getting full Agda syntax highlighting working on my blog.
 This took me around 3-4 hours of debugging but I'm very happy with how it turned out.
 
 First off, a demonstration. Here's the code for function application over a path:
 
 ```
 open import Agda.Primitive
-
-infix 4 _≡_
-data _≡_ {l} {A : Set l} : (a b : A) → Set l where
-  instance refl : {x : A} → x ≡ x
+open import Prelude
 
 ap : {l1 l2 : Level} {A : Set l1} {B : Set l2} {x y : A}
   → (f : A → B)
@@ -24,3 +20,65 @@ ap : {l1 l2 : Level} {A : Set l1} {B : Set l2} {x y : A}
   → f x ≡ f y
 ap {l1} {l2} {A} {B} {x} {y} f refl = refl
 ```
+
+While editing this in my editor, I can issue the "Agda: Load" command to have Agda type-check it.
+I can also work with typed holes interactively.
+
+The crux of the effort boiled down to two things:
+
+1. Writing the markdown processor
+2. Building the Docker image
+
+## Markdown processor
+
+The markdown processor is a [single file of JavaScript][plugin] that runs during my builds.
+It's a [remark] plugin, so you can plug it wherever else you want, as long as it uses remark.
+
+[plugin]: https://git.mzhang.io/michael/blog/src/commit/2b4ca03563286d21d0ba4004ac36e2e2e7a259ed/plugin/remark-agda.ts
+[remark]: https://github.com/remarkjs/remark
+
+I basically just run `agda` using the HTML backend options according to [the documentation here][1].
+Using the code method, I can have it leave the rest of the markdown file intact and only replace the agda code blocks with HTML.
+It'll also spit out a CSS file used to highlight.
+
+[1]: https://agda.readthedocs.io/en/v2.6.4.3-r1/tools/generating-html.html
+
+One bit of complication here is that the generated file stripped off the front matter I needed to continue rendering this page with Astro.
+There's a bit of code in that plugin file where I just order all of the agda blocks from the generated file and paste them back into the original.
+Probably not the best way but it works.
+
+The other bit of complication here is that the generated files need to go back into the public directory of my static site generator.
+In Agda, applying `--html-highlight=code` applies this to _all_ files, including the dependency files (such as `Agda.Primitive.html`).
+So I wrote a bit of glue code to have it also include the CSS file again.
+
+Overall, not too complicated.
+
+## Docker image
+
+Okay, while writing this article I found [sourcedennis/agda-mini][2], but when I first started, I was having trouble finding a slim Agda distribution that was well maintained.
+I looked into writing an Agda Dockerfile, but I also didn't want to maintain that either.
+
+[2]: https://github.com/sourcedennis/docker-agda-mini
+
+My approach was to use Nix to build the layered Docker image.
+My derivation file lives [here][3].
+Originally, I was considering using the version of Agda packaged in Nixpkgs.
+Unfortunately, because of the GHC backend that Agda has, the Nixpkgs closure for Agda is approximately 3GB.
+I didn't want a huge container image for my blog builder.
+
+[3]: https://git.mzhang.io/michael/blog/src/commit/2b4ca03563286d21d0ba4004ac36e2e2e7a259ed/nix/docker-builder.nix
+
+Instead, I use the Agda source directly, which is also packaged as a Nix package.
+After this it's just the matter of including the rest of the party, which [pkgs.dockerTools][4] helped a lot with.
+
+[4]: https://ryantm.github.io/nixpkgs/builders/images/dockertools/
+
+---
+
+That's it! Now my blog builds fully automatically in CI, with Agda syntax highlighting.
+If you want to go back up to the top, click `ap` below :\)
+
+```
+_ : (n : ℕ) → suc n ≡ suc n
+_ = λ _ → ap suc refl
+```