diff --git a/.github/workflows/stale_hints.yml b/.github/workflows/stale_hints.yml new file mode 100644 index 00000000000..f7388d7001a --- /dev/null +++ b/.github/workflows/stale_hints.yml @@ -0,0 +1,19 @@ +name: Check for stale hints +on: + pull_request: + workflow_dispatch: +jobs: + check_stale_hints: + runs-on: ubuntu-latest + defaults: + run: + shell: bash + steps: + - uses: actions/checkout@v4 + - run: | + L=$(.scripts/remove_stale_hints.sh list) + if [ "$L" != "" ]; then + echo "There are stale hints:" + echo "$L" + false + fi diff --git a/.scripts/remove_stale_hints.sh b/.scripts/remove_stale_hints.sh index e8e8f20570c..720f5b34382 100755 --- a/.scripts/remove_stale_hints.sh +++ b/.scripts/remove_stale_hints.sh @@ -2,8 +2,13 @@ set -eu -declare -A files # Store all basenames in repo -declare -A hints # Store all paths of hints in repo +list=false +if [ $# -gt 0 ] && [ $1 == "list" ]; then + list=true +fi + +declare -A files # Store all basenames for non-hint files in repo (value = 1, this is just a set) +declare -A hints # Store a map from hint paths into basenames (turns out basename computation was a bottleneck) trap 'RC=$?; rm -f .filelist; exit $RC' EXIT INT @@ -11,23 +16,30 @@ trap 'RC=$?; rm -f .filelist; exit $RC' EXIT INT # the array. Using a pipe here would be better, but a pipe creates a # subshell, so changes to the variables won't have any effect in the # parent. -find . -name '.git' -prune -o \( -type f \) > .filelist +find . -name '.git' -prune -false -o \( -type f -name '*.hints' \) > .filelist while read f0; do f="$(basename "${f0}")" - files[$f]=1; - if [[ "$f0" == *.hints ]]; then - hints[$f0]=1 - fi + hints[$f0]=$f done < .filelist + +find . -name '.git' -prune -false -o \( -type f -not -name '*.hints' \) -printf '%f\n' > .filelist +while read f; do + files[$f]=1 +done < .filelist + rm -f .filelist for h0 in "${!hints[@]}"; do - h="$(basename "${h0}")" + h=${hints[$h0]} h="${h%.hints}" # Given a/b/c/Foo.Bar.fst.hints, if there is no Foo.Bar.fst # anywhere, then delete the hint file. if ! [ -v "files[$h]" ]; then - echo "DELETING HINT $h0" - rm -f "${h0}" + if $list; then + echo "$h0" + else + echo "DELETING HINT $h0" + rm -f "${h0}" + fi fi done