Advent of bugs

db/posts/4.json

@@ -0,0 +1,14 @@
+{
+  "edited-at": [
+  ],
+  "hidden": false,
+  "markdown": true,
+  "posted-at": "2025-02-07T06:45:08.536663-05:00",
+  "slugs": [
+  ],
+  "source": "/home/nathan/Projects/Blog/projects/Markdown/2025/01-Jan/AdventOfBugs.md",
+  "tags": [
+    "idris",
+    "advent-of-code"
+  ]
+}

lib/Pandoc.rakumod

@@ -88,6 +88,7 @@ sub markdown-first-paragraph(IO::Path:D $file --> Str:D) is export {
                 $para ~= "\n";
             }
             when "Link" {
+                # TODO: Properly descend into links
                 $para ~= $component<c>[1][0]<c>;
             }
             default {

projects/Markdown/2025/01-Jan/AdventOfBugs.md

@@ -0,0 +1,98 @@
+# Advent of bugs
+
+Near the start of january, after bumping into some ecosystem issues and lack of
+a personal support library while working on the 2024
+[Advent of Code](https://adventofcode.com/) in Idris, I started working on a
+project to solve all of the Advent of Code problems from all the years in a
+single massive entirely literate Idris project and publish it as an mdbook. I'm
+calling it
+[Idris 2 by Extremely Contrived](https://static.stranger.systems/idris-by-contrived-example/)
+example.
+
+## The Good
+
+This has been an amazingly fun project so far. AoC problems are nice and bite
+sized, giving really good material to work with for incrementally introducing
+more and more complex concepts. I have been following a sort of "weirdness
+budget" for each day's solutions, letting myself build on the already
+established weirdness from previous days. So far I'm 13 days in, and I've
+already had excuses to introduce all sorts of fun concepts, effects, dependent
+pattern matching, indexed type families, and refinement types, just to name a
+few.
+
+Functional programming languages are a lot of fun to model puzzle problems in to
+start with, but the new design space afforded by dependent typing offers a new,
+wonderfully fun challenge of figuring out just what to show off while I'm
+solving the puzzle. There have already been a few problems that I've wound up
+spending a few days on just tweaking and refining until I was pleased with the
+balance between weirdness expenditure and showing off what I want to show off in
+a reasonably approachable way.
+
+A couple of personal favorites of mine so far have been the
+[JSON parser](https://static.stranger.systems/idris-by-contrived-example/Parser/JSON.html),
+and the
+[`Digits` views](https://static.stranger.systems/idris-by-contrived-example/Util/Eff.html).
+The JSON parser is written in a bespoke mini-library for doing effectively
+parsing that I created just for this project, and refining the library to
+optimize for readability of the parsers written in it was an absolute joy. The
+digits views allowing pattern matching on normal integers as if they were lists
+of digits was less fun to write[^1], they are amazingly fun to use.
+
+## The Bad
+
+I've had to write a lot of support code already. I can't really fault the
+language, its a pretty new language in its pre-1.0 stage, in a pretty niche
+area, dependent types are still quite scary to the majority of programmers, and
+ecosystem improvement was a major goal of the project going in. I have already
+had to write several "basic" data structures, and there's no sign the need to do
+so will let up anytime soon[^6].
+
+Honestly the most painful part has been the lack of support for Idris in
+external tooling. Essentially every syntax highlighting library has _completely
+ass_ support for Idris. I managed to eventually sneak proper semantic
+highlighting into mdbook, it even plays nice with mdbook themes, but I had to
+commit horrible, _horrible_ crimes to get this working[^2].
+
+## The Ugly
+
+This isn't exactly a complaint, after all, ecosystem improvement was a goal
+after all, but I've already run into 2 or 3 compiler bugs, a bug in the `pack`
+package manager, and a weird behavior in katla that's a _maybe_ bug.
+
+I busted the part of the compiler that automatically inserts `force` and `delay`
+calls to make interaction between lazy and strict code Just Work™:
+[idris-lang/Idris2#3461](https://github.com/idris-lang/Idris2/issues/3461). I
+had initially thought I had discovered just _one_ compiler bug, but it turns out
+I also stumbled into an unrelated issue in the termination checker![^8]
+
+I broke the [pack](https://github.com/stefan-hoeck/idris2-pack) package manager
+by, apparently, being the first person to try and upload a library to `pack-db`
+with library code in literate files, in my
+[Structures](https://git.sr.ht/~thatonelutenist/Structures) package, checking in
+a new data structure motivated by my advent project, completely breaking the
+automated docs generation:
+[stefan-hoeck/idris2-pack!319](https://github.com/stefan-hoeck/idris2-pack/pull/319).
+This one was especially wild to me, with how popular literate programs are in
+the community, I would have never expected to be the first person to try this.
+
+## Looking Forward
+
+Despite the challenges, this has been a lovely experience so far. I greatly look
+forward to pressing through to completion, whatever it may bring, and have a
+trophy case full of bugs identified/fixed and new libraries to bring to the
+ecosystem.
+
+[^1]: While perfectly understandable, it's not reasonable to expect the compiler
+    to be able to reason about primitive "machine" integers like this on its
+    own, needing to resort to so much `believe_me` on this one did make me a bit
+    sad
+
+[^6]: Well well well, if it isn't the consequences of my actions
+
+[^2]: Do not look at the `build-book` script if you value your sanity
+
+[^8]: Before anyone gets upset here, despite the name, the termination checker
+    doesn't actually solve the halting problem. It only automatically accepts a
+    subset of the language for which termination is a 'trivial' property, which
+    includes most code I've written in the language so far, but not nearly all
+    of it.

projects/Markdown/RustPosting.md

@@ -107,7 +107,6 @@ impl Point {
 
 ```
 
-
 Modules and imports
 
 ```rust