Connor Baker ConnorBaker

MixOS-based Nix Remote Builder

This is an example of how one could build a MixOS-based Nix remote builder machine. This is adapted to work with qemu, with the SSH keys seeded into the machine via qemu's fw_cfg, but could be adapted to a cloud service by whatever cloud-native tooling there is to do the same sort of thing.

ssh-keygen -t ed25519 -C mixos-builder-server -N "" -f /tmp/server_ssh_key
ssh-keygen -t ed25519 -C mixos-builder-client -N "" -f /tmp/client_ssh_key
nix build .#mixosConfigurations.remote-builder.config.system.build.all
qemu-system-x86_64 -nographic -enable-kvm -smp 4 -m 4G -kernel ./result/bzImage -initrd ./result/initrd -append "quiet console=ttyS0,115200" -fw_cfg name=opt/ssh_key,file=/tmp/server_ssh_key -fw_cfg name=opt/authorized_keys_file,file=/tmp/client_ssh_key.pub -device e1000,netdev=net0 -netdev user,id=net0,hostfwd=tcp::8022-:22
nix build nixpkgs#hello -j0 --builders 'ssh-ng://nix@localhost:8022?ssh-key=/tmp/client_ssh_key x86_64-linux - 1 1 nixos-test,benchma

Notes

Setup

az account set --subscription "Azure subscription 1"
az configure --defaults group=simpleLinuxTestVMResourceGroup location=eastus
az group create --resource-group simpleLinuxTestVMResourceGroup --location eastus

Solving SAT via interaction net superpositions

I've recently been amazed, if not mind-blown, by how a very simple, "one-line" SAT solver on Interaction Nets can outperform brute-force by orders of magnitude by exploiting "superposed booleans" and optimal evaluation of λ-expressions. In this brief note, I'll provide some background for you to understand how this works, and then I'll present a simple code you can run in your own computer to observe and replicate this effect. Note this is a new observation, so I know little about how this algorithm behaves asymptotically, but I find it quite

Implementing complex numbers and FFT with just datatypes (no floats)

In this article, I'll explain why implementing numbers with just algebraic datatypes is desirable. I'll then talk about common implementations of FFT (Fast Fourier Transform) and why they hide inherent inefficiencies. I'll then show how to implement integers and complex numbers with just algebraic datatypes, in a way that is extremely simple and elegant. I'll conclude by deriving a pure functional implementation of complex FFT with just datatypes, no floats.

	{
	allowAliases = false;
	allowBroken = false;
	allowUnfree = true;
	checkMeta = true;
	cudaSupport = true;
	cudaCapabilities = [ "7.5" ];
	packageOverrides =
	pkgs:
	let

	# Clone repositories
	FROM docker.io/bitnami/git:2.39.0@sha256:8802a1053f0a75c948da43c0d04e591b500381447745f0b5f75d3cf85509626c as git_base

	# Basic git configuration
	RUN git config --global advice.detachedHead false \
	&& git config --global init.defaultBranch main

	# Install xz-utils for decompressing tarballs
	RUN --mount=type=cache,target=/var/cache/apt \
	export DEBIAN_FRONTEND=noninteractive \

	/-
	Total and partial maps

	This is inspired by [the relevant chapter in Software Foundations]. Unlike
	Software Foundations, these maps are also parameterised over a `Key`
	type, which must supply an implementation of `DecidableEq`.

	[Software Foundations]: https://softwarefoundations.cis.upenn.edu/lf-current/Maps.html
	-/
	namespace Maps

	10.3 (Panther):
	https://swscan.apple.com/scanningpoints/scanningpointX.xml

	10.4 (Tiger):
	https://swscan.apple.com/content/catalogs/index.sucatalog
	https://swscan.apple.com/content/catalogs/index-1.sucatalog

	10.5 (Leopard):
	https://swscan.apple.com/content/catalogs/others/index-leopard.merged-1.sucatalog

	nix-eval-jobs --flake .#hydraJobs.sm_89.x86_64-linux --store local --constituents \| \
	jq -cr '.constituents + [.drvPath] \| .[] \| select(.!=null) + "^*"' \| \
	nom build --keep-going --no-link --print-out-paths --stdin