Skip to content

Commit

Permalink
[CI] Add a job to check makefiles
Browse files Browse the repository at this point in the history
Checking that Make.all and other Make.* remain in sync
  • Loading branch information
proux01 committed Oct 2, 2024
1 parent b04b065 commit 5f9f464
Show file tree
Hide file tree
Showing 2 changed files with 34 additions and 0 deletions.
14 changes: 14 additions & 0 deletions .github/workflows/basic-checks.yml
Original file line number Diff line number Diff line change
@@ -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
20 changes: 20 additions & 0 deletions dev/tools/check-make-sync.sh
Original file line number Diff line number Diff line change
@@ -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}

0 comments on commit 5f9f464

Please sign in to comment.