dot color

This reverts commit 435ec21f6e.

.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

.dockerignore

@@ -0,0 +1 @@
+*

.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

.gitattributes

@@ -0,0 +1,2 @@
+public/katex/**/* linguist-vendored
+src/**/*.md  linguist-documentation=false

.gitignore

@@ -1,12 +1,34 @@
-/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
+
+.frontmatter

.prettierignore

@@ -0,0 +1,3 @@
+public/katex
+pnpm-lock.yaml
+src/styles/fork-awesome

.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
+}

.tokeignore

@@ -0,0 +1,4 @@
+public
+package-lock.json
+src/styles/fork-awesome
+pnpm-lock.yaml

.vscode/extensions.json

@@ -0,0 +1,7 @@
+{
+  "recommendations": [
+    "astro-build.astro-vscode",
+    "eliostruyf.vscode-front-matter"
+  ],
+  "unwantedRecommendations": []
+}

.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"
+    }
+  ]
+}

.woodpecker.yml

@@ -1,18 +0,0 @@
-pipeline:
-  build:
-    image: klakegg/hugo:ext-pandoc-ci
-    commands:
-      - hugo --buildDrafts --minify --baseURL https://mzhang.io
-
-  deploy:
-    image: alpine
-    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 ]
-    when:
-      branch: master

.woodpecker/deploy.yml

@@ -0,0 +1,27 @@
+steps:
+  build:
+    image: git.mzhang.io/michael/blog-docker-builder:6gzd1rhcl41y02yw4z9kpjgrhxifqyfs
+    environment:
+      - ASTRO_TELEMETRY_DISABLED=1
+    commands:
+      - 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: git.mzhang.io/michael/blog-docker-builder:6gzd1rhcl41y02yw4z9kpjgrhxifqyfs
+    commands:
+      - mc alias set $AWS_DEFAULT_REGION $AWS_ENDPOINT_URL $AWS_ACCESS_KEY_ID $AWS_SECRET_ACCESS_KEY --api S3v4
+      - mc mirror --overwrite ./dist/ $AWS_DEFAULT_REGION/mzhang-io-website/
+    secrets:
+      - AWS_ACCESS_KEY_ID
+      - AWS_DEFAULT_REGION
+      - AWS_ENDPOINT_URL
+      - AWS_SECRET_ACCESS_KEY
+    when:
+      - branch: master
+        event: push

Justfile

@@ -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

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 code / CC-BY-SA-4.0 contents

archetypes/default.md

@@ -1,6 +0,0 @@
----
-title: "{{ replace .Name "-" " " | title }}"
-date: {{ .Date }}
-draft: true
----
-

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%) }

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;
-}

assets/sass/_footer.scss

@@ -1,3 +0,0 @@
-footer {
-  font-size: 0.85rem;
-}

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;
-  }
-}

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;
-        }
-      }
-    }
-  }
-}

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 {  }
-}

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";
-}

astro.config.ts

@@ -0,0 +1,57 @@
+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",
+  prefetch: true,
+  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" }],
+    ],
+  },
+});

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
+    }
+  }
+}

blog.agda-lib

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

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
-

content/about/_index.md

@@ -1,80 +0,0 @@
-+++
-title = "About"
-weight = 2
-
-[cascade]
-type = "generic"
-layout = "single"
-+++
-
-# About Me
-
-{{< left-nav >}}
-
-<!-- more -->
-
-### Research
-
-Currently, I'm learning about [cubical type theory][cubical]. I'll probably
-write some blog posts as I learn more. My advisor is [Favonia].
-
-### University Involvement
-
-During my time at the University of Minnesota, I like to be actively involved in
-computing related student groups.
-
-- **[GopherHack]**. I'm one of the founding officers at the GopherHack
-    organization, hoping to grow a CTF community at the University. I prepare
-    material for club activities.
-- **[PL Seminar]**. A group focused on reading and discussing programming
-    languages related papers.
-- **[UMN Kernel Object]**. A group dedicated to studying operating system
-    development, created in the aftermath of the UMN Linux kernel controversy.
-
-Previously, I was also involved with:
-
-- **[ACM]**. I was webmaster and wrote the current website, as well as helping
-  out with other events such as CTF.
-- **[SASE]**. I was webmaster and was involved in organizing student group
-  events as well.
-
-### Open-source Projects
-
-Some of the projects I've been working on in my free time include:
-
-- **[Wisesplit]**. A tool for easily splitting the bill with friends.
-- **[Garbage]**. A CLI interface to the trash can API.
-- **[Leanshot]**. A Linux screen capture tool.
-
-More can be found on [this page][12] or my public [Gitea][2].
-
-I've also started making an increased effort at using and supporting [FOSS], and
-other software that're not predatory towards users. As a part of this effort,
-I'm also self-hosting and rewriting some of the services and software that I use
-regularly. Find out what I'm using [here][9].
-
-### Hobbies
-
-I'm also an avid rhythm game player and beatmap creator, mostly involved with
-the free-to-play game [osu!]. Check out some of my beatmaps on my osu!
-[userpage].
-
-I also enjoy playing badminton &#x1F3F8; at the rec.
-
-[2]: https://git.mzhang.io/explore
-[9]: setup
-[10]: pgp.txt
-[12]: ../projects
-[cubical]: https://ncatlab.org/nlab/show/cubical+type+theory
-[favonia]: https://favonia.org
-[foss]: https://en.wikipedia.org/wiki/Free_and_open-source_software
-[garbage]: https://git.sr.ht/~mzhang/garbage
-[gopherhack]: https://gopherhack.com
-[leanshot]: https://git.sr.ht/~mzhang/leanshot
-[osu!]: https://osu.ppy.sh
-[pl seminar]: https://umn-plseminar.github.io
-[userpage]: https://osu.ppy.sh/u/2688103
-[wisesplit]: https://wisesplit.org
-[acm]: https://acm.umn.edu
-[sase]: https://saseumn.org
-[umn kernel object]: https://github.com/UMN-Kernel-Object

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-----

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
-```

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.

content/drafts/_index.md

@@ -1,9 +0,0 @@
-+++
-title = "Drafts"
-weight = 1
-hidden = true
-
-[cascade]
-type = "drafts"
-+++
-

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.

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

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

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"]

flake.lock

@@ -1,12 +1,54 @@
 {
   "nodes": {
-    "flake-utils": {
+    "agda": {
+      "inputs": {
+        "flake-parts": "flake-parts",
+        "nixpkgs": [
+          "nixpkgs"
+        ]
+      },
       "locked": {
-        "lastModified": 1659877975,
-        "narHash": "sha256-zllb8aq3YO3h8B/U0/J1WBgAL8EX5yWf5pMj3G0NAmc=",
+        "lastModified": 1729253305,
+        "narHash": "sha256-S7/C8VGMrXeGhFeYXx1cVBjZlNVB5L1o/SkW0hFm0Jc=",
+        "owner": "agda",
+        "repo": "agda",
+        "rev": "3425ed5543d2e6f98094b834fedcdec3a2fb67a6",
+        "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": 1726560853,
+        "narHash": "sha256-X6rJYSESBVr3hBoH0WbKE5KvhPU5bloyZ2L4K60/fPQ=",
         "owner": "numtide",
         "repo": "flake-utils",
-        "rev": "c0e246b9b83f637f4681389ecabcb2681b4f3af0",
+        "rev": "c1dfcf08411b08f6b8615f7d8971a2bfa81d5e8a",
         "type": "github"
       },
       "original": {
@@ -16,11 +58,11 @@
     },
     "nixpkgs": {
       "locked": {
-        "lastModified": 1663593585,
-        "narHash": "sha256-DG6TLLimio1MdBKRTB/dkdUKneJQ+LnNfFT02oIElmE=",
-        "owner": "nixos",
+        "lastModified": 1729265718,
+        "narHash": "sha256-4HQI+6LsO3kpWTYuVGIzhJs1cetFcwT7quWCk/6rqeo=",
+        "owner": "NixOS",
         "repo": "nixpkgs",
-        "rev": "60a27bacb71a009c9479394081aec7b2fc90952a",
+        "rev": "ccc0c2126893dd20963580b6478d1a10a4512185",
         "type": "github"
       },
       "original": {
@@ -28,11 +70,45 @@
         "type": "indirect"
       }
     },
+    "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"
+      }
+    },
     "root": {
       "inputs": {
+        "agda": "agda",
         "flake-utils": "flake-utils",
         "nixpkgs": "nixpkgs"
       }
+    },
+    "systems": {
+      "locked": {
+        "lastModified": 1681028828,
+        "narHash": "sha256-Vy1rq5AaRuLzOxct8nz4T6wlgyUR7zLU309k9mBC768=",
+        "owner": "nix-systems",
+        "repo": "default",
+        "rev": "da67096a3b9bf56a91d16901293e51ba5b49a27e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nix-systems",
+        "repo": "default",
+        "type": "github"
+      }
     }
   },
   "root": "root",

flake.nix

@@ -1,8 +1,31 @@
 {
-  description = "A very basic flake";
-
-  outputs = { self, nixpkgs, flake-utils }:
+  inputs.agda.url = "github:agda/agda";
+  inputs.agda.inputs.nixpkgs.follows = "nixpkgs";
+  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; overlays = [ agda.overlays.default ]; };
+        agda-pkg = agda.packages.x86_64-linux.default;
+        flakePkgs = rec {
+          agda-bin = pkgs.callPackage ./nix/agda-bin.nix { agda-pkg = pkgs.haskellPackages.Agda.bin; };
+          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
+              nixfmt-rfc-style
+              nix-tree
+              shellcheck
+
+              nodejs_20
+              corepack
+            ];
+        };
+      });
 }

frontmatter.json

@@ -0,0 +1,47 @@
+{
+  "$schema": "https://frontmatter.codes/frontmatter.schema.json",
+  "frontMatter.framework.id": "astro",
+  "frontMatter.preview.host": "http://localhost:4321",
+  "frontMatter.content.publicFolder": "public",
+  "frontMatter.content.pageFolders": [
+    {
+      "title": "posts",
+      "path": "[[workspace]]/src/content/posts"
+    }
+  ],
+  "frontMatter.taxonomy.contentTypes": [
+    {
+      "name": "default",
+      "pageBundle": false,
+      "previewPath": "",
+      "filePrefix": null,
+      "clearEmpty": true,
+      "fields": [
+        {
+          "title": "Title",
+          "name": "title",
+          "type": "string",
+          "single": true
+        },
+        {
+          "title": "Description",
+          "name": "description",
+          "type": "string"
+        },
+        {
+          "title": "Publishing date",
+          "name": "date",
+          "type": "datetime",
+          "default": "{{now}}",
+          "isPublishDate": true
+        },
+        {
+          "title": "Content preview",
+          "name": "heroImage",
+          "type": "image",
+          "isPreviewImage": true
+        }
+      ]
+    }
+  ]
+}

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 }}>

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>

layouts/drafts/list.html

@@ -1,8 +0,0 @@
-{{- define "content" -}}
-
-{{ .Content }}
-
-{{ partial "draft-list" . }}
-
-{{- end -}}
-

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 -}}

layouts/generic/single.html

@@ -1,5 +0,0 @@
-{{- define "content" -}}
-
-{{ .Content }}
-
-{{- end -}}

layouts/home.html

@@ -1,9 +0,0 @@
-{{- define "content" -}}
-
-<h2>Blog</h2>
-
-{{ with .GetPage "/posts" }}
-    {{ partial "post-list" . }}
-{{ end }}
-
-{{- end -}}

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>
-

layouts/partials/head.html

@@ -1 +0,0 @@
-{{ if .Params.math }}{{ partial "katex.html" . }}{{ end }}

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>
-

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>

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/

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>

layouts/posts/list.html

@@ -1,7 +0,0 @@
-{{- define "content" -}}
-
-{{ .Content }}
-
-{{ partial "post-list" . }}
-
-{{- end -}}

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 -}}

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 -}}

layouts/shortcodes/docUrl.html

@@ -1 +0,0 @@
-https://git.mzhang.io/michael/blog/src/branch/master/content/{{ .Page.File.Path }}

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 */}}

layouts/shortcodes/left-nav.html

@@ -1 +0,0 @@
-{{ os.ReadFile "/layouts/partials/left-nav.md" | markdownify }}

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>

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 -}}

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.src}/cubical.agda-lib
+        ${agdaPackages.standard-library.src}/standard-library.agda-lib
+      '';
+    };
+
+  # Add an extra layer of indirection here to prevent all of GHC from being pulled in
+  wtf = runCommand "agda-bin" { } ''
+    cp ${agda-pkg}/bin/agda $out
+  '';
+in
+
+writeShellScriptBin "agda" ''
+  set -euo pipefail
+  exec ${wtf} --library-file=${libraryFile} $@
+''

nix/docker-builder.nix

@@ -0,0 +1,47 @@
+{ dockerTools
+, agda-bin
+, bash
+, corepack
+, coreutils
+, gitMinimal
+, gnused
+, minio-client
+, nodejs_20
+, openssh
+, pkgsLinux
+, rsync
+}:
+
+dockerTools.buildLayeredImage {
+  name = "blog-docker-builder";
+
+  contents = with dockerTools; [
+    agda-bin
+    bash
+    caCertificates
+    corepack
+    coreutils
+    fakeNss
+    gitMinimal
+    gnused
+    minio-client
+    nodejs_20
+    openssh
+    rsync
+    usrBinEnv
+  ];
+
+  # 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 = [
+#     ];
+#   };
+

package.json

@@ -0,0 +1,57 @@
+{
+  "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",
+    "sanitize-html": "^2.13.1",
+    "sharp": "^0.33.4"
+  },
+  "devDependencies": {
+    "@biomejs/biome": "^1.8.2",
+    "@types/lodash-es": "^4.17.12",
+    "@types/sanitize-html": "^2.13.0",
+    "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"
+  }
+}

plugin/remark-admonitions.ts

@@ -0,0 +1,155 @@
+// 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) => {
+    const match = title.match(TITLE_PATTERN);
+    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);
+  };
+}

plugin/remark-agda.ts

@@ -0,0 +1,178 @@
+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, resolve, basename } 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");
+    mkdirSync(agdaOutDir, { recursive: true });
+
+    const childOutput = spawnSync(
+      "agda",
+      [
+        "--html",
+        `--html-dir=${agdaOutDir}`,
+        "--highlight-occurrences",
+        "--html-highlight=code",
+        path,
+      ],
+      {},
+    );
+
+    // Locate output file
+    const directory = readdirSync(agdaOutDir);
+    const outputFilename = directory.find((name) => name.endsWith(".md"));
+
+    if (childOutput.status !== 0 || outputFilename === undefined) {
+      throw new Error(
+        `Agda output:
+
+        Stdout:
+        ${childOutput.stdout}
+
+        Stderr:
+        ${childOutput.stderr}
+        `,
+        {
+          cause: childOutput.error,
+        },
+      );
+    }
+
+    const outputFile = join(agdaOutDir, outputFilename);
+
+    // // 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 = basename(resolve(outputFile)).replace(
+      /(\.lagda)?\.md/,
+      ".html",
+    );
+
+    const doc = readFileSync(outputFile);
+
+    // 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;
+    try {
+      visit(tree, "code", (node) => {
+        if (!(node.lang === null || node.lang === "agda")) return;
+
+        if (idx > collectedCodeBlocks.length) {
+          throw new Error("failed");
+        }
+
+        node.type = "html";
+        node.value = collectedCodeBlocks[idx].contents;
+        idx += 1;
+      });
+    } catch (e) {
+      // TODO: Figure out a way to handle this correctly
+      // Possibly by diffing?
+      console.log(
+        "Mismatch in number of args. Perhaps there was an empty block?",
+      );
+    }
+  };
+};
+
+export default remarkAgda;

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;

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;

public/.well-known/atproto-did

@@ -0,0 +1 @@
+did:plc:zbg2asfcpyughqspwjjgyc2d