so i wanted to learn some category theory.

opened up a textbook on one side, agda on the other, and started trying to formalize the concepts and proofs

but i hit a bug in how agda’s pretty printer behaves. one i couldn’t easily work around

so i decided i’ll finally start contributing to agda and try to fix it myself

started poking around, accidentally figured out a different bug that I previously thought wasn’t worth looking into

but okay, gonna keep digging into the bug that actually led me down this path.

soon i found myself wanting to take a look at how agda’s AST looks in practice in one specific case, only to find that there isn’t really a way to do that, because haskell’s Show prints way too much information, all in one line, filling the entire terminal screen with mostly irrelevant info

so i did the natural thing and started writing a pretty printer for this purpose

eventually i got annoyed that each time i compiled agda, it would spend a good 30 seconds doing some kind of build system bookkeeping

like, i measured. a build with the entire cache fresh already would take 30 fucking seconds

as 30 seconds is enough time for me to start scrolling through fedi, i decided i need to look into this

so i started poking around the surprisingly complex makefile, learning more than i ever wanted to know about make

finally found the culprit: in a maze of includes, recursive make invocations and variable expansion, various variations of stack –dest-dir would get called like. way too many times during the build. and each of those would take 750ms to initialize, print the path to the build directory and exit

sigh, okay. i guess i’ll need to optimize the makefile a bit

managed to get it down to 10s for a do-nothing build. scoured the internet looking for a feature of make that would be useful to bring it down further

didn’t find it. as far as i can tell, “expand lazily, but then cache it” is not a behavior that’s available in gnu make, despite the absolute abundance of features they added on top of what posix specifies

now, thankfully i know better than to attempt upstreaming a feature into gnu make. and anyway, in this case the good folks at stack overflow gave me a hint on what absolute crimes i could commit in that makefile to make it go faster

but while i was contemplating my plan, i wondered: why does stack take 750ms to print a path in the first place?

after execsnoop and strace didn’t give me any hints, i decided to try using the linux profiler “perf”, which i’m sure you know is a master class in UX design

(it is not)

so i open the “perf report” and see a bunch of addresses for which i don’t have debuginfo. suspiciously small addresses too, like 0x5ddc

i start to notice the feeling of despair creeping up on me, but decide to persevere for at least a little bit more

i choose the hottest sample on the report and select “Annotate 00…005ddc”

now, i want you to consider that what i saw next was enough to get me to write out this entire rant. take a moment to internalize that.

what batshit insane assembly did i see? what could possibly have been this upsetting?

“Press ‘h’ for help on key bindings”, it said. followed immediately by “erf: Segmentation fault”, that’s right, erf, without the p.

then came a backtrace. one that listed the function name for each stack frame, as well as the source code file in which it were defined.

but the line number of all these entries is fucking 0 for some reason, as if to mock me

like, it’s not like i cared at this point where exactly the segfault happened, because even i do have my limits

but the computer apparently decided to find one more place in which it could subtly signal that there’s a nugget of insanity lurking within, to really get that eye twitchin’

and all i wanted was to learn some category theory