Update

.editorconfig

@@ -6,4 +6,4 @@ insert_final_newline = true
 trim_trailing_whitespace = true
 charset = utf-8
 indent_style = space
-indent_size = 4
+indent_size = 2

.woodpecker.yml

@@ -1,6 +1,6 @@
 steps:
   build:
-    image: git.mzhang.io/michael/blog-docker-builder:n409yvghr9s92rshjfca0niqsq5vnpl7
+    image: git.mzhang.io/michael/blog-docker-builder:qr7whzx27pqqakdxm32c7b958ggyg07z
     environment:
       - ASTRO_TELEMETRY_DISABLED=1
     commands:
@@ -13,7 +13,7 @@ steps:
       - event: push
 
   deploy:
-    image: git.mzhang.io/michael/blog-docker-builder:n409yvghr9s92rshjfca0niqsq5vnpl7
+    image: git.mzhang.io/michael/blog-docker-builder:qr7whzx27pqqakdxm32c7b958ggyg07z
     commands:
       - echo "$${SSH_SECRET_KEY}" > SSH_SECRET_KEY
       - chmod 600 SSH_SECRET_KEY

nix/docker-builder.nix

@@ -8,6 +8,7 @@
 , coreutils
 , nodejs_20
 , gnused
+, pkgsLinux
 }:
 
 dockerTools.buildLayeredImage {
@@ -24,7 +25,22 @@ dockerTools.buildLayeredImage {
     gnused
     usrBinEnv
     caCertificates
+    fakeNss
   ];
+
+  # fakeRootCommands = ''
+  #   #!${pkgsLinux.runtimeShell}
+  #   ${pkgsLinux.dockerTools.shadowSetup}
+  #   groupadd -r builder
+  #   useradd -r -g builder builder
+  # '';
+
+  config = {
+    Cmd = ''
+
+    '';
+    # User = "builder:builder";
+  };
 }
 
 #   copyToRoot = with dockerTools; buildEnv {

scripts/upload-builder.sh

@@ -6,7 +6,10 @@ 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
+echo "Created $REMOTE_IMAGE_NAME"
+
+if [ "${1+}" == "push" ]; then
+  docker push "$REMOTE_IMAGE_NAME"
+fi

src/Prelude.agda

@@ -0,0 +1,51 @@
+{-# OPTIONS --cubical-compatible #-}
+
+module Prelude where
+
+open import Agda.Primitive
+
+module 𝟘 where
+  data ⊥ : Set where
+  ¬_ : Set → Set
+  ¬ A = A → ⊥
+open 𝟘 public
+
+module 𝟙 where
+  data ⊤ : Set where
+    tt : ⊤
+open 𝟙 public
+
+module 𝟚 where
+  data Bool : Set where
+    true : Bool
+    false : Bool
+open 𝟚 public
+
+id : {l : Level} {A : Set l} → A → A
+id x = x
+
+module Nat where
+  data ℕ : Set where
+    zero : ℕ
+    suc : ℕ → ℕ
+  {-# BUILTIN NATURAL ℕ #-}
+
+  infixl 6 _+_
+  _+_ : ℕ → ℕ → ℕ
+  zero + n = n
+  suc m + n = suc (m + n)
+open Nat public
+
+infix 4 _≡_
+data _≡_ {l} {A : Set l} : (a b : A) → Set l where
+  instance refl : {x : A} → x ≡ x
+
+transport : {l₁ l₂ : Level} {A : Set l₁} {x y : A}
+  → (P : A → Set l₂)
+  → (p : x ≡ y)
+  → P x → P y
+transport {l₁} {l₂} {A} {x} {y} P refl = id
+
+infix 4 _≢_
+_≢_ : ∀ {A : Set} → A → A → Set
+x ≢ y  =  ¬ (x ≡ y)

src/content/posts/2023-04-21-proving-true-from-false.lagda.md

@@ -13,15 +13,8 @@ These are some imports that are required for code on this page to work properly.
 
 ```agda
 {-# OPTIONS --cubical #-}
-
 open import Cubical.Foundations.Prelude
-open import Data.Bool
+open import Prelude hiding (_≢_; _≡_; refl; transport)
-open import Data.Unit
-open import Data.Empty
-
-¬_ : Set → Set
-¬ A = A → ⊥
-
 infix 4 _≢_
 _≢_ : ∀ {A : Set} → A → A → Set
 x ≢ y  =  ¬ (x ≡ y)
@@ -40,7 +33,6 @@ For many "obvious" statements, it suffices to just write `refl` since the two
 sides are trivially true via rewriting. For example:
 
 ```
-open import Data.Nat
 1+2≡3 : 1 + 2 ≡ 3
 1+2≡3 = refl
 ```

src/content/posts/2023-10-23-path-induction-gadt-perspective.lagda.md

@@ -9,11 +9,15 @@ tags: ["type-theory", "programming-languages"]
 <summary>Imports</summary>
 
 ```
-open import Relation.Binary.PropositionalEquality hiding (J)
+-- These types aren't actually imported to improve CI performance :(
-open import Data.Integer
+-- It doesn't matter what they are, just that they exist
-open import Data.Bool
+data Int : Set where
-open import Data.String
+postulate
-Int = ℤ
+    String : Set
+{-# BUILTIN STRING String #-}
+
+data _≡_ {l} {A : Set l} : (a b : A) → Set l where
+  instance refl : {x : A} → x ≡ x
 ```
 
 </details>