render primitives

.gitignore

@@ -28,3 +28,5 @@ _build
 
 /result
 .pnpm-store
+
+/public/generated

astro.config.ts

@@ -15,34 +15,42 @@ import rehypeSlug from "rehype-slug";
 import markdoc from "@astrojs/markdoc";
 import remarkAgda from "./plugin/remark-agda";
 
+const outDir = "dist";
+const base = process.env.BASE ?? "/";
+const publicDir = "public";
+
 // https://astro.build/config
 export default defineConfig({
-	site: "https://mzhang.io",
+  site: "https://mzhang.io",
-	integrations: [mdx(), sitemap(), markdoc()],
+  integrations: [mdx(), sitemap(), markdoc()],
-	markdown: {
+
-		syntaxHighlight: "shiki",
+  outDir,
-		shikiConfig: {
+  base,
-			theme: "css-variables",
+  trailingSlash: "always",
-		},
+  publicDir,
-		remarkPlugins: [
+
-            remarkAgda,
+  markdown: {
-			remarkMath,
+    syntaxHighlight: "shiki",
-			remarkAdmonitions,
+    shikiConfig: { theme: "css-variables" },
-			remarkReadingTime,
+    remarkPlugins: [
-			remarkTypst,
+      () => remarkAgda({ outDir, base, publicDir }),
-			remarkEmoji,
+      remarkMath,
-			[
+      remarkAdmonitions,
-				remarkDescription,
+      remarkReadingTime,
-				{
+      remarkTypst,
-					name: "excerpt",
+      remarkEmoji,
-				},
+      [
-			],
+        remarkDescription,
-		],
+        {
-		rehypePlugins: [
+          name: "excerpt",
-			[rehypeKatex, {}],
+        },
-			rehypeAccessibleEmojis,
+      ],
-			rehypeSlug,
+    ],
-			[rehypeLinkHeadings, { behavior: "wrap" }],
+    rehypePlugins: [
-		],
+      [rehypeKatex, {}],
-	},
+      rehypeAccessibleEmojis,
+      rehypeSlug,
+      [rehypeLinkHeadings, { behavior: "wrap" }],
+    ],
+  },
 });

plugin/remark-agda.ts

@@ -1,16 +1,32 @@
-import type { RemarkPlugin } from "@astrojs/markdown-remark";
 import type { RootContent } from "hast";
 import { fromMarkdown } from "mdast-util-from-markdown";
 import { fromHtml } from "hast-util-from-html";
 import { toHtml } from "hast-util-to-html";
 
 import { spawnSync } from "node:child_process";
-import { mkdirSync, mkdtempSync, readFileSync } from "node:fs";
+import {
+  mkdirSync,
+  mkdtempSync,
+  readFileSync,
+  readdirSync,
+  copyFileSync,
+  writeFileSync,
+} from "node:fs";
 import { tmpdir } from "node:os";
 import { join, parse } from "node:path";
 import { visit } from "unist-util-visit";
+import type { RemarkPlugin } from "@astrojs/markdown-remark";
+
+interface Options {
+  base: string;
+  outDir: string;
+  publicDir: string;
+}
+
+const remarkAgda: RemarkPlugin = ({ base, publicDir }: Options) => {
+  const destDir = join(publicDir, "generated", "agda");
+  mkdirSync(destDir, { recursive: true });
 
-const remarkAgda: RemarkPlugin = () => {
   return (tree, { history }) => {
     const path: string = history[history.length - 1]!;
     if (!(path.endsWith(".lagda.md") || path.endsWith(".agda"))) return;
@@ -18,14 +34,14 @@ const remarkAgda: RemarkPlugin = () => {
     console.log("AGDA:processing path", path);
 
     const tempDir = mkdtempSync(join(tmpdir(), "agdaRender."));
-    const outDir = join(tempDir, "output");
+    const agdaOutDir = join(tempDir, "output");
-    mkdirSync(outDir, { recursive: true });
+    mkdirSync(agdaOutDir, { recursive: true });
 
     const childOutput = spawnSync(
       "agda",
       [
         "--html",
-        `--html-dir=${outDir}`,
+        `--html-dir=${agdaOutDir}`,
         "--highlight-occurrences",
         "--html-highlight=code",
         path,
@@ -34,17 +50,45 @@ const remarkAgda: RemarkPlugin = () => {
     );
 
     // TODO: Handle child output
-    console.error("--AGDA OUTPUT--")
+    console.error("--AGDA OUTPUT--");
     console.error(childOutput);
     console.error(childOutput.stdout?.toString());
     console.error(childOutput.stderr?.toString());
-    console.error("--AGDA OUTPUT--")
+    console.error("--AGDA OUTPUT--");
-    // if (childOutput.status !== 0)
+
-    //     throw new Error("Agda failed", childOutput.stderr)
+    const referencedFiles = new Set();
+    for (const file of readdirSync(agdaOutDir)) {
+      referencedFiles.add(file);
+
+      const fullPath = join(agdaOutDir, file);
+      const fullDestPath = join(destDir, file);
+
+      if (file.endsWith(".html")) {
+        const src = readFileSync(fullPath);
+        writeFileSync(
+          fullDestPath,
+          `
+          <!DOCTYPE html>
+          <html>
+          <head>
+          <link rel="stylesheet" href="${base}generated/agda/Agda.css" />
+          </head>
+          <body>
+          <pre class="Agda">
+          ${src}
+          </pre>
+          </body>
+          </html>
+        `,
+        );
+      } else {
+        copyFileSync(fullPath, fullDestPath);
+      }
+    }
 
     const filename = parse(path).base.replace(/\.lagda.md/, ".md");
     const htmlname = parse(path).base.replace(/\.lagda.md/, ".html");
-    const fullOutputPath = join(outDir, filename);
+    const fullOutputPath = join(agdaOutDir, filename);
 
     const doc = readFileSync(fullOutputPath);
 
@@ -60,8 +104,17 @@ const remarkAgda: RemarkPlugin = () => {
       visit(html, "element", (node) => {
         if (node.tagName !== "a") return;
 
-        if (node.properties.href && node.properties.href.includes(htmlname)) {
+        if (node.properties.href) {
-          node.properties.href = node.properties.href.replace(htmlname, "");
+          // Trim off end
+          const [href, hash, ...rest] = node.properties.href.split("#");
+          if (rest.length > 0) throw new Error("come look at this");
+
+          if (href === htmlname) node.properties.href = `#${hash}`;
+
+          if (referencedFiles.has(href)) {
+            node.properties.href = `${base}generated/agda/${href}${hash ? `#${hash}` : ""}`;
+            node.properties.target = "_blank";
+          }
         }
       });
 

src/content/posts/2024-06-26-agda-rendering.lagda.md

@@ -0,0 +1,26 @@
+---
+title: "Agda rendering 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.
+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
+
+ap : {l1 l2 : Level} {A : Set l1} {B : Set l2} {x y : A}
+  → (f : A → B)
+  → (p : x ≡ y)
+  → f x ≡ f y
+ap {l1} {l2} {A} {B} {x} {y} f refl = refl
+```