diff --git a/db/posts/4.json b/db/posts/4.json new file mode 100644 index 0000000..9effd7d --- /dev/null +++ b/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" + ] +} \ No newline at end of file diff --git a/lib/Pandoc.rakumod b/lib/Pandoc.rakumod index 2b0c91f..6018021 100644 --- a/lib/Pandoc.rakumod +++ b/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[1][0]; } default { diff --git a/projects/Markdown/2025/01-Jan/AdventOfBugs.md b/projects/Markdown/2025/01-Jan/AdventOfBugs.md new file mode 100644 index 0000000..3242738 --- /dev/null +++ b/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. diff --git a/projects/Markdown/RustPosting.md b/projects/Markdown/RustPosting.md index e673f02..632d2f1 100644 --- a/projects/Markdown/RustPosting.md +++ b/projects/Markdown/RustPosting.md @@ -107,7 +107,6 @@ impl Point { ``` - Modules and imports ```rust