# ⟨ortho|normal⟩

## Ramblings on the Coq Kernel

Back during the summer of 2019, I worked a bit on the Coq kernel. At the same time, I posted a lot of toots on Mastodon about whatever random problems I was encountering. I’ve decided to collect them here, as it might just be that some of these will be useful to me again at some point.

More …

## Bridges of Vancouver

For reasons yet fathomable, I’ve decided to cross by foot (almost) all major pedestrian-accessible bridges crossing a body of water in Greater Vancouver. These are, courtesy of this list, as labelled on the following map, and listed as follows, in alphabetical order:

More …

## Thulium Part 3: Ghost, monitoring, backups, and a summary

This is part 3 of the Thulium series. Go back to part 2 or jump back to part 1.

Exam season has ended, and so too must this story. There are a lot more things I could self-host, but I’ve come to a point where I’m comfortable with the services I’ve set up for myself, and other ideas have larger scales and likely would deserve their own posts (setting up a mail server, for instance).

More …

## Thulium Part 2: Nextcloud (formerly Syncthing) and Gitea

This is part 2 of the Thulium series. Visit part 3 or go back to part 1.

We are now in the middle of the exam season. What better time than now to set up file syncing and a personal Git host?

More …

## Thulim Part 1: SSH and Web Server

This is part 1 of the Thulium series. Go to part 2 or jump to part 3.

Exam season is coming up now, so naturally I’ve decided to spend my time setting up a home server. I’m hoping to eventually be able to replace Google Drive with a self-hosted instance of perhaps NextCloud or SyncThing, but we’ll start small first. I’ve installed Ubuntu Server 16.04.4 LTS (Xenial Xerus), which was sufficiently straightforward that I won’t elaborate on it except to say that using an LVM caused me to be unable to boot into the OS, so don’t do that.

More …

## Advent of Code 2017, Day 23

As with Day 18, today’s problem involved running a custom assembly program. However, as stated in part b, the program run with a = 1 is much too inefficient to run directly. Whereas with 18 you could simulate a machine in whichever language you choose and finish running the program in a reasonable amount of time, this problem requires deciphering what the program actually does, then optimizing it. We begin with the input (whose real values I won’t bother with hiding):

More …

## Advent of Code 2017, Day 3

My solution for star 2 can be found here, but without the four pages of diagramming I did to get there, it’s largely indecipherable, so here’s some explanation on the mental process.

More …