diff --git a/Dockerfile b/Dockerfile
index a672397d..750e2581 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -1,3 +1,9 @@
+# To upload the Docker images to Dockerhub, log into the Docker console, and then run
+#
+#   docker buildx build --push --platform linux/amd64,linux/arm64 -t aaronbembenek/formulog:vX.Y.Z .
+#
+# (with the appropriate version number substituted for X.Y.Z).
+
 FROM maven:3.8.6-openjdk-11 AS build
 WORKDIR /root/formulog/
 COPY src src
@@ -5,8 +11,8 @@ COPY pom.xml pom.xml
 RUN mvn package -DskipTests
 
 FROM ubuntu:23.04
-WORKDIR /root/formulog/
-ARG version=0.7.0-SNAPSHOT
+ARG version=0.8.0-SNAPSHOT
+WORKDIR /root/
 RUN apt-get update \
   && DEBIAN_FRONTEND=noninteractive \
   apt-get install -y \
@@ -28,13 +34,15 @@ RUN apt-get update \
   make \
   mcpp \
   python3 \
-  sqlite \
-  zlib1g-dev
-COPY --from=build /root/formulog/target/formulog-${version}-jar-with-dependencies.jar formulog.jar
-COPY examples examples
-RUN git clone https://github.com/souffle-lang/souffle.git \
+  sqlite3 \
+  zlib1g-dev \
+  # Install modified Souffle
+  && git clone --branch eager-eval https://github.com/aaronbembenek/souffle.git \
   && cd souffle \
-  && cmake -S . -B build \
-  && cmake --build build --target install -j 4 \
-  && cd .. \
-  && rm -rf souffle
+  && cmake -S . -B build -DCMAKE_BUILD_TYPE=Release -DSOUFFLE_ENABLE_TESTING=OFF \
+  && cmake --build build -j$(nproc) \
+  && cmake --build build --target install \
+  && cmake --build build --target clean
+WORKDIR /root/formulog/
+COPY --from=build /root/formulog/target/formulog-${version}-jar-with-dependencies.jar formulog.jar
+COPY examples examples
\ No newline at end of file
diff --git a/changelog.md b/changelog.md
index 020dc155..1e68dce4 100644
--- a/changelog.md
+++ b/changelog.md
@@ -2,6 +2,27 @@
 
 All notable changes to this project will be documented in this file.
 
+## [0.8.0] - 2024-10-18
+
+### Added
+
+- Support for eager evaluation in both interpreter (`--eager-eval` option) and compiler.
+- Reorganized documentation and added a lot of new material, including a tutorial.
+- Apply Google Java format with Maven.
+- Various improvements to the code generator.
+
+### Changed
+
+- Better error reporting for type arity mismatch.
+- Clean up CI.
+- Better, more consistent CLI options for interpreter and generated code.
+
+### Fixed
+
+- Lexing of arithmetic expressions without spaces.
+- Various (rare) interpreter bugs.
+- Various bugs in the C++ runtime and generated code.
+
 ## [0.7.0] - 2023-02-14
 
 ### Added
diff --git a/docs/eval_modes/compile.md b/docs/eval_modes/compile.md
index 0469839e..6ca376be 100644
--- a/docs/eval_modes/compile.md
+++ b/docs/eval_modes/compile.md
@@ -14,7 +14,7 @@ Within this directory you can use `cmake` to compile the generated code into a b
 For example, to compile and execute the `greeting.flg` program from above, you can use these steps:
 
 ```
-java -jar formulog.jar -c greeting.flg && \
+java -jar formulog.jar -c examples/greeting.flg && \
   cd codegen && \
   cmake -B build -S . && \
   cmake --build build -j && \
diff --git a/docs/eval_modes/eager.md b/docs/eval_modes/eager.md
index 3ae5e514..f5182da2 100644
--- a/docs/eval_modes/eager.md
+++ b/docs/eval_modes/eager.md
@@ -16,7 +16,7 @@ When you configure `cmake` on the generated code, you need to add `-DFLG_EAGER_E
 For example, to build a version of the greeting program that uses eager evaluation, use these commands:
 
 ```
-java -jar formulog.jar -c greeting.flg && \
+java -jar formulog.jar -c examples/greeting.flg && \
   cd codegen && \
   cmake -B build -S . -DFLG_EAGER_EVAL=On && \
   cmake --build build -j && \
diff --git a/docs/starting.md b/docs/starting.md
index 84802a60..d15ad138 100644
--- a/docs/starting.md
+++ b/docs/starting.md
@@ -19,7 +19,7 @@ There are three main ways to set up Formulog (listed in increasing order of numb
 
 ### Use the Docker image
 
-Prebuilt images are available on [Docker Hub](https://hub.docker.com/r/aaronbembenek/formulog).
+Prebuilt images are available on [Docker Hub](https://hub.docker.com/r/aaronbembenek/formulog/tags).
 If you have Docker installed, you can spin up an Ubuntu container with Formulog, our custom version of Soufflé, and some example programs by running this command (replace `X.Y.Z` with the latest version):
 
 ```bash
diff --git a/docs/tutorial/index.md b/docs/tutorial/index.md
index 785c0b9c..b62a79a0 100644
--- a/docs/tutorial/index.md
+++ b/docs/tutorial/index.md
@@ -35,7 +35,7 @@ Our typical approach when implementing an analysis in Formulog is thus to try to
 
 This is the approach we will follow in this tutorial: directly translate the formalism of JV as we encounter it, and then go back to patch our implementation as necessary.
 Concretely, we will work our way through JV Sections 3.1 and 3.2.
-For the full, final code, see [tutorial.flg](https://github.com/HarvardPL/formulog/blob/master/docs/tutorial/tutorial.flg).
+For the full, final code, see [tutorial.flg](https://github.com/HarvardPL/formulog/blob/master/examples/tutorial.flg).
 
 ## Definitions
 
diff --git a/docs/tutorial/tutorial.flg b/examples/tutorial.flg
similarity index 98%
rename from docs/tutorial/tutorial.flg
rename to examples/tutorial.flg
index fe65cd34..1a06bd08 100644
--- a/docs/tutorial/tutorial.flg
+++ b/examples/tutorial.flg
@@ -1,3 +1,10 @@
+(***
+
+This is the full code listing for the Formulog tutorial, which is available at
+<https://harvardpl.github.io/formulog/tutorial/>.
+
+***)
+
 (*******************************************************************************
 DEFINITIONS
 *******************************************************************************)
diff --git a/pom.xml b/pom.xml
index c5c4a4c0..819b5307 100644
--- a/pom.xml
+++ b/pom.xml
@@ -4,7 +4,7 @@
     <modelVersion>4.0.0</modelVersion>
     <groupId>edu.harvard.seas.pl</groupId>
     <artifactId>formulog</artifactId>
-    <version>0.7.0-SNAPSHOT</version>
+    <version>0.8.0-SNAPSHOT</version>
     <name>formulog</name>
     <properties>
         <project.build.sourceEncoding>UTF-8</project.build.sourceEncoding>
diff --git a/src/main/java/edu/harvard/seas/pl/formulog/Main.java b/src/main/java/edu/harvard/seas/pl/formulog/Main.java
index c94796b1..a04c7c70 100644
--- a/src/main/java/edu/harvard/seas/pl/formulog/Main.java
+++ b/src/main/java/edu/harvard/seas/pl/formulog/Main.java
@@ -69,7 +69,7 @@
 @Command(
     name = "formulog",
     mixinStandardHelpOptions = true,
-    version = "Formulog 0.7.0",
+    version = "Formulog 0.8.0",
     description = "Runs Formulog.")
 public final class Main implements Callable<Integer> {
 
diff --git a/src/main/java/edu/harvard/seas/pl/formulog/ast/Var.java b/src/main/java/edu/harvard/seas/pl/formulog/ast/Var.java
index 3e57f0a0..59346ec1 100644
--- a/src/main/java/edu/harvard/seas/pl/formulog/ast/Var.java
+++ b/src/main/java/edu/harvard/seas/pl/formulog/ast/Var.java
@@ -28,7 +28,7 @@
 import java.util.Set;
 import java.util.concurrent.atomic.AtomicInteger;
 
-public class Var extends AbstractTerm implements Term {
+public class Var extends AbstractTerm {
 
   static final AtomicInteger cnt = new AtomicInteger();
 
diff --git a/src/main/java/edu/harvard/seas/pl/formulog/db/SortedIndexedFactDb.java b/src/main/java/edu/harvard/seas/pl/formulog/db/SortedIndexedFactDb.java
index 31163cbc..c02ab48a 100644
--- a/src/main/java/edu/harvard/seas/pl/formulog/db/SortedIndexedFactDb.java
+++ b/src/main/java/edu/harvard/seas/pl/formulog/db/SortedIndexedFactDb.java
@@ -27,8 +27,19 @@
 import edu.harvard.seas.pl.formulog.symbols.SymbolComparator;
 import edu.harvard.seas.pl.formulog.util.Pair;
 import edu.harvard.seas.pl.formulog.util.Util;
-import java.util.*;
+import java.lang.reflect.InvocationTargetException;
+import java.util.ArrayList;
+import java.util.Arrays;
+import java.util.Collections;
+import java.util.Comparator;
+import java.util.HashMap;
+import java.util.HashSet;
+import java.util.LinkedHashMap;
+import java.util.List;
+import java.util.Map;
 import java.util.Map.Entry;
+import java.util.NavigableSet;
+import java.util.Set;
 import java.util.concurrent.ConcurrentSkipListSet;
 import java.util.concurrent.atomic.AtomicInteger;
 import java.util.stream.Collectors;
@@ -511,7 +522,12 @@ private static IndexedFactSet make(List<Integer> order) {
       if (Configuration.genComparators) {
         try {
           cmp = gen.generate(a);
-        } catch (InstantiationException | IllegalAccessException e) {
+        } catch (InstantiationException
+            | IllegalAccessException
+            | IllegalArgumentException
+            | InvocationTargetException
+            | NoSuchMethodException
+            | SecurityException e) {
           throw new AssertionError(e);
         }
       } else {
diff --git a/src/main/java/edu/harvard/seas/pl/formulog/db/TupleComparatorGenerator.java b/src/main/java/edu/harvard/seas/pl/formulog/db/TupleComparatorGenerator.java
index 9d793d08..932f521e 100644
--- a/src/main/java/edu/harvard/seas/pl/formulog/db/TupleComparatorGenerator.java
+++ b/src/main/java/edu/harvard/seas/pl/formulog/db/TupleComparatorGenerator.java
@@ -22,6 +22,7 @@
 import edu.harvard.seas.pl.formulog.ast.Term;
 import edu.harvard.seas.pl.formulog.util.IntArrayWrapper;
 import edu.harvard.seas.pl.formulog.util.Pair;
+import java.lang.reflect.InvocationTargetException;
 import java.util.Comparator;
 import java.util.Map;
 import java.util.concurrent.ConcurrentHashMap;
@@ -52,7 +53,12 @@ public class TupleComparatorGenerator extends ClassLoader {
   private Map<IntArrayWrapper, Comparator<Term[]>> memo = new ConcurrentHashMap<>();
 
   public Comparator<Term[]> generate(int[] accessPat)
-      throws InstantiationException, IllegalAccessException {
+      throws InstantiationException,
+          IllegalAccessException,
+          IllegalArgumentException,
+          InvocationTargetException,
+          NoSuchMethodException,
+          SecurityException {
     IntArrayWrapper key = new IntArrayWrapper(accessPat);
     Comparator<Term[]> cmp = memo.get(key);
     if (cmp == null) {
@@ -67,7 +73,12 @@ public Comparator<Term[]> generate(int[] accessPat)
 
   @SuppressWarnings("unchecked")
   public Comparator<Term[]> generate1(int[] accessPat)
-      throws InstantiationException, IllegalAccessException {
+      throws InstantiationException,
+          IllegalAccessException,
+          IllegalArgumentException,
+          InvocationTargetException,
+          NoSuchMethodException,
+          SecurityException {
     String className = "edu.harvard.seas.pl.formulog.db.CustomComparator" + cnt.getAndIncrement();
     ClassGen classGen =
         new ClassGen(
@@ -82,7 +93,7 @@ public Comparator<Term[]> generate1(int[] accessPat)
 
     byte[] data = classGen.getJavaClass().getBytes();
     Class<?> c = defineClass(className, data, 0, data.length);
-    return (Comparator<Term[]>) c.newInstance();
+    return (Comparator<Term[]>) c.getDeclaredConstructor().newInstance();
   }
 
   private void addCompareMethod(ClassGen cg, int[] accessPat) {
diff --git a/src/main/java/edu/harvard/seas/pl/formulog/validating/ValidRule.java b/src/main/java/edu/harvard/seas/pl/formulog/validating/ValidRule.java
index fcc711be..dd325f5a 100644
--- a/src/main/java/edu/harvard/seas/pl/formulog/validating/ValidRule.java
+++ b/src/main/java/edu/harvard/seas/pl/formulog/validating/ValidRule.java
@@ -97,23 +97,23 @@ public static void order(
     atoms.addAll(newList);
   }
 
-  private static Set<Var> checkBody(Rule<UserPredicate, ComplexLiteral> rule)
-      throws InvalidProgramException {
-    Set<Var> boundVars = new HashSet<>();
-    Map<Var, Integer> varCounts = rule.countVariables();
-    for (ComplexLiteral lit : rule) {
-      if (!Unification.canBindVars(lit, boundVars, varCounts)) {
-        throw new InvalidProgramException(
-            "Rule cannot be evaluated given the supplied order.\n"
-                + "The problematic rule is:\n"
-                + rule
-                + "\nThe problematic literal is: "
-                + lit);
-      }
-      boundVars.addAll(lit.varSet());
-    }
-    return boundVars;
-  }
+  // private static Set<Var> checkBody(Rule<UserPredicate, ComplexLiteral> rule)
+  //     throws InvalidProgramException {
+  //   Set<Var> boundVars = new HashSet<>();
+  //   Map<Var, Integer> varCounts = rule.countVariables();
+  //   for (ComplexLiteral lit : rule) {
+  //     if (!Unification.canBindVars(lit, boundVars, varCounts)) {
+  //       throw new InvalidProgramException(
+  //           "Rule cannot be evaluated given the supplied order.\n"
+  //               + "The problematic rule is:\n"
+  //               + rule
+  //               + "\nThe problematic literal is: "
+  //               + lit);
+  //     }
+  //     boundVars.addAll(lit.varSet());
+  //   }
+  //   return boundVars;
+  // }
 
   private ValidRule(UserPredicate head, List<ComplexLiteral> body) {
     super(head, body);