Use ghostscript to compress PDF output on RTD (#405)

Post-build compression is primarily used because it is
straightforward. It is also aware of the width of the images and as
such can be DPI-based. Even if we compressed the images before PDF
creation, we would likely still have some room for (minimal)
improvement in the rest of the PDF.

.readthedocs.yaml

@@ -11,6 +11,10 @@ build:
     python: "3.11"
   apt_packages:
     - graphviz
+    - ghostscript
+  jobs:
+    post_build:
+      - ./scripts/rtd-compress-pdf.sh
 
 formats:
   - pdf

scripts/rtd-compress-pdf.sh

@@ -0,0 +1,28 @@
+#!/usr/bin/env sh
+
+# Compresses the PDF output using ghostscript on Read the Docs.
+
+DPI=400
+PDF_DIR="$READTHEDOCS_OUTPUT/pdf"
+
+# only run if the PDF build is enabled
+# based on whether or not the PDF output directory exists
+if [ -d "$PDF_DIR" ]; then
+    # find the existing PDF
+    pdf_name=$(ls "$PDF_DIR")
+
+    # Read the Docs expects only one PDF file in the output directory
+    # see https://docs.readthedocs.io/en/stable/reference/environment-variables.html#envvar-READTHEDOCS_OUTPUT
+    # so we move the existing PDF into a temp directory.
+    temp=$(mktemp -d)
+    mv "$PDF_DIR/$pdf_name" "$temp"
+
+    # compress the existing PDF into a new PDF,
+    # placed directly in the output directory
+    gs -sDEVICE=pdfwrite \
+        -dCompatibilityLevel=1.4 \
+        -dPDFSETTINGS=/ebook \
+        -dNOPAUSE \
+        -dBATCH -dColorImageResolution="$DPI" \
+        -sOutputFile="$PDF_DIR/$pdf_name" "$temp/$pdf_name"
+fi