diff --git a/.envrc b/.envrc
index 46262c0..dc7feeb 100644
--- a/.envrc
+++ b/.envrc
@@ -1,2 +1,2 @@
 layout python3
-use flake
+# use flake
diff --git a/flake.nix b/flake.nix
index 50b8d84..c3e381f 100644
--- a/flake.nix
+++ b/flake.nix
@@ -1,7 +1,12 @@
 {
   outputs = { self, nixpkgs, flake-utils }: flake-utils.lib.eachDefaultSystem (system:
-  let pkgs = import nixpkgs { inherit system; };
+  let
+    pkgs = import nixpkgs { inherit system; };
+    flakePkgs = rec {
+      gerby = pkgs.callPackage ./nix/gerby.nix {};
+    };
   in {
+    packages = flake-utils.lib.flattenTree flakePkgs;
     devShell = pkgs.mkShell {};
   });
 }
diff --git a/thesis/.gitignore b/thesis/.gitignore
new file mode 100644
index 0000000..e35d885
--- /dev/null
+++ b/thesis/.gitignore
@@ -0,0 +1 @@
+_build
diff --git a/thesis/Justfile b/thesis/Justfile
new file mode 100644
index 0000000..bae19e6
--- /dev/null
+++ b/thesis/Justfile
@@ -0,0 +1,49 @@
+set export
+builddir := `pwd` / "_build"
+
+all: gerby_db
+
+serve: gerby_db
+  #!/usr/bin/env bash
+  cd $builddir/gerby-website/gerby
+  cp tools/*.sqlite .
+  flask --app . run --host 0.0.0.0
+
+pdf: book_tex
+  tectonic $builddir/book.tex
+
+gerby_src:
+  #!/usr/bin/env bash
+  mkdir -p $builddir
+  if [ ! -d "$builddir/gerby-website" ]; then
+    git clone https://github.com/gerby-project/gerby-website $builddir/gerby-website
+  fi
+
+gerby_db: plastex_files gerby_src
+  #!/usr/bin/env bash
+  cd $builddir/gerby-website/gerby/tools
+  rm -rf stacks stacks.paux stacks.tags
+  cp -r $builddir/web/book stacks
+  cp $builddir/web/book.paux stacks.paux
+  cp $builddir/web/tags stacks.tags
+  python3 update.py
+
+plastex_files: book_tex tags bib
+  #!/usr/bin/env bash
+  mkdir -p $builddir/web
+  cd $builddir/web
+  rm -r book
+  cp tags $builddir/web/tags
+  cp $builddir/my.bib $builddir/web/my.bib
+  plastex --renderer=Gerby $builddir/book.tex
+
+tags:
+  mkdir -p $builddir
+  python3 scripts/update_tags.py tags
+
+bib:
+  touch $builddir/my.bib
+
+book_tex:
+  mkdir -p $builddir
+  python3 scripts/build_book.py > $builddir/book.tex
diff --git a/thesis/index b/thesis/index
new file mode 100644
index 0000000..0af535a
--- /dev/null
+++ b/thesis/index
@@ -0,0 +1,4 @@
+# Ordered index of modules
+
+src/intro.tex
+src/mltt.tex
diff --git a/thesis/preamble.tex b/thesis/preamble.tex
new file mode 100644
index 0000000..89274d8
--- /dev/null
+++ b/thesis/preamble.tex
@@ -0,0 +1,3 @@
+\documentclass{amsart}
+
+\usepackage{hyperref}
diff --git a/thesis/scripts/build_book.py b/thesis/scripts/build_book.py
new file mode 100644
index 0000000..0004c15
--- /dev/null
+++ b/thesis/scripts/build_book.py
@@ -0,0 +1,65 @@
+import os
+import sys
+from pathlib import Path
+
+def debug(*args, **kwargs): print(*args, file=sys.stderr, **kwargs)
+def is_label(t: str): return t.find("\\label{") >= 0
+
+with open("preamble.tex") as f:
+  for line in f.readlines():
+    line = line.strip()
+    if line.find("\\documentclass") == 0:
+      line = line.replace("amsart", "amsbook")
+      line = line.replace("stacks-project", "stacks-project-book")
+    print(line)
+
+print("""
+\\begin{document}
+
+\\begin{titlepage}
+\\pagestyle{empty}
+\\setcounter{page}{1}
+\\vskip1in
+\\noindent
+\\end{titlepage}
+""")
+
+ignored_lines = [
+  "\\input{preamble}",
+  "\\begin{document}",
+  "\\bibliography",
+  "\\end{document}",
+  "\\tableofcontents",
+  "\\input{chapters}",
+  "\\maketitle",
+]
+
+with open("index") as f:
+  files = []
+  for line in f.readlines():
+    line = line.strip()
+    if line.startswith("#"): continue
+    if line == "": continue
+    files.append(line)
+
+for fname in files:
+  file = Path(fname)
+  with open(file) as f:
+    print(f"\\part{{{file.stem}}}")
+    print(f"\\label{{{file.stem}}}")
+
+    for line in f.readlines():
+      line = line.strip()
+      if any(line.find(i) == 0 for i in ignored_lines):
+        continue
+      if is_label(line):
+        line = line.replace("\\label{", f"\\label{{{file.stem}-")
+      if line.find("\\title{") == 0:
+        line = line.replace("\\title{", "\\chapter{")
+      print(line)
+
+print("""
+\\bibliography{my}
+\\bibliographystyle{amsalpha}
+\\end{document}
+""")
diff --git a/thesis/scripts/update_tags.py b/thesis/scripts/update_tags.py
new file mode 100644
index 0000000..2a3b293
--- /dev/null
+++ b/thesis/scripts/update_tags.py
@@ -0,0 +1,82 @@
+import sys
+import click
+import pathlib
+import json
+import math
+import re
+
+letters = "0123456789ABCDEFGHJKLMNPQRSTUVWXYZ"
+label_pat = re.compile(r"\\label\{([^\}]*)\}")
+
+def tag2num(tag: str):
+  arr = [letters.find(c) for c in tag]
+  return sum(n * pow(len(letters), i) for i, n in enumerate(arr[::-1]))
+
+def num2tag(n: int):
+  largest = math.ceil(math.log(n, len(letters)))
+  coeffs = []
+  start = False
+  for i in range(largest, -1, -1):
+    p = pow(len(letters), i)
+    coeff, r = n // p, n % p
+    n = r
+    if coeff != 0:
+      start = True
+      coeffs.append(coeff)
+    elif start: coeffs.append(coeff)
+  return "".join(letters[c] for c in coeffs).zfill(4)
+
+def next_tag(nums: list[int], highest: int) -> tuple[int, int]:
+  prev = 0
+  for c in nums:
+    if c - prev > 1: return (prev + 1, highest)
+    prev = c
+  highest = min(prev, highest)
+  highest += 1
+  return (highest, highest)
+
+@click.command()
+@click.argument("filename", type=click.Path(path_type=pathlib.Path))
+def main(filename):
+  # Load existing tags
+  tag_numbers = []
+  tag_names = set()
+  try:
+    with open(filename) as f:
+      for line in f.readlines():
+        if line.startswith("#"): continue
+        tag_s, name = line.strip().split(",")
+        tag_n = tag2num(tag_s)
+        tag_numbers.append(tag_n)
+        tag_names.add(name)
+  except: pass
+
+  tag_numbers.sort()
+  highest_tag = tag_numbers[-1] if len(tag_numbers) > 0 else 0
+
+  new_tags = []
+  src_dir = pathlib.Path("src")
+  for file in src_dir.iterdir():
+    name = file.stem
+    with open(file) as f:
+      for line in f.readlines():
+        m = label_pat.match(line)
+        if m is None: continue
+        label = m.group(1)
+        full = f"{name}-{label}"
+        if full not in tag_names:
+          n, highest_tag = next_tag(tag_numbers, highest_tag)
+          tag_numbers.append(n)
+          if highest_tag != n: tag_numbers.sort()
+          new_tags.append((n, full))
+
+  # Write back to file
+  with open(filename, "a") as f:
+    for tag_n, name in new_tags:
+      tag_s = num2tag(tag_n)
+      f.write(f"{tag_s},{name}\n")
+    
+
+
+if __name__ == "__main__":
+  main()
diff --git a/thesis/src/intro.tex b/thesis/src/intro.tex
new file mode 100644
index 0000000..990e142
--- /dev/null
+++ b/thesis/src/intro.tex
@@ -0,0 +1,19 @@
+\input{preamble}
+
+\begin{document}
+
+\title{Introduction}
+
+\maketitle
+
+\phantomsection
+\label{section-phantom}
+
+\tableofcontents
+
+Hello
+
+
+
+\end{document}
+
diff --git a/thesis/src/mltt.tex b/thesis/src/mltt.tex
new file mode 100644
index 0000000..028b945
--- /dev/null
+++ b/thesis/src/mltt.tex
@@ -0,0 +1,21 @@
+\input{preamble}
+
+\begin{document}
+
+\title{Martin-Lof Type Theory}
+
+\maketitle
+
+\phantomsection
+\label{section-phantom}
+
+\tableofcontents
+
+\label{intro}
+
+
+\label{constructors-and-eliminators}
+
+
+
+\end{document}
diff --git a/thesis/tags b/thesis/tags
new file mode 100644
index 0000000..57aac1e
--- /dev/null
+++ b/thesis/tags
@@ -0,0 +1,4 @@
+0001,mltt-section-phantom
+0002,mltt-intro
+0003,mltt-constructors-and-eliminators
+0004,intro-section-phantom