agda building!

.gitignore

@@ -24,3 +24,6 @@ PragmataPro-Mono-Liga-Regular-Nerd-Font-Complete.woff2
 *.agdai
 _build
 .direnv
+
+
+/result

.woodpecker.yml

@@ -1,26 +1,18 @@
 steps:
   build:
-    image: node:20
+    image: git.mzhang.io/michael/blog-docker-builder:ksi5l9c786i4x6sq2crsjqlmcfidvvza
+    environment:
+      - ASTRO_TELEMETRY_DISABLED=1
     commands:
-      - npm install -g pnpm
+      - mkdir /tmp
-      #   - cd /tmp
+      - bun install --frozen-lockfile
-      #   - rm -rf astro
+      - bun run build
-      #   - git clone https://git.mzhang.io/michael/astro --depth 1
-      #   - cd astro
-      #   - pnpm install
-      #   - pnpm run build
-      #   - cd /woodpecker/src/git.mzhang.io/michael/blog
-      - pnpm install
-      #   - pnpm link /tmp/astro/packages/astro
-      #   - pnpm link /tmp/astro/packages/markdown/remark
-      - pnpm run build
     when:
       - event: push
 
   deploy:
-    image: alpine
+    image: git.mzhang.io/michael/blog-docker-builder:ksi5l9c786i4x6sq2crsjqlmcfidvvza
     commands:
-      - apk add rsync openssh
       - echo "$${SSH_SECRET_KEY}" > SSH_SECRET_KEY
       - chmod 600 SSH_SECRET_KEY
       - mkdir -p ~/.ssh

astro.config.ts

@@ -14,6 +14,7 @@ import rehypeLinkHeadings from "@justfork/rehype-autolink-headings";
 import rehypeSlug from "rehype-slug";
 
 import markdoc from "@astrojs/markdoc";
+import remarkAgda from "./plugin/remark-agda";
 
 // https://astro.build/config
 export default defineConfig({
@@ -25,6 +26,7 @@ export default defineConfig({
 			theme: "css-variables",
 		},
 		remarkPlugins: [
+            remarkAgda,
 			remarkMath,
 			remarkAdmonitions,
 			remarkReadingTime,

blog.agda-lib

@@ -1,2 +1,2 @@
 include: src/content/posts src
-depend: standard-library
+depend: standard-library cubical

flake.nix

@@ -4,16 +4,22 @@
     let
       pkgs = import nixpkgs { inherit system; };
       agda-pkg = agda.packages.x86_64-linux.default;
-      flakePkgs = {
+      flakePkgs = rec {
-        agda = agda-pkg;
+        agda-bin = pkgs.callPackage ./nix/agda-bin.nix { inherit agda-pkg; };
-        agda-bin = pkgs.callPackage ./nix/agda-bin.nix { agda = agda-pkg; };
+        docker-builder = pkgs.callPackage ./nix/docker-builder.nix { inherit agda-bin; };
-        docker-builder = pkgs.callPackage ./nix/docker-builder.nix { };
       };
     in
     {
       packages = flake-utils.lib.flattenTree flakePkgs;
       devShell = pkgs.mkShell {
-        packages = with pkgs; [ nixfmt-rfc-style ];
+        packages = with pkgs; [
+          bun
+          woodpecker-cli
+          nixfmt-rfc-style
+          dive
+          nix-tree
+          vips
+        ];
       };
     });
 }

nix/agda-bin.nix

@@ -1,6 +1,23 @@
-{ agda, runCommand }:
+{ agda-pkg, runCommand, writeShellScriptBin, writeTextFile, agdaPackages }:
 
-runCommand "agda-bin" { }
+let
-  ''
+  libraryFile =
-    cp ${agda}/bin/agda $out
+    with agdaPackages;
+    writeTextFile {
+      name = "agda-libraries";
+      text = ''
+        ${agdaPackages.cubical}/cubical.agda-lib
+        ${agdaPackages.standard-library}/standard-library.agda-lib
+      '';
+    };
+
+  # Add an extra layer of indirection here to prevent all of GHC from being pulled in
+  wtf = runCommand "agda-bin" { } ''
+    cp ${agda-pkg}/bin/agda $out
+  '';
+in
+
+writeShellScriptBin "agda" ''
+  set -euo pipefail
+  exec ${wtf} --library-file=${libraryFile} $@
 ''

nix/agda.nix

@@ -1,6 +0,0 @@
-{ haskellPackages }:
-
-haskellPackages.developPackage {
-  name = "agda";
-  version = "2.6.4.3";
-}

nix/docker-builder.nix

@@ -1,3 +1,35 @@
-{ dockerTools }:
+{ dockerTools
+, buildEnv
+, agda-bin
+, corepack
+, rsync
+, openssh
+, bash
+, coreutils
+, bun
+, nodejs_20
+}:
+
+dockerTools.buildLayeredImage {
+  name = "blog-docker-builder";
+
+  contents = with dockerTools; [
+    agda-bin
+    corepack
+    rsync
+    openssh
+    bash
+    coreutils
+    bun
+    nodejs_20
+    usrBinEnv
+    caCertificates
+  ];
+}
+
+#   copyToRoot = with dockerTools; buildEnv {
+#     name = "blog-docker-builder-image-root";
+#     paths = [
+#     ];
+#   };
 
-dockerTools.buildImage { }

package.json

@@ -47,7 +47,6 @@
     "prettier-plugin-astro": "^0.12.0",
     "rehype-slug": "^6.0.0",
     "sass": "^1.66.1",
-    "sharp": "^0.32.6",
     "shiki": "^0.14.5",
     "unified": "^11.0.2",
     "unist-util-visit": "^5.0.0"

plugin/remark-agda.ts

@@ -33,6 +33,15 @@ const remarkAgda: RemarkPlugin = () => {
       {},
     );
 
+    // TODO: Handle child output
+    console.error("--AGDA OUTPUT--")
+    console.error(childOutput);
+    console.error(childOutput.stdout?.toString());
+    console.error(childOutput.stderr?.toString());
+    console.error("--AGDA OUTPUT--")
+    // if (childOutput.status !== 0)
+    //     throw new Error("Agda failed", childOutput.stderr)
+
     const filename = parse(path).base.replace(/\.lagda.md/, ".md");
     const htmlname = parse(path).base.replace(/\.lagda.md/, ".html");
     const fullOutputPath = join(outDir, filename);

scripts/upload-builder.sh

@@ -0,0 +1,12 @@
+#!/usr/bin/env bash
+
+set -euo pipefail
+
+nix build .#docker-builder
+IMAGE_NAME=$(docker load -q -i ./result | cut -d':' -f2,3 | xargs)
+REMOTE_IMAGE_NAME="git.mzhang.io/michael/$IMAGE_NAME"
+docker image tag "$IMAGE_NAME" "$REMOTE_IMAGE_NAME"
+docker push "$REMOTE_IMAGE_NAME"
+
+set -x
+sed -i -E "s~(.*image: )blog-docker-builder:?.*~\1$REMOTE_IMAGE_NAME~" .woodpecker.yml

utils/agda.Dockerfile

@@ -1,23 +0,0 @@
-# FROM haskell:9-slim-buster
-# RUN cabal update
-# RUN cabal install --global Agda-2.6.4
-#
-# FROM debian:buster-slim
-# COPY --from=0 /root/.cabal/bin/agda /usr/bin/agda
-# COPY --from=0 /root/.cabal/store/ghc-9.6.3/Agda-2.6.4-c592e701b6d172f37cf6e17790bc1993481dac7a9e29753b34c448a31924a9ab/share/lib /root/.cabal/store/ghc-9.6.3/Agda-2.6.4-c592e701b6d172f37cf6e17790bc1993481dac7a9e29753b34c448a31924a9ab/share/lib
-# CMD ["agda", "--interactive"]
-
-FROM alpine AS base
-ENV PATH /root/.local/bin:/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin
-RUN apk add --update curl alpine-sdk ncurses-dev gmp-dev zlib-dev
-
-FROM base AS agda-build
-RUN curl -sSL https://get.haskellstack.org/ | sh
-RUN stack install ghc-9.4.7
-RUN git clone --depth 1 --single-branch --branch v2.6.4 https://github.com/agda/agda
-WORKDIR /agda
-RUN stack --stack-yaml stack-9.4.7.yaml install
-
-FROM base
-COPY --from=agda-build /root/.local/bin/agda /usr/bin/agda
-COPY --from=agda-build /agda/.stack-work/install/x86_64-linux-musl/099dc152e5f5edaf6e084b385953a851d037c26c20471a6eefaa57c4704a9540/9.4.7/share/x86_64-linux-ghc-9.4.7/Agda-2.6.4/lib /agda/.stack-work/install/x86_64-linux-musl/099dc152e5f5edaf6e084b385953a851d037c26c20471a6eefaa57c4704a9540/9.4.7/share/x86_64-linux-ghc-9.4.7/Agda-2.6.4/lib

utils/builder.Dockerfile

@@ -1,27 +0,0 @@
-FROM git.mzhang.io/michael/agda:2.6.4-x86_64
-
-FROM node:18-alpine AS node
-RUN apk add --update git
-RUN npm install -g pnpm
-
-FROM node AS astro-build
-WORKDIR /tmp
-RUN git clone https://git.mzhang.io/michael/astro --depth 1
-WORKDIR /tmp/astro
-RUN pnpm install
-RUN pnpm run build
-RUN rm -rf node_modules
-
-
-FROM node
-COPY --from=0 /usr/bin/agda /usr/bin/agda
-COPY --from=0 /agda/.stack-work/install/x86_64-linux-musl/099dc152e5f5edaf6e084b385953a851d037c26c20471a6eefaa57c4704a9540/9.4.7/share/x86_64-linux-ghc-9.4.7/Agda-2.6.4/lib /agda/.stack-work/install/x86_64-linux-musl/099dc152e5f5edaf6e084b385953a851d037c26c20471a6eefaa57c4704a9540/9.4.7/share/x86_64-linux-ghc-9.4.7/Agda-2.6.4/lib
-
-COPY --from=astro-build /tmp/astro /tmp/astro
-WORKDIR /tmp/astro/packages/astro
-RUN pnpm link --global
-WORKDIR /tmp/astro/packages/markdown/remark
-RUN pnpm link --global
-
-WORKDIR /
-