Tips on Developing Rocq

N.B. These notes date back to before the name change to Rocq.

The following is a grab bag of tips on developing Rocq itself, from writing plugins for it to modifying the trusted kernel.

Thulium: Disk Failure

On 24 December 2020, my home server Thulium went down. Usually the cause of downtime is my home’s public IP address changing, and I need to update the DDNS record with my domain name provider. This time it wasn’t; when I tried to SSH in through the domain, I reached something, but it wouldn’t let me in. I managed to SSH in through the local IP address and tried to reboot, but I got a segmentation fault, of all things. In the end, I rebooted the server manually by walking over to the other room and holding down the power button. I could then SSH in, my Docker containers were up, all was well.

On 27 December 2020, it happened all over again. This time, I could SSH in again, but everything was painfully slow. I checked htop: CPU and memory were doing fine. I checked my internet connection: that was fine too. It must be, then, a disk issue (obviously, since that’s the title of this post).

Interesting Problems at Small Values

This post is based on the observation that, in a variety of fields (e.g. logic, computics, mathematics, physics), while certain classes of problems can be parameterized by some natural number $n$, it appears that the interesting problems―not so simple as to be trivial, but not so complex as to be unsolvable, undecidable, intractable, or nonexistent―always occur at small $n$. Below is a collection of such problems, describing at which $n$ they are interesting, and how so.

Thulium: A One-Year Retrospective

A few months ago, on the 15th of April, was the one-year anniversary of ert.space and the Thulium server, still running happily in its desktop tower, now with an extra 2 GB of RAM. Even if I didn’t have the Thulium posts to remind me, I would always have the timely bill for the domain name. Over the past year, a multitude of services and Docker containers have risen and fallen, having been replaced or abandoned or, rarely, taken up a more permanent post. In 2018, I began with the following:

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.

Designing ShareVitalSigns for iOS

For usage notes, see the LNhealth wiki page on SVS for iOS. This post is cross-posted to the LNhealth wiki at Designing ShareVitalSigns for iOS.

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:

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).

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?

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.

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):

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.