unignore markdown files

undraft
Change the way admonitions work
2024-06-30 20:36:00 -05:00 · 2024-06-29 17:39:27 -05:00 · 2024-06-29 15:15:48 -05:00 · 2024-06-29 15:15:42 -05:00 · 2024-06-29 14:53:45 -05:00 · 2024-06-29 14:05:06 -05:00
288 changed files with 13054 additions and 2341 deletions
--- a/.build.yml
+++ b/.build.yml
@ -0,0 +1,28 @@
+image: alpine/edge
+oauth: pages.sr.ht/PAGES:RW
+packages:
+  - hut
+  - npm
+  - rsync
+  - typst
+environment:
+  site: mzhang.io
+secrets:
+  - 0b26b413-7901-41c3-a4e2-3c752228ffcb
+sources:
+  - https://git.sr.ht/~mzhang/blog
+tasks:
+  - install: |
+      sudo npm install -g pnpm
+  - build: |
+      cd blog
+      pnpm install
+      pnpm run build
+      # hugo --buildDrafts --minify --baseURL https://mzhang.io
+  - upload: |
+      cd blog/dist
+      tar -cvz . > ../site.tar.gz
+      cd ..
+      hut pages publish -d $site site.tar.gz
+      # echo "mzhang.io ssh-ed25519 AAAAC3NzaC1lZDI1NTE5AAAAIBzBZ+QmM4EO3Fwc1ZcvWV2IY9VF04T0H9brorGj9Udp" >> ~/.ssh/known_hosts
+      # rsync -azvrP dist/ sourcehutBuilds@mzhang.io:/mnt/storage/svcdata/blog-public
--- a/.dockerignore
+++ b/.dockerignore
@ -0,0 +1 @@
+*
--- a/.editorconfig
+++ b/.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
--- a/.gitattributes
+++ b/.gitattributes
@ -0,0 +1,2 @@
+public/katex/**/* linguist-vendored
+src/**/*.md  linguist-documentation=false
--- a/.gitignore
+++ b/.gitignore
@ -1,12 +1,32 @@
-/public
-/old
-/resources
-/content/logseq
+# build output
+dist/
+# generated types
+.astro/

-.hugo_build.lock
-.direnv
+# dependencies
+node_modules/
+
+# logs
+npm-debug.log*
+yarn-debug.log*
+yarn-error.log*
+pnpm-debug.log*
+
+
+# environment variables
+.env
+.env.production
+
+# macOS-specific files
+.DS_Store
+
+PragmataPro-Mono-Liga-Regular-Nerd-Font-Complete.woff2
 *.agdai
+_build
+.direnv

-/result*

-/static/fonts/patched/PragmataPro-Mono-Liga-Regular-Nerd-Font-Complete.woff2
+/result
+.pnpm-store
+
+/public/generated
--- a/.prettierignore
+++ b/.prettierignore
@ -0,0 +1,3 @@
+public/katex
+pnpm-lock.yaml
+src/styles/fork-awesome
--- a/.prettierrc.json
+++ b/.prettierrc.json
@ -0,0 +1,17 @@
+{
+  "plugins": ["prettier-plugin-astro"],
+  "overrides": [
+    {
+      "files": "*.astro",
+      "options": {
+        "parser": "astro"
+      }
+    }
+  ],
+
+  "useTabs": false,
+  "tabWidth": 2,
+  "singleQuote": false,
+  "trailingComma": "all",
+  "printWidth": 100
+}
--- a/.tokeignore
+++ b/.tokeignore
@ -0,0 +1,3 @@
+public
+package-lock.json
+src/styles/fork-awesome
--- a/.vscode/extensions.json
+++ b/.vscode/extensions.json
@ -0,0 +1,4 @@
+{
+  "recommendations": ["astro-build.astro-vscode"],
+  "unwantedRecommendations": []
+}
--- a/.vscode/launch.json
+++ b/.vscode/launch.json
@ -0,0 +1,11 @@
+{
+  "version": "0.2.0",
+  "configurations": [
+    {
+      "command": "./node_modules/.bin/astro dev",
+      "name": "Development server",
+      "request": "launch",
+      "type": "node-terminal"
+    }
+  ]
+}
--- a/.woodpecker.yml
+++ b/.woodpecker.yml
@ -1,18 +1,26 @@
-pipeline:
+steps:
  build:
-    image: klakegg/hugo:ext-pandoc-ci
+    image: git.mzhang.io/michael/blog-docker-builder:x0m1c7r2qzc3qbyw8sfv5flfv75xiqdz
+    environment:
+      - ASTRO_TELEMETRY_DISABLED=1
    commands:
-      - hugo --buildDrafts --minify --baseURL https://mzhang.io
+      - mkdir /tmp
+      - rm -rf node_modules
+      - npm i -g pnpm@9.4.0
+      - npx pnpm install --frozen-lockfile
+      - npx pnpm run build
+    when:
+      - event: push

  deploy:
-    image: alpine
+    image: git.mzhang.io/michael/blog-docker-builder:x0m1c7r2qzc3qbyw8sfv5flfv75xiqdz
    commands:
-      - apk add rsync openssh
      - echo "$${SSH_SECRET_KEY}" > SSH_SECRET_KEY
      - chmod 600 SSH_SECRET_KEY
      - mkdir -p ~/.ssh
-      - echo "mzhang.io ssh-ed25519 AAAAC3NzaC1lZDI1NTE5AAAAIBzBZ+QmM4EO3Fwc1ZcvWV2IY9VF04T0H9brorGj9Udp" >> ~/.ssh/known_hosts
-      - rsync -azvrP -e "ssh -i SSH_SECRET_KEY" public/ sourcehutBuilds@mzhang.io:/mnt/storage/svcdata/blog-public
-    secrets: [ SSH_SECRET_KEY ]
+      - echo "mzhang.io ssh-ed25519 AAAAC3NzaC1lZDI1NTE5AAAAIO+RKFYjD8UjqhfOHFHNyijkbGzC4fJEIIhrBwHj+FsQ" >> known_hosts
+      - rsync -azrP -e "ssh -i SSH_SECRET_KEY -o UserKnownHostsFile=known_hosts" dist/ blogDeploy@mzhang.io:/home/blogDeploy/public
+    secrets: [SSH_SECRET_KEY]
    when:
-      branch: master
+      - branch: master
+        event: push
--- a/5
+++ b/5
@ -1,5 +0,0 @@
-serve:
-    hugo serve --bind 0.0.0.0 --buildDrafts
-
-linkcheck:
-    wget --spider -r -nd -nv -H -l 1 http://localhost:1313
--- a/README.md
+++ b/README.md
@ -1,14 +1,5 @@
-# Blog
+# Michael's Blog

-![Build status](https://ci.mzhang.io/api/badges/michael/blog/status.svg)
+https://mzhang.io

-Powers [mzhang.io][1]. Public replies at [~mzhang/public-inbox][2].
-
-Standard hugo site.
-
-Code License: GPL3
-
-Content License: CC BY-SA 4.0
-
-[1]: https://mzhang.io
-[2]: https://lists.sr.ht/~mzhang/public-inbox
+License: GPL-3.0 / CC-BY-SA-4.0
--- a/archetypes/default.md
+++ b/archetypes/default.md
@ -1,6 +0,0 @@
---
-title: "{{ replace .Name "-" " " | title }}"
-date: {{ .Date }}
-draft: true
---
-
--- a/assets/sass/_agda.scss
+++ b/assets/sass/_agda.scss
@ -1,37 +0,0 @@
-/* Aspects. */
-.Agda .Comment       { color: #608b4e }
-.Agda .Background    {}
-.Agda .Markup        { color: #000000 }
-.Agda .Keyword       { color: #569cd6 }
-.Agda .String        { color: #ce9178 }
-.Agda .Number        { color: #b5cea8 }
-.Agda .Symbol        { color: #cccccc }
-.Agda .PrimitiveType { color: #00cdcd }
-.Agda .Pragma        { color: #cccccc }
-.Agda .Operator      {}
-
-/* NameKinds. */
-.Agda .Bound                  { color: black   }
-.Agda .Generalizable          { color: black   }
-.Agda .InductiveConstructor   { color: #cccccc }
-.Agda .CoinductiveConstructor { color: #cccccc }
-.Agda .Datatype               { color: #00cdcd }
-.Agda .Field                  { color: #cccccc }
-.Agda .Function               { color: #cccccc }
-.Agda .Module                 { color: #cccccc }
-.Agda .Postulate              { color: #00cdcd }
-.Agda .Primitive              { color: #b5cea8 }
-.Agda .Record                 { color: #00cdcd }
-
-/* OtherAspects. */
-.Agda .DottedPattern      {}
-.Agda .UnsolvedMeta       { color: black; background: yellow         }
-.Agda .UnsolvedConstraint { color: black; background: yellow         }
-.Agda .TerminationProblem { color: black; background: #FFA07A        }
-.Agda .IncompletePattern  { color: black; background: #F5DEB3        }
-.Agda .Error              { color: red;   text-decoration: underline }
-.Agda .TypeChecks         { color: black; background: #ADD8E6        }
-
-/* Standard attributes. */
-.Agda a { text-decoration: none }
-.Agda a[href]:hover { background-color: darken(#B4EEB4, 60%) }
--- a/assets/sass/_content.scss
+++ b/assets/sass/_content.scss
@ -1,584 +0,0 @@
-@import "footer";
-
-$breakpoint: 720px;
-
-html {
-    min-height: 100vh;
-    margin: 0;
-}
-
-::selection,
-::-moz-selection {
-    background-color: $heading-color;
-    color: $background-color;
-}
-
-body {
-    max-width: 1024px;
-    margin: auto;
-    width: 100%;
-    height: 1px;
-    min-height: 100vh;
-    font-family: $sansfont;
-    font-weight: normal;
-    letter-spacing: -0.025rem;
-
-    background-color: $background-color;
-    color: $text-color;
-}
-
-h1,
-h2,
-h3,
-h4,
-h5,
-h6 {
-    color: $heading-color;
-}
-
-header {
-    margin: auto 12px;
-
-    #header {
-        border-bottom: 2px solid $link-color;
-        box-sizing: border-box;
-        padding: 20px;
-        margin-bottom: 12px;
-
-        #title {
-            font-size: 2.5em;
-            color: $heading-color;
-
-            &:hover {
-                text-decoration: none;
-            }
-        }
-    }
-}
-
-footer {
-    margin: auto 12px;
-
-    margin-top: 24px;
-    margin-bottom: 40px;
-    text-align: center;
-}
-
-.flex-wrapper {
-    display: flex;
-    align-items: stretch;
-}
-
-.side-nav .side-nav-content {
-    display: flex;
-    justify-content: center;
-    gap: 20px;
-
-    .me {
-        display: flex;
-        justify-content: space-evenly;
-        flex-direction: column;
-
-        .links {
-            text-align: center;
-            font-size: 1.5rem;
-
-            a {
-                text-decoration: none;
-                color: $text-color;
-
-                &:hover {
-                    color: $link-color;
-                }
-            }
-        }
-    }
-}
-
-@media screen and (max-width: $breakpoint) {
-    .flex-wrapper {
-        flex-direction: column;
-        .container {
-            padding: 5px 20px;
-        }
-    }
-
-    .side-nav {
-        .side-nav-content {
-            width: 100%;
-            padding: 18px 0;
-            border-bottom: 1px solid $shadow-color;
-            box-shadow: 0 10px 20px -10px $shadow-color;
-
-            .home-link {
-                display: flex;
-                justify-content: space-evenly;
-            }
-            h1.title {
-                margin-bottom: 5px;
-            }
-            .portrait {
-                max-height: 80px;
-            }
-
-            .bio {
-                display: none;
-            }
-        }
-    }
-}
-
-@media screen and (min-width: $breakpoint) {
-    .flex-wrapper {
-        flex-direction: row;
-        .container {
-            padding: 32px 40px 5px 40px;
-        }
-    }
-
-    .side-nav {
-        position: sticky;
-        height: 100%;
-        left: 0;
-        top: 0;
-        // Capital Min to avoid invoking SCSS min
-        width: 30%;
-        min-width: 300px;
-
-        .side-nav-content {
-            padding-top: 32px;
-            padding-right: 32px;
-            padding-left: 32px;
-            border-right: 1px solid $shadow-color;
-            box-shadow: 10px 0 20px -10px $shadow-color;
-            flex-direction: column;
-
-            .portrait {
-                max-width: 100%;
-            }
-
-            h1.title {
-                text-align: center;
-            }
-
-            .links {
-                margin-bottom: 20px;
-            }
-        }
-    }
-}
-
-.side-nav {
-    .side-nav-content {
-        .home-link {
-            text-decoration: none;
-        }
-
-        .portrait {
-            border-radius: 100%;
-        }
-
-        .bio {
-            font-size: 0.85rem;
-
-            ul {
-                padding-left: 12px;
-                list-style-type: "\25B8\00A0";
-            }
-        }
-    }
-}
-
-small {
-    color: $small-text-color;
-}
-
-a {
-    color: $link-color;
-    text-decoration: none;
-
-    &:hover {
-        text-decoration: underline;
-    }
-}
-
-.permalink-container {
-    position: relative;
-    vertical-align: top;
-
-    .permalink {
-        color: $link-color;
-        font-size: 0.65em;
-        position: absolute;
-        left: -25px;
-    }
-}
-
-blockquote {
-    margin-inline: 14px 14px;
-    color: $small-text-color;
-    border-left: 4px solid $small-text-color;
-    padding-left: 12px;
-    font-size: 0.9rem;
-}
-
-.postlisting-row td {
-    padding-bottom: 10px;
-    line-height: 1;
-
-    .title {
-        font-size: 1.1em;
-    }
-
-    &.info {
-        color: $smaller-text-color;
-        font-size: 0.75em;
-        white-space: nowrap;
-    }
-
-    .summary {
-        padding-top: 4px;
-        font-size: 0.64em;
-        color: $smaller-text-color;
-
-        p {
-            display: inline;
-        }
-    }
-}
-
-#content {
-    font-size: 1.05em;
-    line-height: 1.5em;
-
-    img {
-        max-width: 100%;
-    }
-}
-
-code,
-pre > code {
-    font-size: 0.95rem;
-    letter-spacing: -0.035rem;
-}
-
-code {
-    // font-size: 1.2em;
-    font-family: $monofont;
-    box-sizing: border-box;
-    padding: 1px 5px;
-    background-color: $faded-background-color;
-    // color: $code-color;
-}
-
-a code {
-    color: $link-color;
-}
-
-pre > code {
-    color: $text-color;
-    display: block;
-    padding: 5px;
-    overflow-x: auto;
-    font-family: $monofont;
-    line-height: 1.15rem;
-}
-
-details {
-    font-size: 0.95rem;
-
-    summary {
-        cursor: pointer;
-        position: sticky;
-        top: 0;
-        background-color: $background-color;
-    }
-}
-
-table.table {
-    border: 1px solid $faded;
-    border-collapse: collapse;
-
-    thead {
-        background-color: $smaller-text-color;
-        color: $background-color;
-    }
-
-    tbody td,
-    thead th {
-        border: 1px solid $faded;
-        padding: 5px;
-    }
-}
-
-.toc {
-    background-color: lighten($background-color, 10%);
-    padding: 20px;
-
-    ul {
-        margin-block: 0;
-        margin-bottom: 0;
-    }
-}
-
-.post-title {
-    font-size: 2rem;
-    font-weight: 500;
-    margin-bottom: 12px;
-}
-
-.tags {
-    display: flex;
-    gap: 0.75rem;
-    margin-bottom: 6px;
-
-    .tag {
-        font-size: 0.75rem;
-        background-color: $tag-color;
-        padding: 2px 7px;
-
-        &.draft {
-            background-color: orange;
-            color: black;
-        }
-
-        .text {
-            text-decoration: none;
-        }
-
-        &:hover {
-            text-decoration: none;
-        }
-    }
-}
-
-// Tabbing
-.language-switcher-choice {
-    display: none;
-}
-
-.tabbed {
-    border: 1px solid #eee;
-
-    ul.tabs {
-        margin-top: 0;
-        margin-bottom: 0;
-        list-style: none;
-        padding-inline-start: 0;
-        border-bottom: 1px solid lightgray;
-
-        .tab {
-            display: inline-block;
-            list-style: none;
-
-            label {
-                display: inline-block;
-                padding: 4px 8px;
-                font-size: 0.9rem;
-            }
-        }
-    }
-
-    .contents {
-        .tab-content {
-            padding: 0 12px;
-
-            &:not(:last-child) {
-                border-bottom: 1px solid gray;
-            }
-        }
-    }
-}
-
-@for $i from 1 through 5 {
-    $colors: [green, red, blue, yellow, purple];
-
-    .language-switcher-choice:nth-of-type(#{$i}):checked {
-        outline: 2px solid nth($colors, $i);
-    }
-
-    body:has(.language-switcher-choice:nth-of-type(#{$i}):checked) .tabbed {
-        .tabs .tab:nth-child(#{$i}) {
-            border-bottom: 3px solid gray;
-        }
-
-        .tabs .tab:not(:nth-child(#{$i})) {
-            border-bottom: 3px solid transparent;
-        }
-
-        .contents .tab-content:nth-child(#{$i}) {
-            border-bottom: none;
-        }
-
-        .contents .tab-content:not(:nth-child(#{$i})) {
-            // text-shadow: 2px 2px nth($colors, $i);
-            display: none;
-        }
-    }
-}
-
-// Post container
-
-.post-container {
-    display: flex;
-
-    flex-direction: column;
-    .toc-drawer {
-        display: block;
-        summary {
-            font-weight: bold;
-        }
-    }
-    .toc-list {
-        display: none;
-    }
-
-    /*
-    @media screen and (max-width: 520px) {
-        flex-direction: column;
-        .toc-drawer { display: block; }
-        .toc-list { display: none; }
-    }
-
-    @media screen and (min-width: 520px) {
-        flex-direction: row;
-        align-items: flex-start;
-        gap: 12px;
-
-        .toc-drawer { display: none; }
-        .toc-list {
-            top: 0;
-            display: block;
-            position: sticky;
-            min-width: 160px;
-        }
-    }
-    */
-
-    .post-content {
-        ul:not(.tabs) {
-            padding-left: 1.5rem;
-        }
-
-        min-width: 1px;
-
-        details {
-            border: 1px solid $hr-color;
-            // padding: 10px 30px;
-            font-size: 0.9rem;
-            padding: 0 30px;
-            line-height: 1.5;
-
-            p:nth-of-type(1) {
-                padding-top: 0;
-                margin-top: 0;
-            }
-
-            summary {
-                padding: 10px 0;
-                transition: margin 150ms ease-out;
-            }
-
-            &[open] summary {
-                border-bottom: 1px solid $hr-color;
-                margin-bottom: 15px;
-            }
-        }
-
-        hr {
-            border-width: 1px 0 0 0;
-            border-color: $hr-color;
-            margin: 32px auto;
-            width: 20%;
-        }
-
-        .highlight {
-            .lntd:first-child {
-                // border-right: 1px solid lightgray;
-                padding-right: 2px;
-            }
-            .lntd:last-child {
-                padding-left: 12px;
-            }
-        }
-
-        .highlight,
-        details {
-            margin-top: 16px;
-            margin-bottom: 16px;
-        }
-    }
-
-    &.logseq-post {
-        .post-content {
-            > ul {
-                list-style-type: none;
-                padding: 0;
-
-                > li {
-                    margin-bottom: 1em;
-                }
-            }
-        }
-    }
-
-    .toc-draw #TableOfContents,
-    .toc-list #TableOfContents {
-        ul {
-            list-style-type: "\25B8\00A0";
-            padding-left: 1rem;
-
-            li {
-                margin-bottom: 0.5rem;
-            }
-        }
-
-        li ul {
-            margin-top: 0.5rem;
-        }
-    }
-
-    table {
-        border-collapse: collapse;
-
-        thead {
-            background-color: black;
-        }
-
-        td,
-        th {
-            padding: 5px 10px;
-        }
-    }
-}
-
-.division .post-content,
-.post-content {
-    .heading {
-        font-weight: 500;
-
-        a {
-            color: $heading-color;
-        }
-    }
-
-    > p {
-        line-height: 1.5;
-    }
-
-    > p > img {
-        display: block;
-        margin: auto;
-    }
-
-    .footnotes {
-        font-size: 0.9em;
-        line-height: 1.2;
-    }
-}
-
-hr.endline {
-    margin-top: 30px;
-    border-width: 1px 0 0 0;
-    border-color: $hr-color;
-}
--- a/assets/sass/_footer.scss
+++ b/assets/sass/_footer.scss
@ -1,3 +0,0 @@
-footer {
-  font-size: 0.85rem;
-}
--- a/assets/sass/_grid.scss
+++ b/assets/sass/_grid.scss
@ -1,123 +0,0 @@
-// SIMPLE GRID - SASS/SCSS
-
-html,
-body {
-  height: 100%;
-  width: 100%;
-  margin: 0;
-  padding: 0;
-  left: 0;
-  top: 0;
-  font-size: 100%;
-}
-
-// utility
-
-.left {
-  text-align: left;
-}
-
-.right {
-  text-align: right;
-}
-
-.center {
-  text-align: center;
-  margin-left: auto;
-  margin-right: auto;
-}
-
-.justify {
-  text-align: justify;
-}
-
-.hidden-sm {
-  display: none;
-}
-
-// grid
-
-$width: 96%;
-$gutter: 4%;
-$breakpoint-small: 33.75em; // 540px
-$breakpoint-med: 45em; // 720px
-$breakpoint-large: 60em; // 960px
-
-.container {
-  width: 90%;
-  margin-left: auto;
-  margin-right: auto;
-
-  @media only screen and (min-width: $breakpoint-small) {
-    width: 80%;
-  }
-
-  @media only screen and (min-width: $breakpoint-large) {
-    width: 75%;
-    max-width: 60rem;
-  }
-}
-
-.row {
-  position: relative;
-  width: 100%;
-}
-
-.row [class^="col"] {
-  float: left;
-  margin: 0.5rem 2%;
-  min-height: 0.125rem;
-}
-
-.row::after {
-  content: "";
-  display: table;
-  clear: both;
-}
-
-.col-1,
-.col-2,
-.col-3,
-.col-4,
-.col-5,
-.col-6,
-.col-7,
-.col-8,
-.col-9,
-.col-10,
-.col-11,
-.col-12 {
-  width: $width;
-}
-
-.col-1-sm { width:($width / 12) - ($gutter * 11 / 12); }
-.col-2-sm { width: ($width / 6) - ($gutter * 10 / 12); }
-.col-3-sm { width: ($width / 4) - ($gutter * 9 / 12); }
-.col-4-sm { width: ($width / 3) - ($gutter * 8 / 12); }
-.col-5-sm { width: ($width / (12 / 5)) - ($gutter * 7 / 12); }
-.col-6-sm { width: ($width / 2) - ($gutter * 6 / 12); }
-.col-7-sm { width: ($width / (12 / 7)) - ($gutter * 5 / 12); }
-.col-8-sm { width: ($width / (12 / 8)) - ($gutter * 4 / 12); }
-.col-9-sm { width: ($width / (12 / 9)) - ($gutter * 3 / 12); }
-.col-10-sm { width: ($width / (12 / 10)) - ($gutter * 2 / 12); }
-.col-11-sm { width: ($width / (12 / 11)) - ($gutter * 1 / 12); }
-.col-12-sm { width: $width; }
-
-@media only screen and (min-width: $breakpoint-med) {
-  .col-1 { width:($width / 12) - ($gutter * 11 / 12); }
-  .col-2 { width: ($width / 6) - ($gutter * 10 / 12); }
-  .col-3 { width: ($width / 4) - ($gutter * 9 / 12); }
-  .col-4 { width: ($width / 3) - ($gutter * 8 / 12); }
-  .col-5 { width: ($width / (12 / 5)) - ($gutter * 7 / 12); }
-  .col-6 { width: ($width / 2) - ($gutter * 6 / 12); }
-  .col-7 { width: ($width / (12 / 7)) - ($gutter * 5 / 12); }
-  .col-8 { width: ($width / (12 / 8)) - ($gutter * 4 / 12); }
-  .col-9 { width: ($width / (12 / 9)) - ($gutter * 3 / 12); }
-  .col-10 { width: ($width / (12 / 10)) - ($gutter * 2 / 12); }
-  .col-11 { width: ($width / (12 / 11)) - ($gutter * 1 / 12); }
-  .col-12 { width: $width; }
-
-  .hidden-sm {
-    display: block;
-  }
-}
--- a/assets/sass/_home.scss
+++ b/assets/sass/_home.scss
@ -1,137 +0,0 @@
-.obfuscate {
-  user-select: none;
-  display: inline-flex;
-  flex-direction: row-reverse;
-}
-
-.sym-at-sign::before {
-  content: "@";
-}
-
-.sym-dot::before {
-  content: ".";
-}
-
-#homepageContainer {
-  width: 100%;
-  display: flex;
-  flex-direction: row;
-  align-items: center;
-  padding: 12px;
-  box-sizing: border-box;
-  overflow-y: auto;
-
-  #homepage {
-    width: 100%;
-
-    h1#title {
-      font-weight: normal;
-      font-size: 4em;
-      margin: 0;
-      margin-top: 40px;
-    }
-
-    div#about {
-      line-height: 1.5em;
-
-      p {
-        width: 60%;
-        min-width: Min(100%, 520px);
-      }
-
-      a code {
-        color: $code-color;
-
-        &:hover {
-          text-decoration: none;
-        }
-      }
-
-      ul {
-        list-style-type: "\25B8\00A0";
-        padding-left: 1.5em;
-
-        li {
-          padding-left: .5em;
-
-          p {
-            margin: 0.1rem;
-          }
-        }
-      }
-    }
-
-    h2 {
-      font-weight: normal;
-      margin-bottom: 6px;
-      color: $text-color;
-    }
-
-    h2#blog-posts-title {
-      a {
-        text-decoration: none;
-        color: $text-color;
-      }
-    }
-
-    #blog-posts {
-      width: 100%;
-      display: flex;
-      flex-direction: row;
-      align-content: stretch;
-
-      @media screen and (max-width: 520px) {
-        flex-wrap: wrap;
-        gap: 6px;
-      }
-      @media screen and (min-width: 520px) {
-        flex-wrap: no-wrap;
-        gap: 20px;
-      }
-
-      list-style-type: none;
-      padding: 0;
-
-      > li {
-        display: block;
-        width: 100%;
-        padding: 8px;
-        background-color: $faded-background-color;
-        text-decoration: none;
-
-        flex-grow: 1;
-        flex-basis: 100%;
-      }
-
-      .blog-post-link {
-        text-decoration: none;
-
-        .blog-post {
-          display: flex;
-          width: 100%;
-          height: 100%;
-          flex-direction: column;
-          align-content: stretch;
-          justify-content: space-between;
-
-          color: $text-color;
-          text-decoration: none;
-
-          .title {
-            display: flex;
-          }
-
-          .details {
-            text-align: right;
-            color: $smaller-text-color;
-          }
-        }
-
-        &:hover .title {
-          text-decoration: underline;
-          text-decoration-style: dotted;
-        }
-      }
-    }
-  }
-}
--- a/assets/sass/_syntax.scss
+++ b/assets/sass/_syntax.scss
@ -1,177 +0,0 @@
-.highlight .chroma {
-    margin: 0;
-
-    .lntable td.lntd:last-child {
-        background-color: $faded-background-color;
-        padding-right: 12px;
-    }
-}
-
-@media (prefers-color-scheme: light) {
-    /* Other */ .highlight .x {  }
-    /* Error */ .highlight .err { color: #a61717; background-color: #e3d2d2 }
-    /* LineTableTD */ .highlight .lntd { vertical-align: top; padding: 0; margin: 0; border: 0; }
-    /* LineTable */ .highlight .lntable { border-spacing: 0; padding: 0; margin: 0; border: 0; width: auto; overflow: auto; display: block; }
-    /* LineHighlight */ .highlight .hl { display: block; width: 100%;background-color: #ffffcc }
-    /* LineNumbersTable */ .highlight .lnt { margin-right: 0.4em; padding: 0 0.4em 0 0.4em;color: #7f7f7f }
-    /* LineNumbers */ .highlight .ln { margin-right: 0.4em; padding: 0 0.4em 0 0.4em;color: #7f7f7f }
-    /* Keyword */ .highlight .k { color: #000000; font-weight: bold }
-    /* KeywordConstant */ .highlight .kc { color: #000000; font-weight: bold }
-    /* KeywordDeclaration */ .highlight .kd { color: #000000; font-weight: bold }
-    /* KeywordNamespace */ .highlight .kn { color: #000000; font-weight: bold }
-    /* KeywordPseudo */ .highlight .kp { color: #000000; font-weight: bold }
-    /* KeywordReserved */ .highlight .kr { color: #000000; font-weight: bold }
-    /* KeywordType */ .highlight .kt { color: #445588; font-weight: bold }
-    /* Name */ .highlight .n {  }
-    /* NameAttribute */ .highlight .na { color: #008080 }
-    /* NameBuiltin */ .highlight .nb { color: #0086b3 }
-    /* NameBuiltinPseudo */ .highlight .bp { color: #999999 }
-    /* NameClass */ .highlight .nc { color: #445588; font-weight: bold }
-    /* NameConstant */ .highlight .no { color: #008080 }
-    /* NameDecorator */ .highlight .nd { color: #3c5d5d; font-weight: bold }
-    /* NameEntity */ .highlight .ni { color: #800080 }
-    /* NameException */ .highlight .ne { color: #990000; font-weight: bold }
-    /* NameFunction */ .highlight .nf { color: #990000; font-weight: bold }
-    /* NameFunctionMagic */ .highlight .fm {  }
-    /* NameLabel */ .highlight .nl { color: #990000; font-weight: bold }
-    /* NameNamespace */ .highlight .nn { color: #555555 }
-    /* NameOther */ .highlight .nx {  }
-    /* NameProperty */ .highlight .py {  }
-    /* NameTag */ .highlight .nt { color: #000080 }
-    /* NameVariable */ .highlight .nv { color: #008080 }
-    /* NameVariableClass */ .highlight .vc { color: #008080 }
-    /* NameVariableGlobal */ .highlight .vg { color: #008080 }
-    /* NameVariableInstance */ .highlight .vi { color: #008080 }
-    /* NameVariableMagic */ .highlight .vm {  }
-    /* Literal */ .highlight .l {  }
-    /* LiteralDate */ .highlight .ld {  }
-    /* LiteralString */ .highlight .s { color: #dd1144 }
-    /* LiteralStringAffix */ .highlight .sa { color: #dd1144 }
-    /* LiteralStringBacktick */ .highlight .sb { color: #dd1144 }
-    /* LiteralStringChar */ .highlight .sc { color: #dd1144 }
-    /* LiteralStringDelimiter */ .highlight .dl { color: #dd1144 }
-    /* LiteralStringDoc */ .highlight .sd { color: #dd1144 }
-    /* LiteralStringDouble */ .highlight .s2 { color: #dd1144 }
-    /* LiteralStringEscape */ .highlight .se { color: #dd1144 }
-    /* LiteralStringHeredoc */ .highlight .sh { color: #dd1144 }
-    /* LiteralStringInterpol */ .highlight .si { color: #dd1144 }
-    /* LiteralStringOther */ .highlight .sx { color: #dd1144 }
-    /* LiteralStringRegex */ .highlight .sr { color: #009926 }
-    /* LiteralStringSingle */ .highlight .s1 { color: #dd1144 }
-    /* LiteralStringSymbol */ .highlight .ss { color: #990073 }
-    /* LiteralNumber */ .highlight .m { color: #009999 }
-    /* LiteralNumberBin */ .highlight .mb { color: #009999 }
-    /* LiteralNumberFloat */ .highlight .mf { color: #009999 }
-    /* LiteralNumberHex */ .highlight .mh { color: #009999 }
-    /* LiteralNumberInteger */ .highlight .mi { color: #009999 }
-    /* LiteralNumberIntegerLong */ .highlight .il { color: #009999 }
-    /* LiteralNumberOct */ .highlight .mo { color: #009999 }
-    /* Operator */ .highlight .o { color: #000000; font-weight: bold }
-    /* OperatorWord */ .highlight .ow { color: #000000; font-weight: bold }
-    /* Punctuation */ .highlight .p {  }
-    /* Comment */ .highlight .c { color: #999988; font-style: italic }
-    /* CommentHashbang */ .highlight .ch { color: #999988; font-style: italic }
-    /* CommentMultiline */ .highlight .cm { color: #999988; font-style: italic }
-    /* CommentSingle */ .highlight .c1 { color: #999988; font-style: italic }
-    /* CommentSpecial */ .highlight .cs { color: #999999; font-weight: bold; font-style: italic }
-    /* CommentPreproc */ .highlight .cp { color: #999999; font-weight: bold; font-style: italic }
-    /* CommentPreprocFile */ .highlight .cpf { color: #999999; font-weight: bold; font-style: italic }
-    /* Generic */ .highlight .g {  }
-    /* GenericDeleted */ .highlight .gd { color: #000000; background-color: #ffdddd }
-    /* GenericEmph */ .highlight .ge { color: #000000; font-style: italic }
-    /* GenericError */ .highlight .gr { color: #aa0000 }
-    /* GenericHeading */ .highlight .gh { color: #999999 }
-    /* GenericInserted */ .highlight .gi { color: #000000; background-color: #ddffdd }
-    /* GenericOutput */ .highlight .go { color: #888888 }
-    /* GenericPrompt */ .highlight .gp { color: #555555 }
-    /* GenericStrong */ .highlight .gs { font-weight: bold }
-    /* GenericSubheading */ .highlight .gu { color: #aaaaaa }
-    /* GenericTraceback */ .highlight .gt { color: #aa0000 }
-    /* GenericUnderline */ .highlight .gl { text-decoration: underline }
-    /* TextWhitespace */ .highlight .w { color: #bbbbbb }
-}
-
-@media (prefers-color-scheme: dark) {
-    /* Background */ .highlight { color: #e5e5e5; }
-    /* Other */ .highlight .x {  }
-    /* Error */ .highlight .err { color: #ff0000 }
-    /* LineTableTD */ .highlight .lntd { vertical-align: top; padding: 0; margin: 0; border: 0; }
-    /* LineTable */ .highlight .lntable { border-spacing: 0; padding: 0; margin: 0; border: 0; width: auto; overflow: auto; display: block; }
-    /* LineHighlight */ .highlight .hl { display: block; width: 100%;background-color: #ffffcc }
-    /* LineNumbersTable */ .highlight .lnt { margin-right: 0.4em; padding: 0 0.4em 0 0.4em;color: #727272 }
-    /* LineNumbers */ .highlight .ln { margin-right: 0.4em; padding: 0 0.4em 0 0.4em;color: #727272 }
-    /* Keyword */ .highlight .k { color: #ffffff; font-weight: bold }
-    /* KeywordConstant */ .highlight .kc { color: #ffffff; font-weight: bold }
-    /* KeywordDeclaration */ .highlight .kd { color: #ffffff; font-weight: bold }
-    /* KeywordNamespace */ .highlight .kn { color: #ffffff; font-weight: bold }
-    /* KeywordPseudo */ .highlight .kp { color: #ffffff; font-weight: bold }
-    /* KeywordReserved */ .highlight .kr { color: #ffffff; font-weight: bold }
-    /* KeywordType */ .highlight .kt { color: #ffffff; font-weight: bold }
-    /* Name */ .highlight .n {  }
-    /* NameAttribute */ .highlight .na { color: #007f7f }
-    /* NameBuiltin */ .highlight .nb { color: #ffffff; font-weight: bold }
-    /* NameBuiltinPseudo */ .highlight .bp {  }
-    /* NameClass */ .highlight .nc {  }
-    /* NameConstant */ .highlight .no {  }
-    /* NameDecorator */ .highlight .nd {  }
-    /* NameEntity */ .highlight .ni {  }
-    /* NameException */ .highlight .ne {  }
-    /* NameFunction */ .highlight .nf {  }
-    /* NameFunctionMagic */ .highlight .fm {  }
-    /* NameLabel */ .highlight .nl {  }
-    /* NameNamespace */ .highlight .nn {  }
-    /* NameOther */ .highlight .nx {  }
-    /* NameProperty */ .highlight .py {  }
-    /* NameTag */ .highlight .nt { font-weight: bold }
-    /* NameVariable */ .highlight .nv {  }
-    /* NameVariableClass */ .highlight .vc {  }
-    /* NameVariableGlobal */ .highlight .vg {  }
-    /* NameVariableInstance */ .highlight .vi {  }
-    /* NameVariableMagic */ .highlight .vm {  }
-    /* Literal */ .highlight .l {  }
-    /* LiteralDate */ .highlight .ld { color: #ffff00; font-weight: bold }
-    /* LiteralString */ .highlight .s { color: #00ffff; font-weight: bold }
-    /* LiteralStringAffix */ .highlight .sa { color: #00ffff; font-weight: bold }
-    /* LiteralStringBacktick */ .highlight .sb { color: #00ffff; font-weight: bold }
-    /* LiteralStringChar */ .highlight .sc { color: #00ffff; font-weight: bold }
-    /* LiteralStringDelimiter */ .highlight .dl { color: #00ffff; font-weight: bold }
-    /* LiteralStringDoc */ .highlight .sd { color: #00ffff; font-weight: bold }
-    /* LiteralStringDouble */ .highlight .s2 { color: #00ffff; font-weight: bold }
-    /* LiteralStringEscape */ .highlight .se { color: #00ffff; font-weight: bold }
-    /* LiteralStringHeredoc */ .highlight .sh { color: #00ffff; font-weight: bold }
-    /* LiteralStringInterpol */ .highlight .si { color: #00ffff; font-weight: bold }
-    /* LiteralStringOther */ .highlight .sx { color: #00ffff; font-weight: bold }
-    /* LiteralStringRegex */ .highlight .sr { color: #00ffff; font-weight: bold }
-    /* LiteralStringSingle */ .highlight .s1 { color: #00ffff; font-weight: bold }
-    /* LiteralStringSymbol */ .highlight .ss { color: #00ffff; font-weight: bold }
-    /* LiteralNumber */ .highlight .m { color: #ffff00; font-weight: bold }
-    /* LiteralNumberBin */ .highlight .mb { color: #ffff00; font-weight: bold }
-    /* LiteralNumberFloat */ .highlight .mf { color: #ffff00; font-weight: bold }
-    /* LiteralNumberHex */ .highlight .mh { color: #ffff00; font-weight: bold }
-    /* LiteralNumberInteger */ .highlight .mi { color: #ffff00; font-weight: bold }
-    /* LiteralNumberIntegerLong */ .highlight .il { color: #ffff00; font-weight: bold }
-    /* LiteralNumberOct */ .highlight .mo { color: #ffff00; font-weight: bold }
-    /* Operator */ .highlight .o {  }
-    /* OperatorWord */ .highlight .ow {  }
-    /* Punctuation */ .highlight .p {  }
-    /* Comment */ .highlight .c { color: #007f7f }
-    /* CommentHashbang */ .highlight .ch { color: #007f7f }
-    /* CommentMultiline */ .highlight .cm { color: #007f7f }
-    /* CommentSingle */ .highlight .c1 { color: #007f7f }
-    /* CommentSpecial */ .highlight .cs { color: #007f7f }
-    /* CommentPreproc */ .highlight .cp { color: #00ff00; font-weight: bold }
-    /* CommentPreprocFile */ .highlight .cpf { color: #00ff00; font-weight: bold }
-    /* Generic */ .highlight .g {  }
-    /* GenericDeleted */ .highlight .gd {  }
-    /* GenericEmph */ .highlight .ge {  }
-    /* GenericError */ .highlight .gr {  }
-    /* GenericHeading */ .highlight .gh { font-weight: bold }
-    /* GenericInserted */ .highlight .gi {  }
-    /* GenericOutput */ .highlight .go {  }
-    /* GenericPrompt */ .highlight .gp {  }
-    /* GenericStrong */ .highlight .gs { font-weight: bold }
-    /* GenericSubheading */ .highlight .gu { font-weight: bold }
-    /* GenericTraceback */ .highlight .gt {  }
-    /* GenericUnderline */ .highlight .gl { text-decoration: underline }
-    /* TextWhitespace */ .highlight .w {  }
-}
--- a/assets/sass/main.scss
+++ b/assets/sass/main.scss
@ -1,46 +0,0 @@
-$fa-font-path: "/fork-awesome";
-@import "./fork-awesome/fork-awesome.scss";
-
-@import "grid";
-@import "agda";
-@import "mixins";
-@import "fonts";
-
-$sansfont: "Inter", "Helvetica", "Arial", "Liberation Sans", sans-serif;
-$monofont: "PragmataPro Mono Liga", "Roboto Mono", "Roboto Mono for Powerline", "Inconsolata", "Consolas", monospace;
-
-// colors
-
-@media (prefers-color-scheme: light) {
-    $background-color: white;
-    $faded-background-color: darken($background-color, 10%);
-    $shadow-color: darken($background-color, 10%);
-    $heading-color: darken(royalblue, 10%);
-    $text-color: #15202B;
-    $small-text-color: #6e707f;
-    $smaller-text-color: lighten($text-color, 30%);
-    $faded: lightgray;
-    $hr-color: lightgray;
-    $link-color: royalblue;
-    $code-color: firebrick;
-    $tag-color: lighten($link-color, 35%);
-    @import "syntax";
-    @import "content";
-}
-
-@media (prefers-color-scheme: dark) {
-    $background-color: #202030;
-    $faded-background-color: lighten($background-color, 10%);
-    $shadow-color: lighten($background-color, 10%);
-    $heading-color: lighten(lightskyblue, 20%);
-    $text-color: #CDCDCD;
-    $small-text-color: darken($text-color, 8%);
-    $smaller-text-color: darken($text-color, 12%);
-    $faded: #666;
-    $hr-color: gray;
-    $link-color: lightskyblue;
-    $code-color: lighten(firebrick, 25%);
-    $tag-color: darken($link-color, 55%);
-    @import "syntax";
-    @import "content";
-}
--- a/astro.config.ts
+++ b/astro.config.ts
@ -0,0 +1,56 @@
+import { defineConfig } from "astro/config";
+import mdx from "@astrojs/mdx";
+import sitemap from "@astrojs/sitemap";
+import { rehypeAccessibleEmojis } from "rehype-accessible-emojis";
+import remarkReadingTime from "./plugin/remark-reading-time";
+import remarkEmoji from "remark-emoji";
+import remarkDescription from "astro-remark-description";
+import remarkAdmonitions, { mkdocsConfig } from "./plugin/remark-admonitions";
+import remarkMath from "remark-math";
+import rehypeKatex from "rehype-katex";
+import remarkTypst from "./plugin/remark-typst";
+import rehypeLinkHeadings from "@justfork/rehype-autolink-headings";
+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",
+  integrations: [mdx(), sitemap(), markdoc()],
+
+  outDir,
+  base,
+  trailingSlash: "always",
+  publicDir,
+
+  markdown: {
+    syntaxHighlight: "shiki",
+    shikiConfig: { theme: "css-variables" },
+    remarkPlugins: [
+      () => remarkAgda({ outDir, base, publicDir }),
+      remarkMath,
+      [remarkAdmonitions, mkdocsConfig],
+      remarkReadingTime,
+      remarkTypst,
+      remarkEmoji,
+      [
+        remarkDescription,
+        {
+          name: "excerpt",
+        },
+      ],
+    ],
+    rehypePlugins: [
+      [rehypeKatex, {}],
+      rehypeAccessibleEmojis,
+      rehypeSlug,
+      [rehypeLinkHeadings, { behavior: "wrap" }],
+    ],
+  },
+});
--- a/biome.json
+++ b/biome.json
@ -0,0 +1,17 @@
+{
+  "$schema": "https://biomejs.dev/schemas/1.7.3/schema.json",
+  "organizeImports": {
+    "enabled": true
+  },
+  "formatter": {
+    "enabled": true,
+    "indentStyle": "space",
+    "indentWidth": 2
+  },
+  "linter": {
+    "enabled": true,
+    "rules": {
+      "recommended": true
+    }
+  }
+}
--- a/blog.agda-lib
+++ b/blog.agda-lib
@ -1,3 +1,2 @@
-name: blog
+include: src/content/posts src
 depend: standard-library cubical
-include: content/posts
--- a/bun.lockb
+++ b/bun.lockb
--- a/config.toml
+++ b/config.toml
@ -1,33 +0,0 @@
-baseURL = "http://example.org/"
-languageCode = "en-us"
-title = "Michael's Blog"
-enableGitInfo = true
-
-ignoreFiles = ["logseq"]
-enableEmoji = true
-
-[taxonomies]
-tag = "tags"
-language = "languages"
-
-[markup.tableOfContents]
-endLevel = 4
-ordered = false
-startLevel = 2
-
-[markup.goldmark.renderer]
-unsafe = true
-
-[markup.highlight]
-anchorLineNos = true
-codeFences = true
-guessSyntax = false
-hl_Lines = ''
-lineAnchors = ''
-lineNoStart = 1
-lineNos = true
-lineNumbersInTable = true
-noClasses = false
-style = 'monokai'
-tabWidth = 4
-
--- a/content/about/pgp.txt
+++ b/content/about/pgp.txt
@ -1,78 +0,0 @@
-----BEGIN PGP PUBLIC KEY BLOCK-----
-
-mQINBF4Zd7ABEADGHbFm8V6IPZLt7ZFvS0dXMcjpKgWSyeoLGTZYtZ+tLTgAE2Uc
-FCzpNvo7eIu4kZ1bTsLbmVVXaVz0OKnHz+XfgrLnT2uGsABYfv3rwHd/Ia3Oe4Sc
-ZNVI2UPmi/aLQUZGZrTBRflJd8xs4Ckl8OMOh3qMm0M0uHvYH3kb8gAeLMQZlyFi
-P+65NsxNigXlgvtJzkK1vsqUOytYIJsw639f7Kf4W8QZfHTZ3WOOV/UC7Tuq1s0a
-YgcftlQ1b9O5q01rJvVTNHHGv7i/9nhUMFVuUkOw3aAV3gn/e/THX+BWy0HJ/qtB
-MGfeW8U2UKPqjJzxDIlaDXlPoO4rhrk0yL+CKKCCQNx87Z2PvObRz7u36gU0fgFk
-m7sniexroI6lDA5TdWYEcPMlwfMx2zXoFBgx5Sa1pzMw/XJtqG1DFAUsSuc6g3Ty
-5qOH7uSLFdoO3AflSCXMuS77l7595mptW3zkKcvFKre+u9ZejDePZdsjxnWovWC/
-yCenB7dYofpJ1/RPPGdl0AuTouPmb56/u2FJ3yukJXXSBpR3iXwK+u4962vSJd3t
-QUtqAHo23bvvRj0ZSn8ujIcXNVO3QPXHxnSQ86mnwh3CPL6JV+zTwesiVYvxBTHJ
-kzPMWmpYzsJqW5KNOQA09arNvxyRcgIBpKBKZv34dANYvpzWKEQ0icIH8wARAQAB
-tCNNaWNoYWVsIFpoYW5nIDxpcHRxQHByb3Rvbm1haWwuY29tPokCVAQTAQgAPhYh
-BJJezAKJDVza4mGA1L2kejGjyO5rBQJeGXewAhsDBQkDwmcABQsJCAcCBhUKCQgL
-AgQWAgMBAh4BAheAAAoJEL2kejGjyO5rXfgP/2KwYW5d0oEk9m6ZpORf6KkRlV2y
-tEhiYIjAAuyQDfsqUtgfNMbTlK7MGuVhjUTZY6BP+CRO5xPUyGFBYOSOjgtwe/jU
-QNFAhyUwBmWOXxezX1ZL2p5FJDQkiJFOzsCKO76+awalmp9t9pMUDhx8fkM1QcMM
-Czp4QmeUQ+cZQnGQI8mRBMzX7adEUDusMQTtZLbE+mBdP5Uxu16CsR0JalF1OQOu
-fLJx80ywQ0t4448EQJQ4PgLcYRCLN9m3fvMRIZy6BwfCAge7l4EvN7UtljJwQmlA
-vTbdV6QhaaVeRtHUP6ZhZYxVgKxYaVsm0tDV89pkFR0xB+wmrZKMWMcQZ5X1XwC+
-4Ubdmo7kcfcb7D/Sd4C/GkGDP9Jobn0E0YfBemuWJioC9wt71xREsSAWFNAZ3PzE
-XTF6A5sEHXnxzC3r+ei/ivHhjbMJDqVCXmVqUufS7Cf06lqSyOhEpB6I4sn83sSw
-l/RdqzoDsG/FDudxtgO99r3g405cqR9hVZCFleg1stHs7mDaFnlFaHnJTSqlIU4x
-F6XD4niJa2Ti5xY9tHCqnBYXhlQfAwEwIqONGrrxcl/+YWlRANqEEYW7v28+bZvj
-8Pm+QzW4hjCQ7xHTMeXiMu6yd8RrldPfhb79n4Wsn9dH7cBkMLqjILC+zxqhKXfN
-ew6sqp0m+bYRYXBOtB5NaWNoYWVsIFpoYW5nIDxtYWlsQG16aGFuZy5pbz6JAlcE
-EwEKAEECGwMFCQPCZwAFCwkIBwMFFQoJCAsFFgIDAQACHgECF4AWIQSSXswCiQ1c
-2uJhgNS9pHoxo8juawUCX5hUgQIZAQAKCRC9pHoxo8jua6oID/9ktY4qnpVLMjiP
-hfXrFHml/G7jGAPI/8We07VFEC9f4qKCtwiZIesyltDRiuW+Bdokcoz2oykI3dqL
-MBJLLrvNw409MW34CkhuKxJEKifgNGFja7zljWSOZdVERvMifWh+w/B5eqjWR0iy
-HTpAjzVtYHGMKVK9sBgVPnnba5b19vjmEQKLpiVvhxCZejmUgvICm1Q664540LWz
-xFSgJmz6gONanea6URxyvF3yeT2UY7utDKd7LELd0caxNMJMkqgBrEwak2ykS4OZ
-SD1r/kC6pwRTjEHL5uz0nt/IlcUCKJwNplSSyTewfx8wESGzHdEURS6je0OdkKkn
-7t6JH7XLMYwLKW/TAVBQV19IOdvEr/cNWGmpcW/K/U11vFVxYB0v9URWEwqoWsx3
-K/Uz9Kp9i8dqnMy4IfFx6AUMj6aQp9NyrkNB/Oc/C61PCG1/Fq4VHLgy3OLGIOum
-tM3XPUs7BOvg3MCyVYu0coCinss6RLOUKBAuuEc9J+GB1o0m3bcUGF/XmJpopMpL
-S+HlPtlo29FSmGWQdsyO5Ms33WUHYJxt3bA9bnCEwvPojUzY39YjQ3Pvg3VqCzI0
-dhQs9lKUAr+ias7ydzpcTx3tnRsTtmCUV8AlQYE38fgQU8/Y6CZgXn/l32nv4pyi
-0Vdu3wbRSI+QXV6xaSVvtyDgvT09xrQfTWljaGFlbCBaaGFuZyA8bXpoYW5nQHNp
-ZnQubmV0PokCVAQTAQoAPhYhBJJezAKJDVza4mGA1L2kejGjyO5rBQJf/LV9AhsD
-BQkDwmcABQsJCAcDBRUKCQgLBRYCAwEAAh4BAheAAAoJEL2kejGjyO5rKl0P/irR
-bZhZ6kvAUAFot0eBgOJrGTD+3+8n8VnVHb1AGn6Pq7UqObhrR5gT9zf9A0t+x14L
-C8y+e/OI+/hZWdj2z0n79D3X9ZeHBrU00S1gyBoluc+eKN8yW/A8KfwC/IX5c1ov
-nIz/pP5056Dr9nlvZ99gSg3yR73WYodtH7vNQ9QOsiC99dgMEA04KOjSoDeCkWSv
-+6WwFSjDsOz+SyyrU7uQQSbad00aZwArHQ1iRbqaV+/eESY7aI4TbXSVEDZ36QJg
-LvpAO/pkz3nlKE6BRGl8SFjj3Lr5jYf/gH7A7BiYi1F7WnWHTaIIL3uxxj4U5eZB
-Xd1YM8weAMeU9xT7teyPj35vfZtRebmquXkzeBLIzfjCCUEr2XAgIGajsYcI8fl9
-nIGahng1fs1fGah2J3vR3QM9mL2SaQaknU2lEum9XUDiQuIr6GdjfeH0xyfqIEGG
-2S2uiZvTYKkQxCt9cdaeclfJWcQnF+voveRPzzKAIw6q2V2JMaFkd9uTuBkGY+Ar
-q6z6C9McHxzyoGF4/Nlbmrw2dKgD4lY5Hr92WiwwDnqlBhYPEWR2gSidYqXtRgPW
-ICLt1DrBSzMFqNr3hAcXVjOiFklozpDL1RrUhra5azuscirzM9aIHuz85SzLzpCC
-WSvyhSyknOTOp6dmQrt7mjqDPHw11mDYcBMtFmsQuQINBF4Zd7ABEAC5XlB/S3z+
-WErLjskIkEU4+WmuRZh3eHQCgN//fxondOjODHNUIBydAY+7A4PTfvPwvhRKMIAT
-kVCcRtaT3biqL8PZA7ov2Ul3naGsi42nNc4MHi76mZ82LUtuhdRIKIBMsJrR22pW
-/LLgD4tLqfiaKwzijULFkdaPBdElP4S+dbLb7m3CaugwXcJqHzHTS/iGZyC4uD29
-6NlnammB/vANLhWtGGWobnaieFfFaUNoNrT0T6z1zY4TFIRKshT5HixIhn8qFJuM
-cyyjVeimNWekSLyo1UKwxLVkAhu1jAnd8C6g0X3vFbhthCLQqBSlxGtLjJRVRAU2
-WjiXZsleJXsOBuhDj8GnanPZwVNBgjwNPIKY5X17WAFm324SQD6Hyc1qUMvGoKo5
-OmLulBBX6Z9uwSLCe5q9clEwcqqf0KCOQasNkDlUTw34T2Xc47yycc/2UgVnfrXF
-AteFdjmnuvQRRc8J5Gk/R+sclmQNE9v4TPr4gdwiaz2xpclYyy5NhP+4u1G6ovzH
-/jePm2a3ZyejPEzy1JXZp5HwzgTL7WcPq+NHAgNOJ3wn7dxI8MZogzjEdGdQDfe1
-ckh4BKl9PlZ+q9IZvECAm3HVJ5u4N8sF3KmmCQwCPPhoueZF6GzoMnG4fbs1N1jy
-O0K1nfwnFjwz8E9hiWAyEpEZPjndJzs37QARAQABiQI8BBgBCAAmFiEEkl7MAokN
-XNriYYDUvaR6MaPI7msFAl4Zd7ACGwwFCQPCZwAACgkQvaR6MaPI7mvAIQ/+Mtql
-UWC72vXOjoRJ4BQy3B5pj9vgikgH4ePD3FFpgQzd/aWMgsyVhbV75GNOnk5nOHMD
-X0bIVB7sBF8rAtybZEdxc8TS4xmR3wMCFC79TDwf8JTkBNJfYwBZfRzvHjXe0wlE
-TTyCtdg6/nAzmLUcIonVlS2PUSeL+ueTge2b/4lRMOm7KXoPxChcBDQz+IgD38kt
-NnOF+mWAEwIwQzaav4CqEHnB1N+S2exr6THoQmvhE6QK9aUsDmG8vsr210uJDu8r
-d453NMYHONKgkL9IUJpgSWPu/OtEiiRi5mKTWEMeeNYtDJFdk+hszKsp+UzKHgbz
-8/+mbOdqgbcozdQohEfTiy0lsCg/ZW+H9z/NRLHm7ldZqskNvRxlfRC7mVqh8yHd
-EVFeFBXEnlU2RkXvxlxCZaEfsfogFLDlFmQXezMvSP120kWA7dcHQ8GMGJgDHDCj
-cqyzI+0DYd2+Gpj9k6DJvXXb7zsirNY3ffeqTn3D5gcJ2KtSFEr3GUaINgO6dGej
-PK1cmy3B5pp0Q2A4uuIetKZfE0O3oFrqJkqwM1Hn4BiRl5aMb9HiuGfg0G495ojo
-Shnpdft7CEg0kU/RUfLjAxQs4va53Ma86FFG1FMxDpdaPCQcJma2C2Wr5p/2j3d3
-gGtrxbJh/Mhq51seECOEBVQIrF8gnKYMrOkOv10=
-=8UOD
-----END PGP PUBLIC KEY BLOCK-----
--- a/content/about/random-scripts.md
+++ b/content/about/random-scripts.md
@ -1,12 +0,0 @@
-+++
-title = "random scripts"
-+++
-
-### convert a bunch of `flac`s to `mp3`
-
-```bash
-#!/bin/bash
-function flac2mp3() { ffmpeg -y -i "$1" -acodec libmp3lame "$(basename "$1")".mp3; }
-export -f flac2mp3 # only works in bash
-fd "\.flac$" | parallel flac2mp3
-```
--- a/content/about/setup.md
+++ b/content/about/setup.md
@ -1,48 +0,0 @@
-+++
-title = "Setup"
-+++
-
-# Setup
-
-List of software and services I use and endorse, mostly FOSS.
-
-## Desktop
-
- [**Arch Linux**](https://archlinux.org/) OS with rolling releases.
- [**Home manager** (MIT)](https://github.com/nix-community/home-manager) Dotfile manager.
- [**Firefox** (MPL-2.0)](https://www.mozilla.org/firefox) Browser.
- [**Thunderbird** (MPL-2.0)](https://www.thunderbird.net) Email + calendar client.
-
-## Development
-
- [**Neovim** (Apache-2.0/Vim)](https://neovim.io/) Text editor.
-
-## Server
-
- [**NixOS** (MIT)](https://nixos.org/) Declarative and reproducible operating system.
- [**Hugo** (Apache-2.0)](https://gohugo.io/) Static site generator that powers this site.
- [**Gitea** (MIT)](https://gitea.io/) Self-hosted git.
-
-## Mobile
-
- [**DAVx5** (GPL-3.0)](https://www.davx5.com/) CalDAV and CardDAV sync for Android.
- [**Gadgetbridge** (AGPL-3.0)](https://gadgetbridge.org/) Smartwatch client.
- [**K-9 Mail** (Apache-2.0)](https://k9mail.app/) Mail client.
- [**Feeder** (GPL-3.0)](https://f-droid.org/packages/com.nononsenseapps.feeder/) RSS aggregator.
-
-## Music
-
- [**Navidrome** (GPL-3.0)](https://navidrome.com) Self-hosted Subsonic-compatible streaming server.
- [**Sublime Music** (GPL-3.0)](https://sublimemusic.app) GTK Subsonic-compatible music client.
- [**Subtracks** (GPL-3.0)](https://github.com/austinried/subtracks) Android Subsonic-compatible music client.
-
-## Services
-
- [**SourceHut** (AGPL-3.0)](https://sourcehut.org) Git, mailing list, IRC bouncer, etc. hosting.
- [**Element**](https://element.io/) Federated chat provider.
- [**ProtonMail** (Proprietary)](https://protonmail.com/) Encrypted email.
- [**Signal** (GPL-3.0/AGPL-3.0)](https://signal.org/) Encrypted chat.
-
-## Games
-
-Mostly from Steam.
--- a/content/drafts/_index.md
+++ b/content/drafts/_index.md
@ -1,9 +0,0 @@
-+++
-title = "Drafts"
-weight = 1
-hidden = true
-
-[cascade]
-type = "drafts"
-+++
-
--- a/content/posts/2022-10-30-decentralized-identity-middle-ground.md
+++ b/content/posts/2022-10-30-decentralized-identity-middle-ground.md
@ -1,63 +0,0 @@
-+++
-title = "Decentralized Identity, a Middle Ground"
-date = 2022-10-30T03:04:51-05:00
-
-logseq = true
-+++
-
- With Twitter management changing, I'm starting to think about the small web again. The small web is a concept where you use the Internet to interact with people directly, rather than operating through the medium of megacorps. When we think about big monoliths like Twitter and Facebook, at the very heart of it is some kind of algorithm picking what it is we see. And with the power to control that gives us advertising and mass manipulation.
- For the rest of this blog post, I'll be talking about _microblogging_ specifically: short posts of several sentences, along with a few media attachments, of which Twitter is one of the largest monolithic implementations. But the things I talk about are also applicable to other applications, including long-form blogging (Medium), image sharing (Instagram, Snapchat), video sharing (YouTube), chat (Messenger)
- There's several projects out there that are already trying out other extremes. I'll cover two big types here:
-	- **Federation.** This style of application development is inspired by email. The idea is that you develop a common _protocol_ for apps living on different servers to talk to each other, so you can have people choose their own servers rather than trusting everything to megacorps like Google or Facebook. One notable example of this in the microblogging realm is Mastodon / ActivityPub.
-	- **Peer-to-peer.** This style of application development is rarer, but can be seen commonly in things like torrents. The idea is that _each_ client holds all application info, and interacts with everything else as if they were all clients. One notable example of this in the microblogging realm is Scuttlebutt.
- I'll go into more detail about these two styles later, but they both come with their advantages and drawbacks. However, I don't think any of the solutions that exist are sustainable for longer periods of time.
- ## Feature Evaluation
- One thing I've been doing recently when I think about software applications and system design is break things down into their **features**. This makes it a lot easier to compare applications or services to each other than a vague statement like "I've had a good/bad experience with this". So let's come up with some features of a good microblogging platform:
-	- Application design
-		- **Verifiability:** It should be easy to verify if I did indeed ever say something.
-		- **Freedom:** Within reason, I should not be limited in what I say or do on the platform.
-		- **Universality:** I should be able to communicate to anyone from anywhere (any device, any location).
-	- System design
-		- **Availability:** I want to be confident that the system will be around for many years.
-		- **Connectability:** I should be able to connect with people I don't already know easily.
-		- **Moderation:** I should be able to choose to not interact with a certain subset of users, and this process should not be painful.
-	- Scaling
-		- **User scaling:** Supporting more users should incur a relatively linear or sublinear cost, and should certainly not lead to resource consumption blowup.
-		- **Temporal scaling:** The system should support being run for an arbitrarily long amount of time.
-	- Development
-		- **Malleability:** How easy is it to introduce / roll out new versions and features? This may be important for updating cryptographic algorithms.
-		- **Version drift:** Is it possible to support users who are on different version of the service?
- Some features are certainly more important than others, and may have different importance to different people. But it gives me a base line to evaluate services, and lets me decide which features I consider to be critical.
- These are obviously not the only features, but I like to list them in this form because while some
-  alternative apps may tout certain features, it's useless if it falls short on something more important.
- ### Evaluation
- Now that we know what we're looking for, let's evaluate some existing services.
- **Mastodon**
-	- Satisfies:
-		- **Connectability:** It's easy to find other users based on their user ID, which looks like an email so it's easy to share.
-	- Doesn't satisfy:
-		- **Freedom:** While certain instances may be specialized (i.e hobby-focused), it's certainly not great when you are locked out of communicating with someone on another instance because the admins of your respective instances have beef with each other.
-		- **Availability:** For some reason or another, I've seen Mastodon admins give up on their instances. Running an instance is very costly in terms of money and time, so it's not surprising that if an instance owner decides it's simply no longer worth it, the users are simply hosed. While there are some options for migration like redirection, it's useless if the original server doesn't stay online.
- **Scuttlebutt**
-	- Satisfies:
-		- **Freedom:** This is the maximally free solution: your client is solely responsible for receiving and filtering all messages.
-	- Doesn't satisfy:
-		- **Connectability:** Connecting with someone must take place over an existing channel (i.e either meeting in meatspace or sharing a pub). If I don't have my Scuttlebutt client with me, then it's not possible to get updates.
-		- **Universality:** Since user identity is heavily tied to a single client, having multiple clients for a single user is not a well-supported workflow.
- The Matrix people have also developed [Cerulean], a playground for testing the idea of _relative reputation_, where instead of doing moderation of all users you can assign a web-of-trust-style reputation to people you follow. However, this may lead to further filter-bubbling, the implications of which I'm honestly not sure how to tackle.
-
-  [Cerulean]: https://matrix.org/blog/2020/12/18/introducing-cerulean#whats-with-the-decentralised-reputation-button
- ## Decentralized Identity
- My view for an ideal microblogging platform would be a federated server-client architecture, but where a user identity isn't tied to the server the same way a user is tied to their Mastodon instance. Essentially, you want your account to be promiscuous between several servers.
- This way, you gain all of the benefits of having a server-client architecture (easy to do multiple clients), while not relying on the server itself or its admins to stay around for a long time.
- The problem is, designing such a system securely is difficult. Ultimately, what I'm proposing is:
-	- A user identity model based on an asymmetric-key model. Users generate their own key locally and provide it to instances.
-	- Users should then have _client_ keys, which are independent of the user keys. These are signed by the user key to indicate that they belong to the same user.
-	- When a user wants to switch servers, they can begin requesting a checkout of their data from the server. The data can be signed by the server as well to provide an indicator that the client isn't trying to forge old history.
-		- One problem is if a server wants to deny a user from switching servers; they may try to keep the data hostage. One solution is just to scrape all publicly obtainable data, the other is to hope that this is socially discouraged by just having users avoid servers that engage in user-hostile actions.
-	- Users may also opt to replicate their identity entirely between two servers. This just means that this synchronization process is just happening incrementally or periodically rather than just at switch-time.
- This still has a number of open problems:
-	- **Key revocation.** Obviously, anything involving cryptographic keys requires a revocation protocol in the event that the keys are compromised. I'm not too sure of a good way of doing this that doesn't involve an infinitely growing append-only list of revocations on all of the people who have
- When I have some free time, I may take a crack at a proof-of-concept implementation of a system like this.
- ### Further applications
- Since this scheme only really targets the identity layer with (theoretically) asymptotically constant change required for other parts of the software, this should be able to be extended to things other than just microblogging. I'm not sure about the level of success this may have for things like sharing large data files such as video (maybe mix in something like IPFS?), but there is certainly room for exploration.
--- a/content/projects/_index.md
+++ b/content/projects/_index.md
@ -1,11 +0,0 @@
-+++
-title = "Projects"
-type = "projects"
-layout = "single"
-+++
-
-# Projects
-
-This is a curated list of projects I do outside of work for fun. Find the full list on my [Gitea profile][1].
-
-[1]: https://git.mzhang.io/michael
--- a/data/links.yml
+++ b/data/links.yml
@ -1,29 +0,0 @@
- name: Forgejo
-  url: https://git.mzhang.io
-  icon: fa fa-gitea
-  description: Check out my public open source projects on Forgejo
-
- name: Matrix
-  url: https://matrix.to/#/@michael:chat.mzhang.io
-  icon: fa fa-matrix-org
-  description: Come chat with me on Matrix
-
- name: GitHub
-  url: https://github.com/iptq
-  icon: fa fa-github
-  description: See a history of my old projects on GitHub
-
- name: Mastodon
-  url: https://fosstodon.org/@mzhang
-  icon: fa fa-mastodon-square
-  description: Follow my ramblings on Mastodon
-
- name: Keybase
-  url: https://keybase.io/michaelz
-  icon: fa fa-keybase
-  description: Verify my other identities on Keybase
-
- name: LinkedIn
-  url: https://linkedin.com/in/mzhang0
-  icon: fa fa-linkedin
-  description: Connect with me on LinkedIn
--- a/data/projects.yml
+++ b/data/projects.yml
@ -1,80 +0,0 @@
- category: Research Projects
-  desc: Projects that have a large research component compared to software development.
-  projects:
-  - name: Ag Test
-    link: https://git.mzhang.io/proglangs/agtest
-    desc: A small toy attribute grammar.
-    status: incomplete
-    langs: ["python"]
-
-  - name: Coq-SSH
-    link: https://git.mzhang.io/experiment/coq-ssh
-    desc: Attempt at formally verifying SSH protocol through Coq.
-    status: incomplete
-    langs: ["coq", "ocaml"]
-
-  - name: Enterprise
-    link: https://git.mzhang.io/michael/enterprise
-    desc: Statically-compiled interactive programs like Svelte.
-    status: prototype
-    langs: ["rust"]
-
- category: Learning Projects
-  desc: Software development projects used to gain more experience with a particular set of existing technologies.
-  projects:
-  - name: rsld
-    link: https://git.mzhang.io/michael/rsld
-    desc: A parallel rust linker.
-    status: incomplete
-    langs: ["rust"]
-
-  - name: asciinema
-    link: https://git.mzhang.io/michael/asciinema
-    desc: Reimplementation of the terminal recorder asciinema.
-    status: mvp
-    langs: ["rust"]
-
- category: Utility Projects
-  desc: Software that I developed to solve a very specific problem or to make something useful for myself.
-  projects:
-  - name: Panorama
-    link: https://git.mzhang.io/michael/panorama
-    desc: Mail client.
-    status: incomplete
-    langs: ["rust"]
-
-  - name: Leanshot
-    link: https://git.mzhang.io/michael/leanshot
-    desc: Linux screen capture tool.
-    status: works
-    langs: ["rust"]
-
-  - name: Garbage
-    link: https://git.sr.ht/~mzhang/garbage
-    desc: CLI interface to the FreeDesktop Trash Can API.
-    status: works
-    langs: ["rust"]
-
-  - name: Markout
-    link: https://git.mzhang.io/michael/markout
-    desc: Extracts code blocks for a particular language out of Markdown.
-    status: works
-    langs: ["rust"]
-
- category: Miscellaneous
-  desc: Projects that I did for fun or don't really fit in one of the categories above.
-  projects:
-  - name: Cryptopals
-    link: https://git.mzhang.io/michael/cryptopals
-    desc: My solutions to the cryptopals solution, for learning Common Lisp
-    status: incomplete
-    langs: ["common-lisp"]
-
- category: Old Projects
-  desc: Software I wrote in the past and won't be updating.
-  projects:
-  - name: EasyCTF IV Platform
-    link: https://git.mzhang.io/easyctf/easyctf-iv-platform
-    desc: CTF platform for EasyCTF.
-    status: graveyarded
-    langs: ["python"]
--- a/flake.lock
+++ b/flake.lock
@ -1,12 +1,52 @@
 {
  "nodes": {
-    "flake-utils": {
+    "agda": {
+      "inputs": {
+        "flake-parts": "flake-parts",
+        "nixpkgs": "nixpkgs"
+      },
      "locked": {
-        "lastModified": 1659877975,
-        "narHash": "sha256-zllb8aq3YO3h8B/U0/J1WBgAL8EX5yWf5pMj3G0NAmc=",
+        "lastModified": 1719426791,
+        "narHash": "sha256-jiPGzJM+XMwb1OwyxpbY6jV0Lzr5yLKnPSMZbueFNRM=",
+        "owner": "agda",
+        "repo": "agda",
+        "rev": "777b07f573c7526d677c18c25e44b24a849bc03b",
+        "type": "github"
+      },
+      "original": {
+        "owner": "agda",
+        "repo": "agda",
+        "type": "github"
+      }
+    },
+    "flake-parts": {
+      "inputs": {
+        "nixpkgs-lib": "nixpkgs-lib"
+      },
+      "locked": {
+        "lastModified": 1701473968,
+        "narHash": "sha256-YcVE5emp1qQ8ieHUnxt1wCZCC3ZfAS+SRRWZ2TMda7E=",
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "rev": "34fed993f1674c8d06d58b37ce1e0fe5eebcb9f5",
+        "type": "github"
+      },
+      "original": {
+        "owner": "hercules-ci",
+        "repo": "flake-parts",
+        "type": "github"
+      }
+    },
+    "flake-utils": {
+      "inputs": {
+        "systems": "systems"
+      },
+      "locked": {
+        "lastModified": 1710146030,
+        "narHash": "sha256-SZ5L6eA7HJ/nmkzGG7/ISclqe6oZdOZTNoesiInkXPQ=",
        "owner": "numtide",
        "repo": "flake-utils",
-        "rev": "c0e246b9b83f637f4681389ecabcb2681b4f3af0",
+        "rev": "b1d9ab70662946ef0850d488da1c9019f3a9752a",
        "type": "github"
      },
      "original": {
@ -16,11 +56,45 @@
    },
    "nixpkgs": {
      "locked": {
-        "lastModified": 1663593585,
-        "narHash": "sha256-DG6TLLimio1MdBKRTB/dkdUKneJQ+LnNfFT02oIElmE=",
-        "owner": "nixos",
+        "lastModified": 1702346276,
+        "narHash": "sha256-eAQgwIWApFQ40ipeOjVSoK4TEHVd6nbSd9fApiHIw5A=",
+        "owner": "NixOS",
        "repo": "nixpkgs",
-        "rev": "60a27bacb71a009c9479394081aec7b2fc90952a",
+        "rev": "cf28ee258fd5f9a52de6b9865cdb93a1f96d09b7",
+        "type": "github"
+      },
+      "original": {
+        "owner": "NixOS",
+        "ref": "nixos-23.11",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs-lib": {
+      "locked": {
+        "dir": "lib",
+        "lastModified": 1701253981,
+        "narHash": "sha256-ztaDIyZ7HrTAfEEUt9AtTDNoCYxUdSd6NrRHaYOIxtk=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "e92039b55bcd58469325ded85d4f58dd5a4eaf58",
+        "type": "github"
+      },
+      "original": {
+        "dir": "lib",
+        "owner": "NixOS",
+        "ref": "nixos-unstable",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "nixpkgs_2": {
+      "locked": {
+        "lastModified": 1718089647,
+        "narHash": "sha256-COO4Xk2EzlZ3x9KCiJildlAA6cYDSPlnY8ms7pKl2Iw=",
+        "owner": "NixOS",
+        "repo": "nixpkgs",
+        "rev": "f7207adcc68d9cafa29e3cd252a18743ae512c6a",
        "type": "github"
      },
      "original": {
@ -30,8 +104,24 @@
    },
    "root": {
      "inputs": {
+        "agda": "agda",
        "flake-utils": "flake-utils",
-        "nixpkgs": "nixpkgs"
+        "nixpkgs": "nixpkgs_2"
+      }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
      }
    }
  },
--- a/flake.nix
+++ b/flake.nix
@ -1,8 +1,34 @@
 {
-  description = "A very basic flake";
-
-  outputs = { self, nixpkgs, flake-utils }:
+  inputs.agda.url = "github:agda/agda";
+  outputs = { self, nixpkgs, flake-utils, agda, }:
    flake-utils.lib.eachDefaultSystem (system:
-      let pkgs = import nixpkgs { inherit system; };
-      in { devShell = pkgs.mkShell { packages = with pkgs; [ hugo ]; }; });
+      let
+        pkgs = import nixpkgs { inherit system; };
+        agda-pkg = agda.packages.x86_64-linux.default;
+        flakePkgs = rec {
+          agda-bin = pkgs.callPackage ./nix/agda-bin.nix { inherit agda-pkg; };
+          docker-builder =
+            pkgs.callPackage ./nix/docker-builder.nix { inherit agda-bin; };
+        };
+      in {
+        packages = flake-utils.lib.flattenTree flakePkgs;
+        devShell = pkgs.mkShell {
+          ASTRO_TELEMETRY_DISABLED = 1;
+
+          packages = with pkgs;
+            with flakePkgs; [
+              bun
+              woodpecker-cli
+              nixfmt-rfc-style
+              dive
+              nix-tree
+              vips
+              shellcheck
+              agda-bin
+
+              nodejs_20
+              corepack
+            ];
+        };
+      });
 }
--- a/layouts/_default/_markup/render-heading.html
+++ b/layouts/_default/_markup/render-heading.html
@ -1,3 +0,0 @@
-<h{{ .Level }} id="{{ .Anchor | safeURL }}" class="heading">
-  <a href="#{{ .Anchor | safeURL }}">{{ .Text | safeHTML }}</a>
-</h{{ .Level }}>
--- a/layouts/_default/baseof.html
+++ b/layouts/_default/baseof.html
@ -1,51 +0,0 @@
-<!DOCTYPE html>
-<html lang="en">
-    <head>
-        <meta charset="utf-8" />
-        <meta name="viewport" content="width=device-width, initial-scale=1.0" />
-        <title>
-            {{ block "title" . }}{{ end }}
-            Michael Zhang
-        </title>
-
-        {{ block "headExtra" . }}{{ end }}
-        {{ partial "head" . }}
-
-        {{ if .IsHome }}
-            <link rel="me" href="https://fosstodon.org/@mzhang" />
-            <link rel="alternate" type="application/rss+xml" title="RSS Feed" href="/index.xml" />
-        {{ end }}
-
-        {{ $style := resources.Get "sass/main.scss" | resources.ToCSS }}
-        <link rel="stylesheet" href="{{ $style.RelPermalink }}" crossorigin="anonymous" />
-    </head>
-
-    <body>
-        {{ block "body" . }}
-        <div class="flex-wrapper">
-            {{ partial "left-nav" . }}
-
-            <div class="sep"></div>
-
-            <div class="container">
-                {{ block "content" . }}{{ end }}
-            </div>
-        </div>
-
-        <footer>
-            <p>
-                Blog code licensed under <a
-                    href="https://www.gnu.org/licenses/gpl-3.0.txt"
-                    target="_blank">[GPL-3.0]</a>.
-                Post contents licensed under <a
-                    href="https://creativecommons.org/licenses/by-sa/4.0/legalcode.txt">[CC
-                    BY-SA 4.0]</a>.
-                <br />
-                Written by Michael Zhang.
-                <a href="https://git.mzhang.io/michael/blog" class="colorlink"
-                    target="_blank">[Source]</a>.
-            </p>
-        </footer>
-        {{ end }}
-    </body>
-</html>
--- a/layouts/drafts/list.html
+++ b/layouts/drafts/list.html
@ -1,8 +0,0 @@
-{{- define "content" -}}
-
-{{ .Content }}
-
-{{ partial "draft-list" . }}
-
-{{- end -}}
-
--- a/layouts/generic/list.html
+++ b/layouts/generic/list.html
@ -1,18 +0,0 @@
-{{- define "content" -}}
-
-{{ .Content }}
-
-<table style="width: 100%;">
-    {{- range .Pages -}}
-        <tr class="postlisting-row">
-            <td>
-                <a href="{{ .Permalink }}" class="brand-colorlink">{{ .Title }}</a>
-            </td>
-            <td style="text-align: right;">
-                {{ partial "rel-date" .Date }}
-            </td>
-        </tr>
-    {{- end -}}
-</table>
-
-{{- end -}}
--- a/layouts/generic/single.html
+++ b/layouts/generic/single.html
@ -1,5 +0,0 @@
-{{- define "content" -}}
-
-{{ .Content }}
-
-{{- end -}}
--- a/layouts/home.html
+++ b/layouts/home.html
@ -1,9 +0,0 @@
-{{- define "content" -}}
-
-<h2>Blog</h2>
-
-{{ with .GetPage "/posts" }}
-    {{ partial "post-list" . }}
-{{ end }}
-
-{{- end -}}
--- a/layouts/partials/draft-list.html
+++ b/layouts/partials/draft-list.html
@ -1,24 +0,0 @@
-{{ $posts := .Site.GetPage "/posts" }}
-
-<table style="width: 100%;">
-    {{- range $posts.Pages -}}
-        {{ if .Draft }}
-            <tr class="postlisting-row">
-                <td>
-                    <span class="title">
-                        <a href="{{ .RelPermalink }}" class="brand-colorlink">{{ .Title }}</a>
-                    </span>
-                    <br />
-                    <small>
-                        {{ .ReadingTime }} min read -
-
-                        {{ .Date.Format "Mon Jan 02, 2006" }}
-                    </small>
-
-                    <br />
-                </td>
-            </tr>
-        {{ end }}
-    {{- end -}}
-</table>
-
--- a/layouts/partials/head.html
+++ b/layouts/partials/head.html
@ -1 +0,0 @@
-{{ if .Params.math }}{{ partial "katex.html" . }}{{ end }}
--- a/layouts/partials/katex.html
+++ b/layouts/partials/katex.html
@ -1,21 +0,0 @@
-<link rel="stylesheet" href="/katex/katex.min.css">
-<script defer src="/katex/katex.min.js"></script>
-<script defer src="/katex/contrib/auto-render.min.js" onload="renderMathInElement(document.body);"></script>
-
-<script>
-    document.addEventListener("DOMContentLoaded", function() {
-        renderMathInElement(document.body, {
-          // customised options
-          // • auto-render specific keys, e.g.:
-          delimiters: [
-              {left: '$$', right: '$$', display: true},
-              {left: '$', right: '$', display: false},
-              {left: '\\(', right: '\\)', display: false},
-              {left: '\\[', right: '\\]', display: true}
-          ],
-          // • rendering keys, e.g.:
-          throwOnError : false
-        });
-    });
-</script>
-
--- a/layouts/partials/left-nav.html
+++ b/layouts/partials/left-nav.html
@ -1,23 +0,0 @@
-<nav class="side-nav">
-    <div class="side-nav-content">
-        <a href="/" class="portrait">
-            <img class="portrait" src="/self.png" />
-        </a>
-        <div class="me">
-            <h1 class="title">Michael Zhang</h1>
-            <div class="links">
-                {{ range .Site.Data.links }}
-                <a href="{{ .url }}" title="{{ .description }}">
-                    <i class="{{ .icon }}" aria-hidden="true"></i>
-                </a>
-                {{ end }}
-            </div>
-        </div>
-
-        <div class="bio">
-            {{ os.ReadFile "layouts/partials/left-nav.md" | .RenderString }}
-
-            <a href="/about">More &raquo;</a>
-        </div>
-    </div>
-</nav>
--- a/layouts/partials/left-nav.md
+++ b/layouts/partials/left-nav.md
@ -1,8 +0,0 @@
-I'm a masters student at the University of Minnesota advised by [Favonia]. I
-previously worked as a Software Developer at [AWS] and [SIFT]. My
-computing-related interests lie in programming language design and formal
-verification, systems security, cryptography, and distributed systems.
-
-[aws]: https://aws.amazon.com/
-[sift]: https://www.sift.net/
-[favonia]: https://favonia.org/
--- a/layouts/partials/post-list.html
+++ b/layouts/partials/post-list.html
@ -1,16 +0,0 @@
-<table style="width: 100%;">
-    {{- range .Pages -}}
-        {{ if not .Draft }}
-            <tr class="postlisting-row">
-                <td class="info">
-                    {{ .Date.Format "2006 Jan 02" }}
-                </td>
-                <td>
-                    <span class="title">
-                        <a href="{{ .RelPermalink }}" class="brand-colorlink">{{ .Title }}</a>
-                    </span>
-                </td>
-            </tr>
-        {{ end }}
-    {{- end -}}
-</table>
--- a/layouts/posts/list.html
+++ b/layouts/posts/list.html
@ -1,7 +0,0 @@
-{{- define "content" -}}
-
-{{ .Content }}
-
-{{ partial "post-list" . }}
-
-{{- end -}}
--- a/layouts/posts/single.html
+++ b/layouts/posts/single.html
@ -1,82 +0,0 @@
-{{- define "title" }}
-{{ .Title }} -
-{{- end -}}
-
-{{- define "headExtra" -}}
-<meta name="description" content="{{ .Summary }}" />
-<meta property="og:title" content="{{ .Site.Title }}: {{ .Title }}" />
-<meta property="og:url" content="{{ .Permalink }}" />
-<meta property="og:description" content="{{ .Summary }}" />
-<meta property="og:type" content="article" />
-<meta property="article:published_time" content="{{ .Date.Format "2006-01-02T15:04:05Z07:00" }}" />
-{{- end -}}
-
-{{- define "content" -}}
-
-<h1 class="post-title">{{ .Title }}</h1>
-
-<span class="tags">
-    {{ if .Draft }}
-        <a href="/drafts" class="tag draft">
-            <i class="fa fa-warning" aria-hidden="true"></i>
-            <span class="text">draft</span>
-        </a>
-    {{ end }}
-
-    {{ range .Params.tags }}
-        <a href="/tags/{{ . }}" class="tag">
-            <i class="fa fa-tag" aria-hidden="true"></i>
-            <span class="text">{{ . }}</span>
-        </a>
-    {{ end }}
-</span>
-
-<small style="display: block; margin-bottom: 20px;">
-    Posted
-    on {{ .Date.Format "Mon Jan 02, 2006" }}
-    - {{ .ReadingTime }} min read
-</small>
-
-{{ if .Params.language_switcher_languages }}
-    <div class="language_switcher_choices">
-    {{ range $index, $lang := .Page.Params.language_switcher_languages }}
-        <input
-            type="radio"
-            name="language-switcher"
-            class="language-switcher-choice"
-            id="language-switcher-{{ $lang }}"
-            value="{{ $lang }}"
-            {{ if (eq $index 0) }}
-                checked
-            {{ end }}
-        >
-    {{ end }}
-    </div>
-{{ end }}
-
-<div class="post-container
-    {{ if .Params.logseq }}logseq-post{{ end }}
-    ">
-    {{ if .Params.toc }}
-        <div class="toc-drawer">
-            <details>
-                <summary>Table of Contents</summary>
-                {{ .TableOfContents }}
-            </details>
-        </div>
-        <!-- <div class="toc-list"> {{ .TableOfContents }} </div> -->
-    {{ end }}
-    <div id="content" class="post-content">{{ .Content }}</div>
-</div>
-
-<hr class="endline" />
-
-<small>
-    Thanks for reading!
-
-    Have comments? Discuss this post by sending an email to my
-    <a href="https://lists.sr.ht/~mzhang/public-inbox">public inbox</a> using this
-    <a href="mailto:~mzhang/public-inbox@lists.sr.ht?subject=Re: {{ .Title }}">email link</a>.
-</small>
-
-{{- end -}}
--- a/layouts/projects/single.html
+++ b/layouts/projects/single.html
@ -1,33 +0,0 @@
-{{- define "content" -}}
-
-{{ .Content }}
-
-{{ range .Site.Data.projects }}
-<h2>{{ .category }}</h2>
-
-<p>{{ .desc }}</p>
-
-<table class="table">
-    <thead>
-        <tr>
-            <th>Name</th>
-            <th>Description</th>
-            <th>Lang</th>
-            <th>Status</th>
-        </tr>
-    </thead>
-
-    <tbody>
-        {{ range .projects }}
-        <tr>
-            <td><a href="{{ .link }}" target="_blank">{{ .name }}</a></td>
-            <td>{{ .desc }}</td>
-            <td>{{ delimit .langs ", " }}</td>
-            <td>{{ .status }}</td>
-        </tr>
-        {{ end }}
-    </tbody>
-</table>
-{{ end }}
-
-{{- end -}}
--- a/layouts/shortcodes/docUrl.html
+++ b/layouts/shortcodes/docUrl.html
@ -1 +0,0 @@
-https://git.mzhang.io/michael/blog/src/branch/master/content/{{ .Page.File.Path }}
--- a/layouts/shortcodes/language-switcher.html
+++ b/layouts/shortcodes/language-switcher.html
@ -1,28 +0,0 @@
-{{ $_hugo_config := `{ "version": 1 }` }}
-
-{{ $parts := split .Inner "---" }}
-{{ $page := .Page }}
-
-<div class="tabbed">
-
-<ul class="tabs">
-{{ range $index, $snippet := $parts }}
-	{{ $lang := index $page.Params.language_switcher_languages $index }}
-	<li class="tab">
-		<label for="language-switcher-{{ $lang }}">{{ $lang }}</label>
-	</li>
-{{ end }}
-</ul>
-
-
-<div class="contents">
-	{{ range $index, $snippet := $parts }}
-	<div class="tab-content">
-		{{ $snippet | markdownify }}
-	</div>
-	{{ end }}
-</div>
-
-</div>
-
-{{/* Thank you https://codepen.io/MPDoctor/pen/mpJdYe */}}
--- a/layouts/shortcodes/left-nav.html
+++ b/layouts/shortcodes/left-nav.html
@ -1 +0,0 @@
-{{ os.ReadFile "/layouts/partials/left-nav.md" | markdownify }}
--- a/layouts/shortcodes/obfuscate.html
+++ b/layouts/shortcodes/obfuscate.html
@ -1,21 +0,0 @@
-{{/* This is fucked */}}
-
-{{- $sliceOriginal := split .Inner "" -}}
-{{- $len := len $sliceOriginal -}}
-{{- $sliceReversed := slice -}}
-{{- range seq $len -}}
-  {{- $sliceReversed = $sliceReversed | append (index $sliceOriginal (sub $len .)) }}
-{{- end -}}
-
-<span class="obfuscate">
-    {{- range $sliceReversed -}}
-        {{- if (eq . "@") -}}
-            <span class="sym-at-sign"></span>
-        {{- else if (eq . ".") -}}
-            <span class="sym-dot"></span>
-        {{- else -}}
-            <span>{{ . }}</span>
-        {{- end -}}
-        &#8205;
-    {{- end -}}
-</span>
--- a/layouts/taxonomy/list.html
+++ b/layouts/taxonomy/list.html
@ -1,22 +0,0 @@
-{{- define "content" -}}
-
-<h1>{{ .Name }}</h1>
-
-<ul>
-{{- range $name, $value := sort .Data.Pages "Title" -}}
-    {{ if not .Draft }}
-        <li style="margin-bottom: 15px;">
-            <a href="{{ $value.RelPermalink }}">{{ $value.Title }}</a>
-            <br />
-            <small>
-            {{- range $index, $page := $value.Pages -}}
-                {{ if $index }},{{ end }}
-                <a href="{{ $page.RelPermalink }}">{{ $page.Title }}</a>
-            {{- end -}}
-            </small>
-        </li>
-    {{ end }}
-{{- end -}}
-</ul>
-
-{{- end -}}
--- a/nix/agda-bin.nix
+++ b/nix/agda-bin.nix
@ -0,0 +1,23 @@
+{ agda-pkg, runCommand, writeShellScriptBin, writeTextFile, agdaPackages }:
+
+let
+  libraryFile =
+    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} $@
+''
--- a/nix/docker-builder.nix
+++ b/nix/docker-builder.nix
@ -0,0 +1,43 @@
+{ dockerTools
+, agda-bin
+, corepack
+, rsync
+, openssh
+, bash
+, coreutils
+, nodejs_20
+, gnused
+, pkgsLinux
+}:
+
+dockerTools.buildLayeredImage {
+  name = "blog-docker-builder";
+
+  contents = with dockerTools; [
+    agda-bin
+    corepack
+    rsync
+    openssh
+    bash
+    coreutils
+    nodejs_20
+    gnused
+    usrBinEnv
+    caCertificates
+    fakeNss
+  ];
+
+  # fakeRootCommands = ''
+  #   #!${pkgsLinux.runtimeShell}
+  #   ${pkgsLinux.dockerTools.shadowSetup}
+  #   groupadd -r builder
+  #   useradd -r -g builder builder
+  # '';
+}
+
+#   copyToRoot = with dockerTools; buildEnv {
+#     name = "blog-docker-builder-image-root";
+#     paths = [
+#     ];
+#   };
+
--- a/package.json
+++ b/package.json
@ -0,0 +1,55 @@
+{
+  "name": "blog",
+  "type": "module",
+  "version": "0.0.1",
+  "packageManager": "pnpm@9.4.0+sha256.b6fd0bfda555e7e584ad7e56b30c68b01d5a04f9ee93989f4b93ca8473c49c74",
+  "scripts": {
+    "dev": "astro dev",
+    "start": "astro dev",
+    "build": "astro build",
+    "preview": "astro preview",
+    "astro": "astro",
+    "format": "prettier -w ."
+  },
+  "dependencies": {
+    "@astrojs/markdoc": "^0.11.1",
+    "@astrojs/markdown-remark": "^5.1.1",
+    "@astrojs/mdx": "^1.1.5",
+    "@astrojs/rss": "^3.0.0",
+    "@astrojs/sitemap": "^3.1.6",
+    "@justfork/rehype-autolink-headings": "^5.1.1",
+    "astro": "^3.6.5",
+    "astro-imagetools": "^0.9.0",
+    "astro-remark-description": "^1.1.2",
+    "classnames": "^2.5.1",
+    "fork-awesome": "^1.2.0",
+    "katex": "^0.16.10",
+    "lodash-es": "^4.17.21",
+    "mdast-util-to-string": "^4.0.0",
+    "nanoid": "^4.0.2",
+    "reading-time": "^1.5.0",
+    "rehype-accessible-emojis": "^0.3.2",
+    "rehype-katex": "^6.0.3",
+    "remark-emoji": "^4.0.1",
+    "remark-github-beta-blockquote-admonitions": "^2.2.1",
+    "remark-math": "^5.1.1",
+    "remark-parse": "^10.0.2",
+    "sharp": "^0.33.4"
+  },
+  "devDependencies": {
+    "@biomejs/biome": "^1.8.2",
+    "@types/lodash-es": "^4.17.12",
+    "date-fns": "^2.30.0",
+    "hast-util-from-html": "^2.0.1",
+    "hast-util-to-html": "^9.0.1",
+    "mdast": "^3.0.0",
+    "mdast-util-from-markdown": "^2.0.1",
+    "prettier": "^3.3.2",
+    "prettier-plugin-astro": "^0.12.3",
+    "rehype-slug": "^6.0.0",
+    "sass": "^1.77.6",
+    "shiki": "^0.14.7",
+    "unified": "^11.0.5",
+    "unist-util-visit": "^5.0.0"
+  }
+}
--- a/plugin/remark-admonitions.ts
+++ b/plugin/remark-admonitions.ts
@ -0,0 +1,157 @@
+// https://github.com/myl7/remark-github-beta-blockquote-admonitions
+// License: Apache-2.0
+
+import { visit } from "unist-util-visit";
+import type { Data } from "unist";
+import type { BuildVisitor } from "unist-util-visit";
+import type { Blockquote, Paragraph, Text } from "mdast";
+import type { RemarkPlugin } from "@astrojs/markdown-remark";
+import classNames from "classnames";
+
+const remarkAdmonitions: RemarkPlugin =
+  (providedConfig?: Partial<Config>) => (tree) => {
+    visit(tree, handleNode({ ...defaultConfig, ...providedConfig }));
+  };
+
+export default remarkAdmonitions;
+
+const handleNode =
+  (config: Config): BuildVisitor =>
+  (node) => {
+    // Filter required elems
+    if (node.type !== "blockquote") return;
+    const blockquote = node as Blockquote;
+
+    if (blockquote.children[0]?.type !== "paragraph") return;
+
+    const paragraph = blockquote.children[0];
+    if (paragraph.children[0]?.type !== "text") return;
+
+    const text = paragraph.children[0];
+
+    // A link break after the title is explicitly required by GitHub
+    const titleEnd = text.value.indexOf("\n");
+    if (titleEnd < 0) return;
+
+    const textBody = text.value.substring(titleEnd + 1);
+    let title = text.value.substring(0, titleEnd);
+    // Handle whitespaces after the title.
+    // Whitespace characters are defined by GFM
+    const m = /[ \t\v\f\r]+$/.exec(title);
+    if (m && !config.titleKeepTrailingWhitespaces) {
+      title = title.substring(0, title.length - m[0].length);
+    }
+    if (!nameFilter(config.titleFilter)(title)) return;
+    const { displayTitle, checkedTitle } = config.titleTextMap(title);
+
+    // Update the text body
+    text.value = textBody;
+
+    // Insert the title element and add classes for the title
+    const paragraphTitleText: Text = { type: "text", value: displayTitle };
+    const paragraphTitle: Paragraph = {
+      type: "paragraph",
+      children: [paragraphTitleText],
+      data: config.dataMaps.title({
+        hProperties: {
+          className: classNameMap(config.classNameMaps.title)(checkedTitle),
+        },
+      }),
+    };
+    blockquote.children.unshift(paragraphTitle);
+
+    // Add classes for the block
+    blockquote.data = config.dataMaps.block({
+      ...blockquote.data,
+      hProperties: {
+        className: classNameMap(config.classNameMaps.block)(checkedTitle),
+      },
+      // The blockquote should be rendered as a div, which is explicitly required by GitHub
+      hName: "div",
+    });
+  };
+
+const TITLE_PATTERN =
+  /\[\!admonition: (attention|caution|danger|error|hint|important|note|tip|warning)\]/i;
+
+export const mkdocsConfig: Partial<Config> = {
+  classNameMaps: {
+    block: (title) => [
+      "admonition",
+      ...(title.startsWith("admonition: ")
+        ? title.substring("admonition: ".length)
+        : title
+      ).split(" "),
+    ],
+    title: classNames("admonition-title"),
+  },
+
+  titleFilter: (title) => Boolean(title.match(TITLE_PATTERN)),
+
+  titleTextMap: (title: string) => {
+    console.log("title", title);
+    const match = title.match(TITLE_PATTERN);
+    console.log("matches", match);
+    const displayTitle = match?.[1] ?? "";
+    const checkedTitle = displayTitle;
+    return { displayTitle, checkedTitle };
+  },
+};
+
+export interface Config {
+  classNameMaps: {
+    block: ClassNameMap;
+    title: ClassNameMap;
+  };
+  titleFilter: NameFilter;
+  titleTextMap: (title: string) => {
+    displayTitle: string;
+    checkedTitle: string;
+  };
+  dataMaps: {
+    block: (data: Data) => Data;
+    title: (data: Data) => Data;
+  };
+  titleKeepTrailingWhitespaces: boolean;
+  legacyTitle: boolean;
+}
+
+export const defaultConfig: Config = {
+  classNameMaps: {
+    block: "admonition",
+    title: "admonition-title",
+  },
+
+  titleFilter: ["[!NOTE]", "[!IMPORTANT]", "[!WARNING]"],
+
+  titleTextMap: (title) => ({
+    displayTitle: title.substring(2, title.length - 1),
+    checkedTitle: title.substring(2, title.length - 1),
+  }),
+  dataMaps: {
+    block: (data) => data,
+    title: (data) => data,
+  },
+  titleKeepTrailingWhitespaces: false,
+  legacyTitle: false,
+};
+
+type ClassNames = string | string[];
+type ClassNameMap = ClassNames | ((title: string) => ClassNames);
+
+export function classNameMap(gen: ClassNameMap) {
+  return (title: string) => {
+    const classNames = typeof gen === "function" ? gen(title) : gen;
+    return typeof classNames === "object" ? classNames.join(" ") : classNames;
+  };
+}
+
+type NameFilter = ((title: string) => boolean) | string[];
+
+export function nameFilter(filter: NameFilter) {
+  return (title: string) => {
+    return typeof filter === "function"
+      ? filter(title)
+      : filter.includes(title);
+  };
+}
--- a/plugin/remark-agda.ts
+++ b/plugin/remark-agda.ts
@ -0,0 +1,156 @@
+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,
+  existsSync,
+  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 });
+
+  return (tree, { history }) => {
+    const path: string = history[history.length - 1]!;
+    if (!(path.endsWith(".lagda.md") || path.endsWith(".agda"))) return;
+
+    console.log("AGDA:processing path", path);
+
+    const tempDir = mkdtempSync(join(tmpdir(), "agdaRender."));
+    const agdaOutDir = join(tempDir, "output");
+    const agdaOutFilename = parse(path).base.replace(/\.lagda.md/, ".md");
+    const agdaOutFile = join(agdaOutDir, agdaOutFilename);
+    mkdirSync(agdaOutDir, { recursive: true });
+
+    const childOutput = spawnSync(
+      "agda",
+      [
+        "--html",
+        `--html-dir=${agdaOutDir}`,
+        "--highlight-occurrences",
+        "--html-highlight=code",
+        path,
+      ],
+      {},
+    );
+
+    if (childOutput.error || !existsSync(agdaOutFile)) {
+      throw new Error(
+        `Agda error:
+
+        Stdout:
+        ${childOutput.stdout}
+
+        Stderr:
+        ${childOutput.stderr}`,
+        {
+          cause: childOutput.error,
+        },
+      );
+    }
+
+    // // 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--");
+
+    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 htmlname = parse(path).base.replace(/\.lagda.md/, ".html");
+
+    const doc = readFileSync(agdaOutFile);
+
+    // This is the post-processed markdown with HTML code blocks replacing the Agda code blocks
+    const tree2 = fromMarkdown(doc);
+
+    const collectedCodeBlocks: RootContent[] = [];
+    visit(tree2, "html", (node) => {
+      const html = fromHtml(node.value, { fragment: true });
+
+      const firstChild: RootContent = html.children[0]!;
+
+      visit(html, "element", (node) => {
+        if (node.tagName !== "a") return;
+
+        if (node.properties.href) {
+          // 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";
+          }
+        }
+      });
+
+      if (!firstChild?.properties?.className?.includes("Agda")) return;
+
+      const stringContents = toHtml(firstChild);
+      collectedCodeBlocks.push({
+        contents: stringContents,
+      });
+    });
+
+    let idx = 0;
+    visit(tree, "code", (node) => {
+      if (!(node.lang === null || node.lang === "agda")) return;
+
+      node.type = "html";
+      node.value = collectedCodeBlocks[idx].contents;
+      idx += 1;
+    });
+  };
+};
+
+export default remarkAgda;
--- a/plugin/remark-reading-time.ts
+++ b/plugin/remark-reading-time.ts
@ -0,0 +1,16 @@
+import getReadingTime from "reading-time";
+import { toString } from "mdast-util-to-string";
+import type { RemarkPlugin } from "@astrojs/markdown-remark";
+
+const remarkReadingTime: RemarkPlugin = () => {
+  return (tree, { data }) => {
+    const textOnPage = toString(tree);
+    const readingTime = getReadingTime(textOnPage);
+
+    // readingTime.text will give us minutes read as a friendly string,
+    // i.e. "3 min read"
+    data.astro.frontmatter.minutesRead = readingTime.text;
+  };
+};
+
+export default remarkReadingTime;
--- a/plugin/remark-typst.ts
+++ b/plugin/remark-typst.ts
@ -0,0 +1,42 @@
+import type { RemarkPlugin } from "@astrojs/markdown-remark";
+import { mkdtempSync, readFileSync, writeFileSync } from "node:fs";
+import { visit } from "unist-util-visit";
+import { join } from "node:path";
+import { spawnSync } from "node:child_process";
+import { tmpdir } from "node:os";
+
+const remarkTypst: RemarkPlugin = () => {
+  const tmp = mkdtempSync(join(tmpdir(), "typst"));
+  let ctr = 0;
+
+  return (tree) => {
+    visit(
+      tree,
+      (node) => node.type === "code" && node.lang === "typst",
+      (node, index, parent) => {
+        const doc = join(tmp, `${ctr}.typ`);
+        const docOut = join(tmp, `${ctr}.svg`);
+        ctr += 1;
+
+        writeFileSync(doc, node.value);
+        const result = spawnSync(
+          "typst",
+          [
+            "compile",
+            "--format",
+            "svg",
+            doc,
+          ],
+          {},
+        );
+        console.log("OUTPUT", result.stderr.toString());
+
+        const svgOut = readFileSync(docOut);
+        node.type = "html";
+        node.value = svgOut.toString();
+      },
+    );
+  };
+};
+
+export default remarkTypst;
--- a/pnpm-lock.yaml
+++ b/pnpm-lock.yaml
--- a/public/.well-known/atproto-did
+++ b/public/.well-known/atproto-did
@ -0,0 +1 @@
+did:plc:zbg2asfcpyughqspwjjgyc2d
--- a/public/fonts/Inter-Black.ttf
+++ b/public/fonts/Inter-Black.ttf
--- a/public/fonts/Inter-Bold.ttf
+++ b/public/fonts/Inter-Bold.ttf
--- a/public/fonts/Inter-ExtraBold.ttf
+++ b/public/fonts/Inter-ExtraBold.ttf
--- a/public/fonts/Inter-ExtraLight.ttf
+++ b/public/fonts/Inter-ExtraLight.ttf
--- a/public/fonts/Inter-Light.ttf
+++ b/public/fonts/Inter-Light.ttf
--- a/public/fonts/Inter-Medium.ttf
+++ b/public/fonts/Inter-Medium.ttf
--- a/public/fonts/Inter-Regular.ttf
+++ b/public/fonts/Inter-Regular.ttf
--- a/public/fonts/Inter-SemiBold.ttf
+++ b/public/fonts/Inter-SemiBold.ttf
--- a/public/fonts/Inter-Thin.ttf
+++ b/public/fonts/Inter-Thin.ttf
--- a/public/fonts/OFL.txt
+++ b/public/fonts/OFL.txt
--- a/static/fork-awesome/forkawesome-webfont.eot
+++ b/static/fork-awesome/forkawesome-webfont.eot
--- a/static/fork-awesome/forkawesome-webfont.svg
+++ b/static/fork-awesome/forkawesome-webfont.svg
--- a/static/fork-awesome/forkawesome-webfont.ttf
+++ b/static/fork-awesome/forkawesome-webfont.ttf
--- a/static/fork-awesome/forkawesome-webfont.woff
+++ b/static/fork-awesome/forkawesome-webfont.woff
--- a/static/fork-awesome/forkawesome-webfont.woff2
+++ b/static/fork-awesome/forkawesome-webfont.woff2
--- a/public/katex/README.md
+++ b/public/katex/README.md
--- a/public/katex/contrib/auto-render.js
+++ b/public/katex/contrib/auto-render.js
--- a/public/katex/contrib/auto-render.min.js
+++ b/public/katex/contrib/auto-render.min.js
--- a/public/katex/contrib/auto-render.mjs
+++ b/public/katex/contrib/auto-render.mjs
--- a/public/katex/contrib/copy-tex.css
+++ b/public/katex/contrib/copy-tex.css
--- a/public/katex/contrib/copy-tex.js
+++ b/public/katex/contrib/copy-tex.js
--- a/public/katex/contrib/copy-tex.min.css
+++ b/public/katex/contrib/copy-tex.min.css
--- a/public/katex/contrib/copy-tex.min.js
+++ b/public/katex/contrib/copy-tex.min.js
--- a/public/katex/contrib/copy-tex.mjs
+++ b/public/katex/contrib/copy-tex.mjs
--- a/public/katex/contrib/mathtex-script-type.js
+++ b/public/katex/contrib/mathtex-script-type.js
--- a/public/katex/contrib/mathtex-script-type.min.js
+++ b/public/katex/contrib/mathtex-script-type.min.js
--- a/public/katex/contrib/mathtex-script-type.mjs
+++ b/public/katex/contrib/mathtex-script-type.mjs
--- a/public/katex/contrib/mhchem.js
+++ b/public/katex/contrib/mhchem.js
--- a/public/katex/contrib/mhchem.min.js
+++ b/public/katex/contrib/mhchem.min.js
--- a/public/katex/contrib/mhchem.mjs
+++ b/public/katex/contrib/mhchem.mjs
--- a/public/katex/contrib/render-a11y-string.js
+++ b/public/katex/contrib/render-a11y-string.js
--- a/public/katex/contrib/render-a11y-string.min.js
+++ b/public/katex/contrib/render-a11y-string.min.js
--- a/public/katex/contrib/render-a11y-string.mjs
+++ b/public/katex/contrib/render-a11y-string.mjs
--- a/public/katex/fonts/KaTeX_AMS-Regular.ttf
+++ b/public/katex/fonts/KaTeX_AMS-Regular.ttf
--- a/public/katex/fonts/KaTeX_AMS-Regular.woff
+++ b/public/katex/fonts/KaTeX_AMS-Regular.woff
--- a/Show more
+++ b/Show more
Author	SHA1	Message	Date
Michael Zhang	77b3323fc6	unignore markdown files All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2024-06-30 20:36:00 -05:00
Michael Zhang	76ea2d345a	undraft All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2024-06-29 17:39:27 -05:00
Michael Zhang	06d483b3dd	Change the way admonitions work All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2024-06-29 15:15:48 -05:00
Michael Zhang	bbfe4f67ca	More updates	2024-06-29 15:15:42 -05:00
Michael Zhang	9318880a9a	Remove allow unused metas	2024-06-29 14:53:45 -05:00
Michael Zhang	83ceb81f8a	a All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2024-06-29 14:05:06 -05:00
Michael Zhang	043b3ebe74	new blog post All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2024-06-28 20:48:21 -05:00
Michael Zhang	531b33442d	boolean equivalences Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2024-06-28 17:46:08 -05:00
Michael Zhang	85c10d012b	fix agda colors All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2024-06-27 10:27:22 -05:00
Michael Zhang	e0ff5bf910	agda All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2024-06-27 00:43:35 -05:00
Michael Zhang	2b4ca03563	render primitives All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2024-06-27 00:22:46 -05:00
Michael Zhang	c1d92f48f9	Fix space All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2024-06-26 21:04:24 -05:00
Michael Zhang	726554826a	fix deploy All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2024-06-26 20:44:17 -05:00
Michael Zhang	6324b12c33	Update builder Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2024-06-26 20:38:45 -05:00
Michael Zhang	b574a929a7	Update Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2024-06-26 20:29:52 -05:00
Michael Zhang	68823357ab	Add sharp Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2024-06-26 19:50:00 -05:00
Michael Zhang	4f88615c31	Update builder Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2024-06-26 19:47:02 -05:00
Michael Zhang	38e2a8cec5	Update dependencies	2024-06-26 19:42:02 -05:00
Michael Zhang	7375f9c81b	agda building! Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2024-06-26 19:17:01 -05:00
Michael Zhang	a8f1ce9acd	agda plugin	2024-06-26 18:18:47 -05:00
Michael Zhang	b5a5f9cf0a	nix	2024-06-26 18:18:25 -05:00
Michael Zhang	65e5471c3c	ci All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2024-06-21 16:06:43 -05:00
Michael Zhang	5635d03e08	update bio All checks were successful ci/woodpecker/manual/woodpecker Pipeline was successful Details	2024-06-21 15:57:44 -05:00
Michael Zhang	4fb464325c	update th'bio All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2024-06-21 01:09:32 -05:00
Michael Zhang	63d837b264	event: push	2024-06-21 01:00:23 -05:00
Michael Zhang	0d70a68769	Revert "pudate" All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details This reverts commit `435ec21f6e`.	2024-06-21 00:58:59 -05:00
Michael Zhang	5d631561b5	refactoring post Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2024-06-21 00:57:37 -05:00
Michael Zhang	435ec21f6e	pudate Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2024-06-11 13:54:47 -04:00
Michael Zhang	dfbdf2d4ff	update path All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2024-06-11 10:58:14 -04:00
Michael Zhang	216b1c35ed	show left All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2024-06-11 10:53:37 -04:00
Michael Zhang	3fcaeccf48	logical relations All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2024-06-11 10:52:37 -04:00
Michael Zhang	d85b7f729f	update	2024-05-29 13:33:23 -05:00
Michael Zhang	22a8c36fff	add biome config	2024-05-29 13:32:27 -05:00
Michael Zhang	6224860b0a	add goatcounter All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2024-05-03 16:08:54 -05:00
Michael Zhang	4fc2c3e589	Update src/content/posts/2024-05-02-ddr/index.mdx All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2024-05-03 18:13:56 +00:00
Michael Zhang	85ce708153	update All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2024-05-03 06:35:52 -05:00
Michael Zhang	71481acbf1	pipeline All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2024-05-03 06:26:42 -05:00
Michael Zhang	f913eb52e2	ddr	2024-05-03 06:22:47 -05:00
Michael Zhang	b402ee102f	add comments All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2024-05-03 05:00:04 -05:00
Michael Zhang	bc8cb94181	tmp ignore All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2024-05-02 15:51:23 -05:00
Michael Zhang	1cb392dbae	woodpecker Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2024-05-02 15:48:55 -05:00
Michael Zhang	9bb4c462d8	update	2024-05-02 15:06:19 -05:00
Michael Zhang	1d48472aa2	start ddr post	2024-05-02 13:00:04 -05:00
Michael Zhang	1d3a17937d	git attributes	2024-04-21 18:24:14 -05:00
Michael Zhang	cbc83ae11d	what the hell	2024-04-20 18:22:15 -05:00
Michael Zhang	31d4b1fb71	update readme	2024-04-20 01:14:46 -05:00
Michael Zhang	1f454d6883	lambda calc post	2024-04-20 01:14:46 -05:00
Michael Zhang	42cbda6ae1	fix the header issue	2024-04-20 01:14:46 -05:00
Michael Zhang	1f8aac0a5e	use alpine/edge	2024-04-20 01:14:46 -05:00
Michael Zhang	d4fe025437	typst	2024-04-20 01:14:46 -05:00
Michael Zhang	90f7fa2ee9	home to postlist	2024-04-20 01:14:46 -05:00
Michael Zhang	ea600b05f7	make the lines more condensed	2024-04-20 01:14:46 -05:00
Michael Zhang	62b4c105a9	style	2024-04-20 01:14:46 -05:00
Michael Zhang	565de50eb3	change colors	2024-04-20 01:14:46 -05:00
Michael Zhang	f048ce45ac	remove box shadow	2024-04-20 01:14:46 -05:00
Michael Zhang	56c95f6051	bio	2024-04-20 01:14:46 -05:00
Michael Zhang	4768a49fce	css	2024-04-20 01:14:46 -05:00
Michael Zhang	4dafc1b3e8	sourcehut publish	2024-04-20 01:14:46 -05:00
Michael Zhang	e1cb9b5e0f	sudo	2024-04-20 01:14:46 -05:00
Michael Zhang	226264f124	node > npm	2024-04-20 01:14:46 -05:00
Michael Zhang	dbbcc3aae7	build	2024-04-20 01:14:46 -05:00
Michael Zhang	32098a3278	Add 'public/. well-known/atproto-did' Some checks failed ci/woodpecker/manual/woodpecker Pipeline failed Details	2024-02-29 09:06:48 -06:00
Michael Zhang	901fb1c005	a	2024-02-05 15:18:35 -06:00
Michael Zhang	f8e04d7342	install pnpm All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-10-24 14:05:49 -05:00
Michael Zhang	0adaf0c122	try node 20 Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2023-10-24 14:05:09 -05:00
Michael Zhang	da64309feb	undraft path induction post Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2023-10-24 14:02:45 -05:00
Michael Zhang	d70327ffb9	tags on home page Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2023-10-24 14:00:40 -05:00
Michael Zhang	4895546226	minor: parameter -> index All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-10-24 11:02:19 -05:00
Michael Zhang	396e1f5098	not ish All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-10-23 22:22:36 -05:00
Michael Zhang	025437ca10	more sane date format All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-10-23 21:50:45 -05:00
Michael Zhang	bd63dba9df	use the original names All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-10-23 21:38:28 -05:00
Michael Zhang	5216167465	path induction post All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-10-23 21:26:47 -05:00
Michael Zhang	f50ec75e01	comment out all the other build stuff All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-10-12 18:34:57 -05:00
Michael Zhang	0e0249d113	sad Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2023-10-12 17:22:58 -05:00
Michael Zhang	92c7982c0c	wtf	2023-10-11 18:01:49 -05:00
Michael Zhang	183c998199	z Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2023-10-11 17:43:51 -05:00
Michael Zhang	fe2377b0b4	z Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2023-10-11 17:43:31 -05:00
Michael Zhang	0c3659055a	z Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2023-10-11 17:42:41 -05:00
Michael Zhang	8670e8cf7b	a Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2023-10-11 17:40:21 -05:00
Michael Zhang	3e07267470	zz Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2023-10-11 17:38:07 -05:00
Michael Zhang	9ecc011029	a Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2023-10-11 17:36:46 -05:00
Michael Zhang	e22340a98d	test Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2023-10-11 17:34:34 -05:00
Michael Zhang	948c982418	add packages Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2023-10-11 17:30:50 -05:00
Michael Zhang	b33ba945b6	a Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2023-10-11 17:27:56 -05:00
Michael Zhang	5319b38560	build Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2023-10-11 17:19:13 -05:00
Michael Zhang	1e5bef0b6f	use agda Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2023-10-11 16:17:08 -05:00
Michael Zhang	efd0b420dd	build agda Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2023-10-11 16:16:32 -05:00
Michael Zhang	11e1601426	builder Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2023-10-11 14:46:16 -05:00
Michael Zhang	1ff3499e81	rip Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2023-10-11 13:42:22 -05:00
Michael Zhang	43a56c941a	docker shit Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2023-10-11 13:09:15 -05:00
Michael Zhang	3935a8934c	agda fix Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2023-10-11 12:47:18 -05:00
Michael Zhang	3833a310e0	render agda Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2023-10-11 11:48:34 -05:00
Michael Zhang	334e6cb1bf	add edit history All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-10-04 09:16:04 -05:00
Michael Zhang	b36a272815	enable syntax highlighting All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-10-02 17:36:09 -05:00
Michael Zhang	263ed46253	time to bury this forever	2023-09-21 17:40:43 -05:00
Michael Zhang	328680c54b	equality notes Some checks failed ci/woodpecker/push/woodpecker Pipeline was successful Details ci/woodpecker/manual/woodpecker Pipeline failed Details	2023-09-15 01:42:41 -05:00
Michael Zhang	f9e388eb6e	fix ordering issue	2023-09-15 00:35:19 -05:00
Michael Zhang	109c2997c3	border radius All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-09-08 17:24:51 -05:00
Michael Zhang	2d7abd47d0	dont be so verbose All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-09-08 05:15:25 -05:00
Michael Zhang	99e0e5ebab	push Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2023-09-08 05:12:55 -05:00
Michael Zhang	f497f3536a	compiler?	2023-09-08 05:10:52 -05:00
Michael Zhang	6bb860f61a	oops All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-09-01 22:32:18 -05:00
Michael Zhang	ab1597a28b	add utterances Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2023-09-01 22:25:11 -05:00
Michael Zhang	c4b29c5e6f	FUCK All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-09-01 21:38:53 -05:00
Michael Zhang	60db0faba3	fix width All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-09-01 21:37:13 -05:00
Michael Zhang	89ece03307	remove prints	2023-09-01 20:59:39 -05:00
Michael Zhang	a670600ad7	scroll spy All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-09-01 20:59:23 -05:00
Michael Zhang	e3ded78ba3	make toc look better All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-09-01 19:30:15 -05:00
Michael Zhang	13d83842aa	fix padding again All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-09-01 19:26:23 -05:00
Michael Zhang	424c056a09	fix padding All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-09-01 19:25:56 -05:00
Michael Zhang	3bf0200e7e	wip toc All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-09-01 12:38:59 -05:00
Michael Zhang	e94fee5345	latexify All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-09-01 12:05:29 -05:00
Michael Zhang	49cfb3ccc4	no extra padding on left on mobile All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-09-01 10:12:29 -05:00
Michael Zhang	8e1fac9bd5	admonitions All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-09-01 10:09:01 -05:00
Michael Zhang	5ecc5f8eed	update All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-09-01 09:24:12 -05:00
Michael Zhang	b47c8ffae3	cek post revive All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-09-01 09:16:36 -05:00
Michael Zhang	0627d6b0d9	author All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-09-01 08:02:15 -05:00
Michael Zhang	2122aca697	keywords All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-09-01 08:01:19 -05:00
Michael Zhang	4a03a76348	more opengraph metadata All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-09-01 07:59:21 -05:00
Michael Zhang	0ef4b692e4	networking? All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-08-31 23:15:54 -05:00
Michael Zhang	88fd13a01a	code blocks All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-08-31 22:45:24 -05:00
Michael Zhang	2a1ebcf251	intro All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-08-31 22:38:49 -05:00
Michael Zhang	edcbc68af3	changes All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-08-31 22:29:45 -05:00
Michael Zhang	6468b29dd7	minor edits All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-08-31 22:25:25 -05:00
Michael Zhang	62ad559dbd	sidebar styling All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-08-31 22:04:16 -05:00
Michael Zhang	c7c8be95b5	image borders All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-08-31 21:59:12 -05:00
Michael Zhang	b61a54de22	bigger title All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-08-31 21:53:16 -05:00
Michael Zhang	f3d89cfb61	more changes All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-08-31 21:52:21 -05:00
Michael Zhang	83d21cf9b6	remove more technical stuff All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-08-31 21:41:52 -05:00
Michael Zhang	b29d3dda82	mermaid All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-08-31 19:10:20 -05:00
Michael Zhang	8c5c341f44	margin is too big All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-08-31 15:17:40 -05:00
Michael Zhang	35f6d93ca0	about page All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-08-31 14:25:04 -05:00
Michael Zhang	0c6f3ff48a	wording All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-08-31 14:14:48 -05:00
Michael Zhang	322441a144	metadata All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-08-31 10:37:26 -05:00
Michael Zhang	b892dfa000	what All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-08-31 10:33:26 -05:00
Michael Zhang	0c2ac5e521	logseq post	2023-08-31 10:33:14 -05:00
Michael Zhang	10426919e1	include drafts All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-08-31 09:05:06 -05:00
Michael Zhang	86feeefbe3	remove brackets All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-08-31 08:53:36 -05:00
Michael Zhang	2c1b3c5677	blockquote All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-08-31 08:47:19 -05:00
Michael Zhang	e8f1437d95	no padding on links All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-08-31 08:46:08 -05:00
Michael Zhang	e2cc513dd4	a All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-08-31 08:39:21 -05:00
Michael Zhang	c478116f88	fill in site	2023-08-31 03:17:02 -05:00
Michael Zhang	a3a7d84d1e	pragmata All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-08-31 03:09:41 -05:00
Michael Zhang	4a89b35ba3	ok kinda working Some checks failed ci/woodpecker/push/woodpecker Pipeline failed Details	2023-08-31 03:07:03 -05:00
Michael Zhang	4eeec04dad	build works	2023-08-30 23:51:10 -05:00
Michael Zhang	43c5a8f70c	progress	2023-08-30 22:47:22 -05:00
Michael Zhang	4b853c6c86	init astro	2023-08-30 19:30:45 -05:00
Michael Zhang	98d3dddc41	misc All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-07-04 04:42:47 -05:00
Michael Zhang	3f6bdacaf6	conclusion All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-07-04 04:35:40 -05:00
Michael Zhang	abb4f9f8ad	fix intro All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-07-04 04:31:46 -05:00
Michael Zhang	68fb26e7ac	fuck meant to be a draft All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-07-04 04:29:24 -05:00
Michael Zhang	5850483297	new blog post about nginx All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-07-04 04:24:45 -05:00
Michael Zhang	63c7c43afc	Dotted All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-05-08 23:48:58 -05:00
Michael Zhang	353f325bac	Selection color All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-05-08 11:57:42 -05:00
Michael Zhang	28025a8c66	Equivalences post All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-05-08 11:51:29 -05:00
Michael Zhang	7f8137b9f6	add headers All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-05-08 00:39:10 -05:00
Michael Zhang	2f68aae3dd	Update to true \== false post All checks were successful ci/woodpecker/push/woodpecker Pipeline was successful Details	2023-05-08 00:37:13 -05:00
				`@ -1 +0,0 @@`
				`{{ if .Params.math }}{{ partial "katex.html" . }}{{ end }}`
				`@ -1 +0,0 @@`
				`https://git.mzhang.io/michael/blog/src/branch/master/content/{{ .Page.File.Path }}`
				`@ -1 +0,0 @@`
				`{{ os.ReadFile "/layouts/partials/left-nav.md" \| markdownify }}`