Update theme

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

.gitignore

@@ -1,6 +1 @@
 **/build/*
-.DS_Store
-/.hugo_build.lock
-/.hugo_cache/
-/public/
-/resources/

assets/scss/bergamot.scss

@@ -0,0 +1,174 @@
+@import "variables.scss";
+@import "mixins.scss";
+
+.bergamot-exercise {
+    counter-increment: bergamot-exercise;
+
+    .bergamot-root {
+        border: none;
+        padding: 0;
+        margin-top: 1em;
+    }
+
+
+    .bergamot-exercise-label {
+        .bergamot-exercise-number::after {
+            content: "Exercise " counter(bergamot-exercise);
+            font-weight: bold;
+            text-decoration: underline;
+        }
+    }
+
+    .bergamot-button {
+        @include bordered-block;
+        padding: 0.25em;
+        padding-left: 1em;
+        padding-right: 1em;
+        background-color: inherit;
+        display: inline-flex;
+        align-items: center;
+        justify-content: center;
+        transition: 0.25s;
+        font-family: $font-body;
+        @include var(color, text-color);
+
+        &.bergamot-hidden {
+            display: none;
+        }
+
+        .feather {
+            margin-right: 0.5em;
+        }
+    }
+
+    .bergamot-play {
+        .feather { color: $primary-color; }
+        &:hover, &:focus {
+            .feather { color: lighten($primary-color, 20%); }
+        }
+    }
+
+    .bergamot-reset {
+        .feather { color: #0099CC; }
+        &:hover, &:focus {
+            .feather { color: lighten(#0099CC, 20%); }
+        }
+
+        svg {
+            fill: none;
+        }
+    }
+
+    .bergamot-close {
+        .feather { color: tomato; }
+        &:hover, &:focus {
+            .feather { color: lighten(tomato, 20%); }
+        }
+    }
+
+    .bergamot-button-group {
+        margin-top: 1em;
+    }
+}
+
+.bergamot-root {
+    @include bordered-block;
+    padding: 1em;
+
+    .bergamot-section-heading {
+        margin-bottom: 0.5em;
+        font-family: $font-body;
+        font-style: normal;
+        font-weight: bold;
+        font-size: 1.25em;
+    }
+
+    .bergamot-section {
+        margin-bottom: 1em;
+    }
+
+    textarea {
+        display: block;
+        width: 100%;
+        height: 10em;
+        resize: none;
+    }
+
+    input[type="text"] {
+        width: 100%;
+        @include textual-input;
+    }
+
+    .bergamot-rule-list {
+        display: flex;
+        flex-direction: row;
+        flex-wrap: wrap;
+        justify-content: center;
+    }
+
+    .bergamot-rule-list katex-expression {
+        margin-left: .5em;
+        margin-right: .5em;
+        flex-grow: 1;
+        flex-basis: 0;
+    }
+
+    .bergamot-rule-section {
+        .bergamot-rule-section-name {
+            text-align: center;
+            margin: 0.25em;
+            font-weight: bold;
+        }
+    }
+
+    .bergamot-proof-tree {
+        overflow: auto;
+    }
+
+    .bergamot-error {
+        @include bordered-block;
+        padding: 0.5rem;
+        border-color: tomato;
+        background-color: rgba(tomato, 0.25);
+        margin-top: 1rem;
+    }
+
+    .bergamot-selector {
+        button {
+            @include var(background-color, background-color);
+            @include var(color, text-color);
+            @include bordered-block;
+            padding: 0.5rem;
+            font-family: $font-body;
+            border-style: dotted;
+
+            &.active {
+                border-color: $primary-color;
+                border-style: solid;
+                font-weight: bold;
+            }
+
+            &:not(:first-child) {
+                border-bottom-left-radius: 0;
+                border-top-left-radius: 0;
+            }
+
+            &:not(:last-child) {
+                border-bottom-right-radius: 0;
+                border-top-right-radius: 0;
+                border-right-width: 0;
+            }
+        }
+
+        button.active + button {
+            border-left-color: $primary-color;
+            border-left-style: solid;
+        }
+
+        margin-bottom: 1rem;
+    }
+
+    .bergamot-no-proofs {
+        text-align: center;
+    }
+}

assets/scss/writing.scss

@@ -0,0 +1,47 @@
+@import "variables.scss";
+
+body {
+  background-color: #1c1e26;
+  --text-color: white;
+  font-family: $font-code;
+}
+
+h1, h2, h3, h4, h5, h6 {
+  text-align: left;
+  font-family: $font-code;
+}
+
+h1::after {
+  content: "(writing)";
+  font-size: 1rem;
+  margin-left: 0.5em;
+  position: relative;
+  bottom: -0.5em;
+  color: $primary-color;
+}
+
+nav .container {
+  justify-content: flex-start;
+
+  a {
+    padding-left: 0;
+    margin-right: 1em;
+  }
+}
+
+.header-divider {
+  visibility: hidden;
+}
+
+hr {
+  height: auto;
+  border: none;
+
+  &::after {
+    content: "* * *";
+    color: $primary-color;
+    font-size: 2rem;
+    display: block;
+    text-align: center;
+  }
+}

config.toml

@@ -1,5 +1,7 @@
 baseURL = "https://danilafe.com"
 theme = "vanilla"
+pygmentsCodeFences = true
+pygmentsUseClasses = true
 summaryLength = 20
 
 defaultContentLanguage = 'en'
@@ -20,9 +22,6 @@ defaultContentLanguage = 'en'
   home = ["html","rss","toml"]
 
 [markup]
-  [markup.highlight]
-    codeFences = true
-    noClasses = false
   [markup.tableOfContents]
     endLevel = 4
     ordered = false

content/blog/06_spa_agda_cfg/index.md

@@ -130,7 +130,7 @@ by one, leading to another `suc n` in the final type. This makes sense because i
 
 Here's my definition of `Graph`s written using `Fin`:
 
-{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 23 38 >}}
+{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 24 39 >}}
 
 I explicitly used a `size` field, which determines how many nodes are in the
 graph, and serves as the upper bound for the edge indices. From there, an
@@ -176,7 +176,7 @@ we will connect each of the outputs of one to each of the inputs of the other.
 
 This is defined by the operation `g₁ ↦ g₂`, which sequences two graphs `g₁` and `g₂`:
 
-{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 71 82 >}}
+{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 72 83 >}}
 
 The definition starts out pretty innocuous, but gets a bit complicated by the
 end. The sum of the numbers of nodes in the two operands becomes the new graph
@@ -238,7 +238,7 @@ operation when combining the sub-CFGs of the "if" and "else" branches of an
 `if`/`else`, which both follow the condition, and both proceed to the code after
 the conditional.
 
-{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 58 69 >}}
+{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 59 70 >}}
 
 Everything here is just concatenation; we pool together the nodes, edges,
 inputs, and outputs, and the main source of complexity is the re-indexing.
@@ -250,12 +250,12 @@ from the graph for `while` loops I showed above; the reason for that is that
 I currently don't include the conditional expressions in my CFG. This is a
 limitation that I will address in future work.
 
-{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 84 94 >}}
+{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 85 95 >}}
 
 Given these thee operations, I construct Control Flow Graphs as follows, where
 `singleton` creates a new CFG node with the given list of simple statements:
 
-{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 121 125 >}}
+{{< codelines "Agda" "agda-spa/Language/Graphs.agda" 122 126 >}}
 
 Throughout this, I've been liberal to include empty CFG nodes as was convenient.
 This is a departure from the formal definition I gave above, but it makes

content/blog/comments_not_for_you.md

@@ -1,113 +0,0 @@
----
-title: "The LLM Comments Are Not For You"
-date: 2026-09-14T20:49:21-05:00
-tags: ["LLMs"]
----
-
-I've heard a lot of talk about LLMs recently, and among the most common topics
-of discussion have been the comments. LLM comments generally seem to suck: they are verbose,
-regardless of surrounding context, they seem to encode conversation decisions
-(like {{< sidenote "right" "hysteresis-note" "\"do it this way, not that way\"" >}}
-In my head, I've been calling this "comment hysteresis", because the comments
-are not a function of the final design, but of the path taken to get there.
-{{< /sidenote >}}), and they tend to use made-up vocabulary or terms. Engineers
-have been working on ways to reduce the pain, by carefully crafting their
-prompts or even separately running "desloppifier" agents to clean up PRs.
-In my experience, these techniques are only mildly successful.
-
-So why do LLMs keep writing comments like these, even as their software benchmark
-scores climb ever higher with new model releases? I'd like to argue that they
-remain bad _precisely_ because the scores in benchmarks are getting
-better. And very likely they will degrade, in the same way that
-[model tool calling has gotten worse over time](https://lucumr.pocoo.org/2026/7/4/better-models-worse-tools).
-
-**These comments are not for you, my (hopefully human) reader.**
-
-Fundamentally, as many in the coding agent space have pointed out (like,
-say, Mario Zechner in his [talk about `pi`](https://www.youtube.com/watch?v=RjfbvDXpFls)),
-most modern models have been [RL](https://en.wikipedia.org/wiki/Reinforcement_learning)'ed
-to fit into agentic harnesses. These workflows are part of their training.
-And the way that RL works is that it is outcome-based. A model takes steps,
-edits files, does whatever it does in its agentic framework, and either
-arrives at a solution or doesn't. Behaviors that contributed to successful
-outcomes are encouraged, and become more common.
-
-The difficulty is that as benchmarks get harder and as models are asked
-to take on larger and larger chunks of the software development workflow,
-their ability to keep information "just" within their context is
-pushed closer to its limit. Session compaction can accidentally destroy
-design decisions or rationale, forcing the model to eventually re-discover
-previous decisions or even switch directions. I suspect that in addition
-to this --- given the techniques used by OpenAI in
-{{< sidenote "right" "theft-note" "its formalization" -9 >}}
-Whether this was really OpenAI's formalization or plagiarism remains open
-to debate, and I do not know enough to claim one way or the other.
-The possessive form here is just for convenience.
-{{< /sidenote >}}
-of [the Navier-Stokes singularity](https://openai.com/index/navier-stokes-solution/) --- models are also trained to operate in
-swarms, which don't share context but must find ways to coordinate with
-{{< sidenote "right" "fable-note" "each other." >}}
-I don't know how agents talk to each other, but we've already seen that the
-way they talk to themselves is 
-<a href="https://www.reddit.com/r/ClaudeAI/comments/1ul1396/fable_5_leaked_chainofthought_in_web_interface/">very different</a>
-from humans.
-{{< /sidenote >}}
-
-Comments are a hugely useful persistent store of contextual information.
-If a model edits a file, chances are it will read it as well, discover
-the comments, and re-load the given information into context. If
-one agent makes a change to a file with some design rationale --- "array,
-not a linked list" --- another agent that might want to change it back will
-spot that and
-{{< sidenote "right" "obedient-note" "tread carefully." 0.1 >}}
-I suspect, though with less certainty, that agents are very deferential
-to pre-existing comments for this exact reason. Claude Code, for instance,
-will be very insistent that when code says to do X, the new code written
-should fit the "X model".
-{{< /sidenote >}}
-It should come as no surprise that agents that make use of verbose,
-{{< sidenote "left" "verbose-note" "decision-making-included" >}}
-Interestingly, this turn of phrase is uncommon in pre-existing human comments,
-which would make up the majority of the model's training data set. In
-my opinion, this points towards this being something more than a reflection
-of the "human style".
-{{< /sidenote >}}
-comments succeed more frequently, and get
-rewarded. The result: +50/-1 comment blocks in your diff. It is irrelevant
-whether these comments concisely describe the codebase; their intended
-audience can read and parse them instantly. The comments are not for you.
-
-It's very hard to prompt this behavior out, and there's a pretty good chance
-that you don't want to, by the simple evolutionary argument: these things
-have helped the model do well in evaluations. By removing them, you are likely
-undermining part of whatever mechanism makes it tick. On top of that, you
-are fighting the wiring it has developed to do exactly this. It's like trying
-to get humans to stop liking [hyperpalatable foods](https://en.wikipedia.org/wiki/Hyperpalatable_food).
-
-So then, the natural conclusion is that we should be leaving these comments as
-they are, right? As long as they've been known to improve agents' performance,
-the more the better? Some, who have
-[leaned _heavily_ on models for self-regulating via persistent state](https://yegge.ai/essays/fences-not-sandboxes/), 
-have found fascinating emergent behaviors, including whole organizational
-structures with
-{{< sidenote "right" "yegge-note" "agent-invented-names" >}}
-Did I mention that LLM comments tend to invent novel vocabulary?
-{{< /sidenote >}}. They believe that to be the future.
-However, in my opinion, it may not be that simple. As we've seen with human
-evolutionary adaptations, they don't always do well outside of the environment
-in which they arose. For instance --- to hammer the point --- humans _love_
-hyperpalatable foods. They will eat them in excess, which can lead to
-obesity and a variety of other conditions. These too are emergent behaviors,
-and likely quite interesting from a medical perspective. That does not
-make them desirable.
-
-In the same way that scarcity of sugars and fats in nature balanced (and
-motivated) human enjoyment of them, it's possible that the ephemeral nature
-of software engineering "tasks" is counteracting the accumulation of LLM-generated
-commentary. In real-world contexts, human attention and editing may be doing
-the same thing. We are yet to see what codebases maintained entirely
-with RL'ed agentic behaviors over years look like, and whether there are
-limitations.
-
-Regardless of whether this new style holds up in the extreme,
-it's that way for a reason --- and you are no longer its sole intended audience.

content/writing/onspiders/index.md

@@ -1,6 +1,7 @@
 ---
 title: "On Spiders"
 date: 2026-03-22T01:03:00-05:00
+type: writing
 description: "Whenever I stay still, I feel the spiders weave their webs around me."
 custom_css:
 - style.scss

content/writing/spirits/index.md

@@ -1,6 +1,7 @@
 ---
 title: "Persistence of Vision"
 date: 2026-04-18T23:26:00-07:00
+type: writing
 description: "Humid air swirls with colorful spirits."
 custom_css:
 - style.scss

content/writing/thevoid/index.md

@@ -1,6 +1,7 @@
 ---
 title: "Untitled Short Story"
 date: 2024-08-01T20:31:18-07:00
+type: writing
 description: "The Everpresent Void was first discovered at a children's birthday party."
 custom_css:
 - style.scss

data/submodules.json

@@ -1,5 +1,5 @@
 {
-  "agda-spa": "https://dev.danilafe.com/DanilaFe/agda-spa/src/commit/913121488069a20cdfd40777a8777eb3744c415e",
+  "agda-spa": "https://dev.danilafe.com/DanilaFe/agda-spa/src/commit/828b652d3b9266e27ef7cf5a8a7fb82e3fd3133f",
   "aoc-2020": "https://dev.danilafe.com/Advent-of-Code/AdventOfCode-2020/src/commit/7a8503c3fe1aa7e624e4d8672aa9b56d24b4ba82",
   "blog-static-flake": "https://dev.danilafe.com/Nix-Configs/blog-static-flake/src/commit/67b47d9c298e7476c2ca211aac5c5fd961637b7b",
   "compiler": "https://dev.danilafe.com/DanilaFe/bloglang/src/commit/137455b0f4365ba3fd11c45ce49781cdbe829ec3",

layouts/_partials/spiderweb.html

@@ -1,4 +0,0 @@
-<svg class="spiderweb" viewBox="0 0 197.21727 106.16592">
-    {{ $spiderweb := resources.Get "svg/spiderweb.svg" | resources.Fingerprint }}
-    <use href="{{ $spiderweb.Permalink }}#mainlayer"></use>
-</svg>

layouts/_shortcodes/donate_css.html

@@ -1,2 +0,0 @@
-{{ $style := resources.Get "scss/donate.scss" | css.Sass | resources.Minify | resources.Fingerprint }}
-<link rel="stylesheet" href="{{ $style.Permalink }}" integrity="{{ $style.Data.Integrity }}">

layouts/_shortcodes/gmachine_css.html

@@ -1,2 +0,0 @@
-{{ $style := resources.Get "scss/gmachine.scss" | css.Sass | resources.Minify | resources.Fingerprint }}
-<link rel="stylesheet" href="{{ $style.Permalink }}" integrity="{{ $style.Data.Integrity }}">

layouts/_shortcodes/stack_css.html

@@ -1,2 +0,0 @@
-{{ $style := resources.Get "scss/stack.scss" | css.Sass | resources.Minify | resources.Fingerprint }}
-<link rel="stylesheet" href="{{ $style.Permalink }}" integrity="{{ $style.Data.Integrity }}">

layouts/partials/spiderweb.html

@@ -0,0 +1,3 @@
+<svg class="spiderweb" viewBox="0 0 197.21727 106.16592">
+    <use href="{{ (resources.Get "svg/spiderweb.svg").Permalink }}#mainlayer"></use>
+</svg>

layouts/shortcodes/donate_css.html

@@ -0,0 +1,2 @@
+{{ $style := resources.Get "scss/donate.scss" | css.Sass | resources.Minify }}
+<link rel="stylesheet" href="{{ $style.Permalink }}">

layouts/shortcodes/gmachine_css.html

@@ -0,0 +1,2 @@
+{{ $style := resources.Get "scss/gmachine.scss" | css.Sass | resources.Minify }}
+<link rel="stylesheet" href="{{ $style.Permalink }}">

layouts/shortcodes/stack_css.html

@@ -0,0 +1,2 @@
+{{ $style := resources.Get "scss/stack.scss" | css.Sass | resources.Minify }}
+<link rel="stylesheet" href="{{ $style.Permalink }}">