From bbf7b4f6c8c0cad6bf6a1eee19fb2b0c766fd9e0 Mon Sep 17 00:00:00 2001 From: Nathan McCarty Date: Fri, 7 Feb 2025 06:54:36 -0500 Subject: [PATCH] oops --- projects/Markdown/2025/01-Jan/AdventOfBugs.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/projects/Markdown/2025/01-Jan/AdventOfBugs.md b/projects/Markdown/2025/01-Jan/AdventOfBugs.md index 3242738..121f50e 100644 --- a/projects/Markdown/2025/01-Jan/AdventOfBugs.md +++ b/projects/Markdown/2025/01-Jan/AdventOfBugs.md @@ -65,6 +65,10 @@ calls to make interaction between lazy and strict code Just Work™: 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 also found a convoluted hole in the case generator that I had to reach out to +the community for help minimizing (thank you +dunhamsteve!):[idris-lang/Idris2#3466](https://github.com/idris-lang/Idris2/issues/3466)[^9] + 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 @@ -96,3 +100,5 @@ ecosystem. 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. + +[^9]: It's me, I'm the user on the discord