Tools

NixOS replaces piecemeal system administration with a single declarative configuration: packages, services, and the user environment are all described in files that can be versioned, rolled back, and reproduced exactly on another machine. My dotfiles are one flake that builds three machines plus a bootable USB installer from a shared set of modules, split between modules/system/ (NixOS proper) and modules/home/ (Home Manager, for the per-user environment).

The flake also defines a handful of packages that are not in nixpkgs: wrappers for the Claude Code and OpenCode CLIs, Loogle for searching Lean's Mathlib library, and an offline text-to-speech and speech-to-text pipeline used for AI-assistant notifications and voice input. Home Manager installs the NeoVim package, while ~/.config/nvim/ stays a separate repository — the configuration described below. The repository's docs/ directory covers installation, building the USB installer, and each module included in the system.

My NeoVim configuration is as much a writing and research environment as a development one — fast and fully customizable, without the weight of an IDE. It is built on lazy.nvim, with plugins organized into six categories (editor, LSP, text, tools, UI, and AI) and Mason-managed language servers, alongside VimTeX for LaTeX, a Typst filetype plugin, Markdown and Jupyter notebook support, Lean 4 theorem proving, and Zotero citations. Every directory carries its own README, and docs/ collects the architecture overview, installation guide, and full keybinding reference.

AI assistance comes from two complementary agent systems rather than one plugin. Claude Code is the primary integration — a terminal sidebar with session persistence across restarts, git-worktree-per-session support, and a Telescope-based command and session picker. OpenCode provides an alternative terminal UI for the same agent-driven workflow. Email runs in the editor too, through Himalaya for a full in-editor client and Aerc alongside it in the terminal.

For most of NeoVim's speed and AI integration without the learning curve, Zed is an easier place to start. It is a fast, native editor written in Rust, and my pro bono configuration I made for others looking to upgrade their setup is deliberately minimal: one install script walks through the setup with accept-or-skip prompts, the extensions install themselves on first launch, and a preset theme and font mean there is almost nothing to hand-configure before you start writing.

Minimal does not mean limited. Language servers and formatters come configured for Python, R, LaTeX, Typst, Lean, and anything else you can imagine. I have included Claude Code and OpenCode with ten shared domain extensions add commands for web development, presentations, grant proposals and budgets, epidemiological studies, document conversion, and persistent memory. Two worked examples in the repository show a full run end to end. The result is a lower-friction alternative to NeoVim — quick to install, easy to learn, and as customizable as you care to make it.

Lean 4 is an interactive theorem prover: definitions, theorems, and proofs are written in a language whose compiler accepts a proof only if each step follows from what came before, with Mathlib and CSLib supplying large bodies of already-verified mathematics and computer science to build on. Z3 is an SMT solver: instead of checking a proof you have written, it takes a set of constraints — equations, inequalities, and logical conditions over arithmetic, functions, and finite structures — and searches for something satisfying all of them at once. Where a solution exists it returns a concrete witness; where none does, it reports the constraints unsatisfiable, settling that no counterexample lies anywhere in the space it searched. These are extremely flexible and powerful tools, invaluable for work in any formal discipline.

For document preparation I rely on two typesetting tools: LaTeX for its mature, decades-deep ecosystem, and Typst for its faster, single-pass compilation and modern scripting syntax. Both separate composition from formatting, both are configured in my NeoVim setup behind the same <leader>l keymap prefix, and both are installed system-wide through NixOS (see above) rather than a per-project install — a full TeX Live distribution with the texlab language server for LaTeX, and the typst compiler with the tinymist language server for Typst.

Even if you have no interest in typesetting, Zotero is worth adopting for managing bibliographic data and PDFs on its own. It is open-source reference-management software that handles the bookkeeping for you: bibliographic records, PDFs, and notes are all saved and organized automatically rather than piling up as loose files on your hard drive. Project folders can be created and dissolved freely without spawning duplicate copies of the same paper, and a single click in the browser captures both a reference and its associated PDF in one step, so your library grows passively as you read. Selected folders or files can then be turned into a bibliography compatible with most word processors.