From 5f9f4648b42007a1feed68f21ce1234436f36bff Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Tue, 30 Jul 2024 16:30:02 +0200
Subject: [PATCH] [CI] Add a job to check makefiles

Checking that Make.all and other Make.* remain in sync
---
 .github/workflows/basic-checks.yml | 14 ++++++++++++++
 dev/tools/check-make-sync.sh       | 20 ++++++++++++++++++++
 2 files changed, 34 insertions(+)
 create mode 100644 .github/workflows/basic-checks.yml
 create mode 100755 dev/tools/check-make-sync.sh

diff --git a/.github/workflows/basic-checks.yml b/.github/workflows/basic-checks.yml
new file mode 100644
index 0000000000..86fab21ecf
--- /dev/null
+++ b/.github/workflows/basic-checks.yml
@@ -0,0 +1,14 @@
+name: Basic checks
+on:
+  pull_request:
+  push:
+    branches:
+    - master
+jobs:
+  basic-checks:
+    runs-on: ubuntu-latest
+    steps:
+    - name: Checkout
+      uses: actions/checkout@v4
+    - name: Check consistency of files in Makefiles
+      run: dev/tools/check-make-sync.sh
diff --git a/dev/tools/check-make-sync.sh b/dev/tools/check-make-sync.sh
new file mode 100755
index 0000000000..759d06fa08
--- /dev/null
+++ b/dev/tools/check-make-sync.sh
@@ -0,0 +1,20 @@
+#!/bin/sh
+
+MAKE_FILES=$(find theories -name "Make.*")
+
+FILES_OTHERS=files_others__
+FILES_ALL=files_all__
+
+rm -f ${FILES_OTHERS} ${FILES_ALL}
+grep "[.]v" ${MAKE_FILES} | sed -e 's/.*://' | sort > ${FILES_OTHERS}
+find theories -name "*.v" | sed -e 's_theories/__' | sort > ${FILES_ALL}
+
+if $(diff -q ${FILES_OTHERS} ${FILES_ALL} > /dev/null) ; then
+  echo "Make.* match files in theories/"
+else
+  echo "Make.* and files in theories/ don't match"
+  diff ${FILES_OTHERS} ${FILES_ALL}
+  exit 1
+fi
+
+rm -f ${FILES_OTHERS} ${FILES_ALL}