From 4c2f3256adb95cfd6c4c9774b354f0218c614ebe Mon Sep 17 00:00:00 2001
From: Marcella Hastings <marcella@galois.com>
Date: Thu, 19 Sep 2024 17:15:50 -0400
Subject: [PATCH] ci: add a check for the cryptol book pdf

---
 .github/check_book_update.sh | 40 ++++++++++++++++++++++++++++++++++++
 .github/workflows/book.yml   | 23 +++++++++++++++++++++
 2 files changed, 63 insertions(+)
 create mode 100644 .github/check_book_update.sh
 create mode 100644 .github/workflows/book.yml

diff --git a/.github/check_book_update.sh b/.github/check_book_update.sh
new file mode 100644
index 000000000..566f74b97
--- /dev/null
+++ b/.github/check_book_update.sh
@@ -0,0 +1,40 @@
+#!/usr/bin/env bash
+#
+# Indicates whether the Programming Cryptol book PDF needs to be updated.
+#
+
+TEX_CHANGED=0
+PDF_CHANGED=0
+
+# Examine the set of changed files to see if either the book source code
+# or the book PDF were changed.
+for fname in $@ ; do
+    case $fname in
+        docs/ProgrammingCryptol/*)
+            TEX_CHANGED=1
+            TEX_FILES="$TEX_FILES$fname " ;;
+        docs/ProgrammingCryptol.pdf)
+            PDF_CHANGED=1 ;;
+    esac
+done
+
+if (($TEX_CHANGED)) && ((! $PDF_CHANGED)); then
+    echo -e "Changed files: $TEX_FILES"
+    echo "The Programming Cryptol source code changed, but the PDF was"
+    echo "not updated. Please rebuild the book to incorporate your changes"
+    echo "and copy the file to 'docs/ProgrammingCryptol.pdf'."
+    exit 1
+elif (($TEX_CHANGED)) && (($PDF_CHANGED)); then
+    echo "Thanks for updating the PDF along with your changed source code!"
+    echo "This CI job doesn't check that you incorporated all the source"
+    echo "changes into the PDF; please confirm that it's properly updated"
+    echo "before merging."
+    exit 0
+elif ((! $TEX_CHANGED)) && (($PDF_CHANGED)); then
+    echo "The Programming Cryptol PDF changed but there was no corresponding"
+    echo "change to the source code."
+    exit 1
+else
+    echo "There were no changes to the book. No action needed."
+    exit 0
+fi
diff --git a/.github/workflows/book.yml b/.github/workflows/book.yml
new file mode 100644
index 000000000..ddd28a50a
--- /dev/null
+++ b/.github/workflows/book.yml
@@ -0,0 +1,23 @@
+#
+# Checks that the PDF version of the Programming Cryptol book was updated
+# if any of its consitituent files were changed.
+#
+
+name: Programming Cryptol PDF Update
+on: [pull_request]
+
+
+jobs:
+    update_needed:
+        runs-on: ubuntu-latest
+        steps:
+          - id: checkout
+            uses: actions/checkout@v4
+            with:
+                fetch-depth: 0
+          - name: "Check if update to local PDF is needed"
+            run: |
+                changed_files=$(git diff --name-only --diff-filter ACDMRT ${{ github.event.pull_request.base.sha }} ${{ github.sha }})
+                # This will fail if any files have spaces in the names.
+                bash .github/check_book_update.sh $changed_files
+