Brandon’s Pet Server


What lives here

This page is being served by my home server, nousowl. I plan to run the parts of my online life here that make more sense on my own hardware. This box is meant as a playground where I can learn things but also eventually host some cool things.

Services and Plans

Carnap

Carnap brands itself as a “formal logic framework for Haskell.” Many universities, including UC Davis, use it for teaching formal logic because it’s highly capable and grading is automated. The latest Docker release is currently live on nousowl here (the copyright still says 2022, but I compiled it from the source in December 2025). I currently have it closed to all new registrations, but if you’re interested in figuring out a way to try to use it, talk to me; it wouldn’t be easy but it’s possible. I use it mainly for curriculum development, as I can directly edit assignment files via SSH and view the rendered output live on the site. I also have it here as a way of learning about managing such a site, and as a way to interact more directly with the source code. I also have ideas about a remote Carnap assignment compiler, which displays assignment files much the same way Overleaf does, but without all the garb—but this would be a lot of work to build.

Isabelle/HOL

Isabelle/HOL is one of many theorem-provers, but which is attractive to me because of work that’s already been done with it in deontic logic, e.g., here. Like Carnap, it takes a bit of configuration on any machine you want to use it on (although it is definitely more straightforward), and it doesn’t work on things like iPads, phones, etc. A dedicated server for this would allow quite a bit of personal freedom on this front. The simple solution is to simply use Isabelle/HOL in the shell on the server (although it’s not very fun to use in the shell). The more complex idea is to actually serve jEdit as a web application with only a scratch buffer, which I can simply access via URL and paste my working Isabelle theories into.

Zulip

Zulip is like Slack but with LaTeX syntax support and better asynchronous threading. For example, a working group like LLEMMMa could benefit from having a dedicated chat server on a UC Davis domain: llemmma dot ucdavis dot edu slash chat. Obviously, like with Carnap, one of the main purposes of this would be to learn about hosting the server; but who knows, perhaps the server becomes a little discussion board for me and my friends.

Git hub

Yes, lowercase “h”. Why not make a single machine my everything? I could use RAID to back everything up. I imagine, though, that having such a machine would require more sophisticated hardware than I’m currently using.


System Information

Hardware

Software

Security

Status

The server currently runs a minimal configuration: site hosting behind Caddy, a configured firewall, and automatic updates. I prioritize staying current over maximizing uptime, so the machine may reboot when required for updates (typically during off-hours).