astro.config.ts

@@ -5,7 +5,7 @@ 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 remarkAdmonitions from "./plugin/remark-admonitions";
 import remarkMath from "remark-math";
 import rehypeKatex from "rehype-katex";
 import remarkTypst from "./plugin/remark-typst";
@@ -35,7 +35,7 @@ export default defineConfig({
     remarkPlugins: [
       () => remarkAgda({ outDir, base, publicDir }),
       remarkMath,
-      [remarkAdmonitions, mkdocsConfig],
+      remarkAdmonitions,
       remarkReadingTime,
       remarkTypst,
       remarkEmoji,

plugin/remark-admonitions.ts

@@ -6,7 +6,6 @@ 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) => {
@@ -15,9 +14,7 @@ const remarkAdmonitions: RemarkPlugin =
 
 export default remarkAdmonitions;
 
-const handleNode =
+const handleNode = (config: Config): BuildVisitor => (node) => {
-  (config: Config): BuildVisitor =>
-  (node) => {
   // Filter required elems
   if (node.type !== "blockquote") return;
   const blockquote = node as Blockquote;
@@ -71,43 +68,46 @@ const handleNode =
   });
 };
 
-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
+        : title).split(
-      ).split(" "),
+          " ",
+        ),
     ],
-    title: classNames("admonition-title"),
+    title: "admonition-title",
   },
-
+  titleFilter: (title) =>
-  titleFilter: (title) => Boolean(title.match(TITLE_PATTERN)),
+    (title.startsWith("[!admonition: ") && title.endsWith("]")) ||
-
+    (Boolean(
-  titleTextMap: (title: string) => {
+      title.match(
-    console.log("title", title);
+        /^\[!(attention|caution|danger|error|hint|important|note|tip|warning)/,
-    const match = title.match(TITLE_PATTERN);
+      ),
-    console.log("matches", match);
+    ) &&
-    const displayTitle = match?.[1] ?? "";
+      title.endsWith("]")),
-    const checkedTitle = displayTitle;
+  titleTextMap: (title) => {
+    title = title.substring(2, title.length - 1);
+    // ' "' will not occur in classes
+    const i = title.indexOf(' "');
+    const displayTitle = i >= 0
+      ? title.substring(i + 2, title.length - 1) // Display title is wrapped with ""
+      : "";
+    const checkedTitle = title.substring(0, i);
     return { displayTitle, checkedTitle };
   },
 };
-
 export interface Config {
   classNameMaps: {
     block: ClassNameMap;
     title: ClassNameMap;
   };
   titleFilter: NameFilter;
-  titleTextMap: (title: string) => {
+  titleTextMap: (
-    displayTitle: string;
+    title: string,
-    checkedTitle: string;
+  ) => { displayTitle: string; checkedTitle: string };
-  };
   dataMaps: {
     block: (data: Data) => Data;
     title: (data: Data) => Data;
@@ -121,9 +121,7 @@ export const defaultConfig: Config = {
     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),

src/content/posts/2023-03-29-shell-in-docker-compose-container-without-shell.md

@@ -12,7 +12,7 @@ container without exiting it. Some Docker containers are incredibly stripped
 down to optimize away bloat (which is good!) but this may make debugging them
 relatively annoying.
 
-> [!admonition: NOTE]
+> [!NOTE]
 > These are my specific steps for running it, please replace the paths and
 > container names with the ones relevant to your specific use-case.
 

src/content/posts/2023-04-20-developing-without-flake.md

@@ -61,7 +61,7 @@ I shove new config files in their root directory.
      flake.nix ✗
 ```
 
-> [!admonition: NOTE]
+> [!NOTE]
 > The `✗` indicates that I added the file to the project, and it hasn't been
 > committed to the repo yet.
 
@@ -131,7 +131,7 @@ project structure should look a bit more like this:
      flake.nix
 ```
 
-> [!admonition: NOTE]
+> [!NOTE]
 > Remember, since you moved the `.envrc` file, you will need to run `direnv allow`
 > again. Depending on how you moved it, you might also need to change the path you
 > wrote in the `use flake` command.

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

@@ -108,7 +108,7 @@ true≢false2 p = transport bool-map2 p refl
 
 ## Note on proving divergence on equivalent values
 
-> [!admonition: NOTE]
+> [!NOTE]
 > Update: some of these have been commented out since regular Agda doesn't support higher inductive types
 
 Let's make sure this isn't broken by trying to apply this to something that's

src/content/posts/2023-08-31-thoughts-on-organization/index.md

@@ -29,7 +29,7 @@ my personal schedule, yet they only see a small slice of your life. The only
 things calendars can see automatically with no intervention on my part are
 emails that are sent from airlines.
 
-> [!admonition: NOTE]
+> [!NOTE]
 > I'm sure Google or Apple could probably ritz up their services to scan text
 > and guess events to put on your calendar, but that's missing the point. The vast
 > majority of people I associate with rarely coordinate events over email in the
@@ -118,7 +118,7 @@ data using various visualizations for this purpose.
 
 [2]: https://git.mzhang.io/michael/logseq-calendar
 
-> [!admonition: NOTE]
+> [!NOTE]
 > As an aside, this isn't sponsored in any way. While this post makes me sound
 > like just a Logseq shill, it's actually quite the opposite: they're an
 > open-source project solely funded by donations. I've been donating to them

src/content/posts/2023-09-01-formal-cek-machine-in-agda/index.md

@@ -142,7 +142,7 @@ That's quite a mouthful. If you tried calling $Y$ on some term, you will find
 that evaluation will quickly expand infinitely. That makes sense given its
 purpose: to find a _fixed point_ of whatever function you pass in.
 
-> [!admonition: NOTE]
+> [!NOTE]
 > As an example, the fixed-point of the function $f(x) = \sqrt{x}$ is $1$.
 > That's because $f(1) = 1$, and applying $f$ to any other number sort of
 > converges in on this value. If you took any number and applied $f$ infinitely
@@ -221,7 +221,7 @@ much. But as a result of this tiny change, _every_ term now has a type:
 - $λ(x:\mathbb{N}).2x :: \mathbb{N} \rightarrow \mathbb{N}$
 - $isEven(3) :: (\mathbb{N} \rightarrow \mathrm{Bool}) · \mathbb{N} = \mathrm{Bool}$
 
-> [!admonition: NOTE]
+> [!NOTE]
 > Some notation:
 >
 > - $x :: T$ means $x$ has type $T$, and

src/content/posts/2023-09-15-equality.md

@@ -16,7 +16,7 @@ to, since they're very different concepts.
   to be the same, so anytime you see $x$, you can replace it with $y$ and vice
   versa."
 
-  > [!admonition: NOTE]
+  > [!NOTE]
   > Technically speaking, definitional and judgmental are two separate concepts
   > but coincide in many type theories. You could think of multiple levels of
   > equalities like this:

src/content/posts/2023-10-10-dtt-project.md

@@ -70,7 +70,7 @@ data Type where
 
 Monotypes (usually denoted $\tau$) are types that aren't universally quantified.
 
-> [!admonition: NOTE]
+> [!NOTE]
 > In the declarative version of this algorithm, monotypes don't have existential quantifiers either,
 > but the algorithmic type system includes it.
 > TODO: Explain why

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

@@ -22,7 +22,7 @@ data _≡_ {l} {A : Set l} : (a b : A) → Set l where
 
 </details>
 
-> [!admonition: NOTE]
+> [!NOTE]
 > This content is a writeup from a weekend discussion session for the fall 2023 special-topics course CSCI 8980 at the University of Minnesota taught by [Favonia], who provided the examples.
 > This post is primarily a summary of the concepts discussed.
 

src/content/posts/2024-05-02-ddr/index.mdx

@@ -130,7 +130,7 @@ With this knowledge, when you see a 200 BPM song, you can divide $300 / 200 = 1.
 
 Some tools like [3icecream] have a BPM calculator for charts if you enter in your reading speed, but often using your phone's calculator or just memorizing some common benchmark BPMs will do just fine.
 
-> [!admonition: NOTE]
+> [!NOTE]
 > Since every song you play might be a different BPM, always check to make sure the scroll speed is what you want!
 
 If a song's BPM is variable, it will show a range instead.

src/content/posts/2024-06-21-coping-with-refactoring/index.md

@@ -55,7 +55,7 @@ boat load of files to hide your potential complexity into, consider whether the
 cost of adding that abstraction is worth the pain it will take to change it
 later.
 
-> [!admonition: NOTE]
+> [!NOTE]
 > As a bonus, if your language has a good enough type system, you probably don't
 > need the strategy pattern at all. Just create a function signature and pass
 functions as values!

src/content/posts/2024-06-28-boolean-equivalences.lagda.md

@@ -15,16 +15,16 @@ $$
   (2 \simeq 2) \simeq 2
 $$
 
-> [!admonition: WARNING]
+> [!NOTE]
-> :warning: This post describes exercise 2.13 of the [Homotopy Type Theory
+> This problem is exercise 2.13 of the [Homotopy Type Theory book][book]. If you
-> book][book]. If you are planning to attempt this problem yourself, spoilers
+> are planning to attempt this problem, spoilers ahead!
-> ahead!
 
 [book]: https://homotopytypetheory.org/book/
 
 <small>The following line imports some of the definitions used in this post.</small>
 
 ```
+{-# OPTIONS --allow-unsolved-metas #-}
 open import Prelude
 open Σ
 ```
@@ -220,7 +220,7 @@ g∘f false = refl
 
 Now comes the complicated case: proving $f \circ g \sim \textrm{id}$.
 
-> [!admonition: NOTE]
+> [!NOTE]
 > Since Agda's comment syntax is `--`, the horizontal lines in the code below
 > are simply a visual way of separating out our proof premises from our proof
 > goals.
@@ -412,6 +412,6 @@ main-theorem = g , mkEquiv f g∘f f∘g
 
 Now that Agda's all happy, our work here is done!
 
-Going through all this taught me a lot about how the basics of equivalences work
+Going through all this taught me a lot about how the basics of equivalences and
-and how to express a lot of different ideas into the type system. Thanks for
+how to express a lot of different ideas into the type system. Thanks for
 reading!

src/styles/_colors.scss

@@ -22,8 +22,6 @@
     // Admonition
     --note-color: #{$linkColor};
     --note-background-color: var(--link-hover-color);
-    --warning-color: rgb(208, 126, 25);
-    --warning-bg-color: rgb(255, 250, 202);
 
     // Syntax Highlighting
     --astro-code-color-text: #24292e;
@@ -64,8 +62,6 @@
     // Admonition
     --note-color: #{$linkColor};
     --note-background-color: var(--link-hover-color);
-    --warning-color: rgb(211, 185, 107);
-    --warning-bg-color: rgb(121, 81, 21);
 
     // Syntax Highlighting
     --astro-code-color-text: #e1e4e8;

src/styles/post.scss

@@ -245,10 +245,10 @@ hr.endline {
 }
 
 .admonition {
+  // TODO: Figure out how to distinguish admonitions
   --admonition-color: var(--note-color);
-  --admonition-bg-color: var(--note-background-color);
 
-  background-color: var(--admonition-bg-color);
+  background-color: var(--note-background-color);
   border-left: 4px solid var(--admonition-color);
   padding: 8px;
   font-size: 0.9rem;
@@ -269,9 +269,4 @@ hr.endline {
   :last-child {
     margin-bottom: 0;
   }
-
-  &.WARNING {
-    --admonition-color: var(--warning-color);
-    --admonition-bg-color: var(--warning-bg-color);
-  }
 }