Oct 25, 2026, 6:31 PMThis last bit of debugging would be going so much easier if I could just figure out why there is a documented module named "Libraries.Utils.Octal" which doesn't actually exist in the standard library. https://mastodon.social/@mcc/117471914682729495
Maybe I should give up and write my own int-to-octal-string function.
Oct 25, 2026, 7:34 PMSo functional programming likes linked lists, and the standard way to build a list in ML derivatives (which includes Idris) is not a ".append" like in C, JS, Rust but newelement::list, i.e., a prepend operation. This means functional programming involves a lot of generating a list then reversing it.
Anyway, what I've figured out is my automated solution search, now that it's finished, *actually* finds solutions which print *the target output, but backward*.
Sigh.
Oct 25, 2026, 11:38 PMOkay. Yes. Straightfoward. I intentionally left my output reversed because I needed to compare it to the target string rightmost-value-first, but then I forgot to reverse the target string. Pretty quick to find.
This project is officially a
FAILURE
Because it took 12 days instead of the planned 7. If I'd finished it yesterday I'd have complained "that's 7 days, it's just dealing with PHP and '4' left me unable to work on it tuesday through friday" but it still took me two days once I resumed.
Oct 25, 2026, 11:48 PMThere turned out to be exactly 16 different integers that were correct solutions to my problem, and then one I found by hand was not the lowest. It appears I made a mistake on digit 3.
I am now at 11/25 puzzles completed, 9/11 completed in the time limit. I think I am going to put this project down for a while, this one puzzle was brutal. Especially the second half.
Pity, because my next two languages were Zig and MIR ( https://github.com/rust-lang/rustc_public/ ) and I was legit really excited about those.
Oct 26, 2026, 12:00 AMHere's my solution code for "part 2", but of course it's confusing unless you've read the "spoilers" blocks above and know what part 2 is even meant to be doing.
You may find line 276 interesting.
Oct 26, 2026, 12:00 AMIt is my hope this is not the last time I use Idris. I feel I'm closer to Actually Getting the functor/applicative/monad distinction than ever before, and Idris is a good place to explore it, better than Haskell. However, as it is I think I'm only writing small "learning FP" programs in this language, as writing moment-to-moment practical code is just too metal-on-metal grinding painful.
Oct 26, 2026, 12:03 AMThe design of Idris is smart. The package ecosystem is good. This could be a good, useful language. But the base documentation and the error messages are just too lacking. The former is fixable (especially if the devs/community leaned less heavily on "make it work like Haskell, then assume everyone already knows Haskell") but the latter is more of an open question. In general, making a language with good compiler diagnostics is a harder problem than the rest of "making a language" combined.
@mcc "A.I." slop or good old fashioned crappy documentation?
Oct 25, 2026, 7:29 PM@fiend_unpleasant It is an auto-generated documentation database in the style of doxygen, I believe based on inline doc comments.
@mcc sometimes SNOC lists are built in
Oct 25, 2026, 7:42 PM@pkhuong https://idris2docs.sinyax.net/data/base/docs/Data.List.html#Data.List.snoc
…hm. Well, next time I write something in Idris I'll consider that
Oct 25, 2026, 7:43 PM@pkhuong Is SNOC an immutable data type? I'd not heard of it
@mcc it's a cons list, but in reverse order (…)
Oct 25, 2026, 8:22 PM@pkhuong so, that implies every forward traversal is hiding a list?
Oct 25, 2026, 7:43 PMOct 25, 2026, 7:47 PM@mcc Andi
I think you're allowed to take sick leave from your AoC challenge run
Oct 25, 2026, 11:40 PM@ratsnakegames No, but that's the problem. Before Tuesday I wasn't sick.
@mcc I’ve always wanted to figure out the crazy functional stuff; it’s really interesting to see you tackle it. I wonder if Elixir or Gleam is any more do-able.
Oct 26, 2026, 1:26 AM@noodlenog I would like to try Elixir or Gleam, and given their target audiences, I'm certain they're massively more approachable.
@mcc
Rust would never have gotten all this traction if they hadn't done the work from the very star to get truly useful, informative error messages at every turn.
Shows how even a very complex language becomes usable when it tells you what's going wrong and how you (probably) want to fix it.
@mcc i saw you had an error "expected foo but here's what i got: foo". that goes beyond bad and into broken, i feel.