I like to keep even traditionally system-level dependencies isolated and pinned per-project, so I use Nix for that.

I have been playing with Agda for a while now, and it has been a joy to work with a theorem proof assistant for the first time. (I am hoping to write some more on the topic when I am more familiar with it, but for now, I’ll just recommend Wadler, Kokke, and Siek’s excellent and free book, Programming Language Foundations in Agda.)

I found it a bit of a pain to configure Agda with Nix, and I haven’t found this advice anywhere else, so I thought I’d document it so someone else searching for the same thing doesn’t struggle quite so much.

I am assuming, for the sake of this guide, that you are using Agda with Emacs, which is the only real way to use it due to its heavy editor integration.

So, follow along to set up this combination of incredibly niche tools that you almost certainly have zero interest in. 😜

I got some praise yesterday. A colleague of mine told me that I never shy away from the hard problems.

It’s hard not to have a big grin on your face when you hear something like that.

Got me thinking though… what’s hard, exactly? And so I’ve been musing. Aren’t all problems hard?

Say a customer reports a bug, and you’ve got to fix it. You can fix it. You know you can fix it. Maybe it’ll take an hour, maybe it’ll take a day, maybe a week. But you’ll narrow it down, figure out the smallest possible increment of work you can do to remedy the problem, and then you’ll do it. And as much as it pains me to say it, because I want to be able to check that box that said I did the thing… this is the easy part.

Once in a while, when we’re feeling brave, we also try to tackle the hard problem. We try to answer the questions that we usually avoid.

• Why was this bug caused in the first place?
• Did we know about it before the customer hit it, and if so, why didn’t we do anything about it?
• Was the customer upset? Did we make sure they’re happy again?
• Can we fix not just this bug, but all classes of this bug in the future?
• What are the root causes ingrained in our culture that made this bug possible?
• Can we change our culture to ensure this doesn’t happen again?

These are the hard problems. We can’t always solve them. Maybe they’re too entrenched, maybe you don’t have the power, maybe others don’t see the problem, maybe they’re too expensive to fix. Or maybe you just don’t have the energy to fight this battle. We can’t fight all of them, after all. That way lies burnout.

But every so often, we tackle a hard problem, and we make just a little bit of progress. And whether we do, or we don’t, I think the fact that we sat up, took notice, and recognised that there’s a hard problem here—that’s cause for celebration.

I had a lot planned for last year.

We’d just moved to Zürich, and were getting to know the place. I’d found the good coffee, and I was on the hunt for decent Thai food. We bought some furniture, we didn’t have ceiling lights (now resolved), we’d figured out how to buy bin bags (it was a challenge) and I missed fish and chips. I planned to work on an open-source project, buy a TV, and jump in the lake a lot. I planned on buying a snowboard, and come winter 2020–21, learning how to use it properly.

Then… well, you know what happened.

I’ve been oscillating a lot, the past year. Some months were good. I exercised regularly, kept sensible hours while working from home (and I’m very grateful I have a job where I can do that), and practiced being a reasonable human being to the people who were forced to interact with me over fucking video chat (yes, fucking video chat). I did jump in the lake once or twice, and we found some excellent paths through the local forest that we could meander through on the weekend.

And then there were other months. The lost months. The months of always-on, low-level grumpiness, where the highlight of my day was eating more cheese while the cat judged me. The months of sitting until my back hurt, then complaining my back hurt and sitting some more to “rest” it. The months where an entire week would go by without me having a meaningful conversation with anyone past, “Do you like your coffee?”

So no, I didn’t accomplish all I set out to in 2020. I didn’t snowboard. I didn’t work on my highly secret open-source project. I didn’t get swole.

Last month, I turned 32. Like any round number, it inspired reflection on the past few years. And I realised that while I didn’t achieve a bunch of arbitrary goals, I did accomplish one thing without even noticing.

Possibly for the first time in my life… I feel pretty good.

Sure, not everything is amazing, and there’s lots more to do. I still want to learn to snowboard (without falling a lot), and I still want to work on my secret project, but I know that I can and I will. I don’t have to worry about them all the time.

I have a lot going well for me in my life right now, and it’s fun to celebrate that instead of always getting stressed out about the next thing.

Say one thing for 2020: it taught me how to be content.

Recently, I had the displeasure of experiencing a few interesting situations in which traps in zsh don’t run. This isn’t the first time I’ve wasted hours or days debugging this problem, so I’m writing it down.

For those of you who may not know, a trap is a catch-all exception handler. Think of it as a finally block for your shell script.

Try this script:

#!/usr/bin/env zsh

set -e

trap 'echo "Finished."' EXIT

echo 'Started.'
false
echo 'This will not print.'

This script will exit with a failure code due to the false invocation. This is because set -e, or set -o errexit, will tell the shell to exit as soon as one command fails. (This is not the default, or your shell would keep quitting on you every time you made a typo.)

It’ll output this:

Started.
Finished.

I’ve just released version 2.1.0 of Smoke, my integration test framework for command-line applications.

The major feature: if your command-line application produces files, you can now test their contents.

The release notes explain all: