From dea4be6ee51e35f068f56593c23a8b94abdcc2db Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Guido=20Mart=C3=ADnez?= <mtzguido@gmail.com>
Date: Wed, 8 Jan 2025 17:39:16 -0800
Subject: [PATCH] test.mk: factor out diff checking, emit github errors

---
 mk/diff.sh | 30 ++++++++++++++++++++++++++++++
 mk/test.mk |  2 +-
 2 files changed, 31 insertions(+), 1 deletion(-)
 create mode 100755 mk/diff.sh

diff --git a/mk/diff.sh b/mk/diff.sh
new file mode 100755
index 00000000000..c100506714a
--- /dev/null
+++ b/mk/diff.sh
@@ -0,0 +1,30 @@
+#!/bin/bash
+
+if [ $# -ne 2 ]; then
+  echo "usage: $0 <actual_output> <expected_output>" >&2
+  exit 1
+fi
+
+ACTUAL="$1"
+EXPECTED="$2"
+
+DIFF="diff -u --strip-trailing-cr"
+
+if $DIFF "$ACTUAL" "$EXPECTED" ; then
+  # OK
+  exit 0
+else
+  # We're gonna fail. If we're running in CI, emit a Github
+  # error message.
+  if [ -v GITHUB_ENV ]; then
+    DIFFTEXT=$($DIFF "$ACTUAL" "$EXPECTED" | sed 's/$/%0A/' | tr -d '\n')
+    ACTUAL=$(realpath "$ACTUAL")
+    ACTUAL="${ACTUAL#$FSTAR_ROOT}"
+    EXPECTED=$(realpath "$EXPECTED")
+    EXPECTED="${EXPECTED#$FSTAR_ROOT}"
+    echo "::error::Diff failed for files $ACTUAL and $EXPECTED:%0A%0A$DIFFTEXT"
+  else
+    echo "error: Diff failed for files $ACTUAL and $EXPECTED" >&2
+  fi
+  exit 1
+fi
diff --git a/mk/test.mk b/mk/test.mk
index f7862946e04..43729b3d01a 100644
--- a/mk/test.mk
+++ b/mk/test.mk
@@ -119,7 +119,7 @@ $(OUTPUT_DIR)/%.out: $(OUTPUT_DIR)/%.exe
 ### Checking expected output for any kind of file (error output, ml, etc)
 $(OUTPUT_DIR)/%.diff: $(OUTPUT_DIR)/% %.expected
 	$(call msg, "DIFF", $<)
-	diff -u --strip-trailing-cr $^
+	$(FSTAR_ROOT)/mk/diff.sh $^
 	touch $@
 
 $(OUTPUT_DIR)/%.accept: $(OUTPUT_DIR)/%