From 723dcfab106a3376bedcbf4921a8ed5ebf6c9aa5 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Tue, 30 Jun 2026 12:17:28 -0400 Subject: [PATCH 01/10] Add defunct-readme.sh --- .github/tooling/defunct-readme.sh | 14 ++++++++++++++ 1 file changed, 14 insertions(+) create mode 100644 .github/tooling/defunct-readme.sh diff --git a/.github/tooling/defunct-readme.sh b/.github/tooling/defunct-readme.sh new file mode 100644 index 0000000000..fd200e34b6 --- /dev/null +++ b/.github/tooling/defunct-readme.sh @@ -0,0 +1,14 @@ +#!/usr/bin/env bash + +# This script searches through any READMEs which have been removed from +# the current branch (via a diff with master) and scans for references +# for them in existing READMEs +# +# If a reference to a now deleted README is found, an error is raised + +echo "Searching for deleted READMEs" + +git diff --diff-filter D --name-only master | grep '^doc/README/' | while read file; do + echo "$p was deleted, scanning for references" +done + From fab38e1da0e6fe6a0a6b679760745bc9cea53871 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Tue, 30 Jun 2026 12:22:24 -0400 Subject: [PATCH 02/10] Fix variable name --- .github/tooling/defunct-readme.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/tooling/defunct-readme.sh b/.github/tooling/defunct-readme.sh index fd200e34b6..55e0215de4 100644 --- a/.github/tooling/defunct-readme.sh +++ b/.github/tooling/defunct-readme.sh @@ -9,6 +9,6 @@ echo "Searching for deleted READMEs" git diff --diff-filter D --name-only master | grep '^doc/README/' | while read file; do - echo "$p was deleted, scanning for references" + echo "$file was deleted, scanning for references" done From 69dc9affec7c8067f0bfb9884d4b652100c9f563 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Tue, 30 Jun 2026 14:40:59 -0400 Subject: [PATCH 03/10] Update defunct-readme.sh to scan for references to deleted READMEs --- .github/tooling/defunct-readme.sh | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/.github/tooling/defunct-readme.sh b/.github/tooling/defunct-readme.sh index 55e0215de4..59accc07d3 100644 --- a/.github/tooling/defunct-readme.sh +++ b/.github/tooling/defunct-readme.sh @@ -6,9 +6,22 @@ # # If a reference to a now deleted README is found, an error is raised -echo "Searching for deleted READMEs" +echo "Searching for deleted READMEs..." git diff --diff-filter D --name-only master | grep '^doc/README/' | while read file; do echo "$file was deleted, scanning for references" + + # remove 'doc/' and '.agda, replace / with . + module=${file#"doc/"} + module=${module%".agda"} + module=${module//\//.} + + # search for *any* reference to the README + # be it an import, in a comment, or wherever else + grep -r ".*$module.*" | while read ref; do + echo "ERROR: file referenced: $ref" >&2 + exit 1 + done done +exit From 8fca1ec3dacb8fbdb4ead8d6eb422e18ef7a4f4e Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Tue, 30 Jun 2026 15:08:40 -0400 Subject: [PATCH 04/10] Update defunct-readme.sh to scan for renamed files as well --- .github/tooling/defunct-readme.sh | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) diff --git a/.github/tooling/defunct-readme.sh b/.github/tooling/defunct-readme.sh index 59accc07d3..ec08ea631b 100644 --- a/.github/tooling/defunct-readme.sh +++ b/.github/tooling/defunct-readme.sh @@ -5,10 +5,12 @@ # for them in existing READMEs # # If a reference to a now deleted README is found, an error is raised +# +# Silas Hayes-Williams, 2026 echo "Searching for deleted READMEs..." -git diff --diff-filter D --name-only master | grep '^doc/README/' | while read file; do +git diff --diff-filter DR --name-status master | awk '{print $2}' | grep '^doc/README/' | while read file; do echo "$file was deleted, scanning for references" # remove 'doc/' and '.agda, replace / with . @@ -18,7 +20,14 @@ git diff --diff-filter D --name-only master | grep '^doc/README/' | while read f # search for *any* reference to the README # be it an import, in a comment, or wherever else - grep -r ".*$module.*" | while read ref; do + # ([^\.]*)?$ says the module must be followed by *not* a . and any other text, or followed + # by nothing + # + # E.g. if README.Axiom was deleted, then it would match + # "-- see README.Axiom for some notes. :-)" + # or "-- see README.Axiom" + # but not "-- see README.Axiom.Some.Sub.Mod" + grep -r -E ".*$module([^\.].*)?$" | while read ref; do echo "ERROR: file referenced: $ref" >&2 exit 1 done From 4be6d32c258275deb71669676afeda8f48afe5af Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Tue, 30 Jun 2026 15:18:29 -0400 Subject: [PATCH 05/10] Reformat comments --- .github/tooling/defunct-readme.sh | 30 +++++++++++++++++++----------- 1 file changed, 19 insertions(+), 11 deletions(-) diff --git a/.github/tooling/defunct-readme.sh b/.github/tooling/defunct-readme.sh index ec08ea631b..90ff8392cf 100644 --- a/.github/tooling/defunct-readme.sh +++ b/.github/tooling/defunct-readme.sh @@ -1,16 +1,21 @@ #!/usr/bin/env bash -# This script searches through any READMEs which have been removed from -# the current branch (via a diff with master) and scans for references +# This script searches through any READMEs which have +# been removed (or renamed) from the current branch +# (via a diff with master) and scans for references # for them in existing READMEs # -# If a reference to a now deleted README is found, an error is raised +# If a reference to a now deleted/renamed README is +# found, an error is raised (exit code 1) # # Silas Hayes-Williams, 2026 echo "Searching for deleted READMEs..." -git diff --diff-filter DR --name-status master | awk '{print $2}' | grep '^doc/README/' | while read file; do +git diff --diff-filter DR --name-status master \ + | awk '{print $2}' \ + | grep '^doc/README/' \ + | while read file; do echo "$file was deleted, scanning for references" # remove 'doc/' and '.agda, replace / with . @@ -19,14 +24,17 @@ git diff --diff-filter DR --name-status master | awk '{print $2}' | grep '^doc/R module=${module//\//.} # search for *any* reference to the README - # be it an import, in a comment, or wherever else - # ([^\.]*)?$ says the module must be followed by *not* a . and any other text, or followed - # by nothing + # be it an import, in a comment, or wherever + # else. # - # E.g. if README.Axiom was deleted, then it would match - # "-- see README.Axiom for some notes. :-)" - # or "-- see README.Axiom" - # but not "-- see README.Axiom.Some.Sub.Mod" + # ([^\.]*)?$ says the module must be followed + # by *anything but* a '.' + any other text, or + # followed by nothing at all + # + # E.g. if README.A was deleted, then it would match + # "-- see README.A for some notes. :-)" + # or "-- see README.A" + # but not "-- see README.A.Some.Sub.Module" grep -r -E ".*$module([^\.].*)?$" | while read ref; do echo "ERROR: file referenced: $ref" >&2 exit 1 From b75c7f4a4e7866b0c57c6f72d3378b8dca8bcb78 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Tue, 30 Jun 2026 15:22:00 -0400 Subject: [PATCH 06/10] Update comments --- .github/tooling/defunct-readme.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/tooling/defunct-readme.sh b/.github/tooling/defunct-readme.sh index 90ff8392cf..ab4c00223d 100644 --- a/.github/tooling/defunct-readme.sh +++ b/.github/tooling/defunct-readme.sh @@ -3,7 +3,7 @@ # This script searches through any READMEs which have # been removed (or renamed) from the current branch # (via a diff with master) and scans for references -# for them in existing READMEs +# for them in all files within the curretn working directory # # If a reference to a now deleted/renamed README is # found, an error is raised (exit code 1) From 2a9a078a452f9ed3b500ad45aabf85db2d86f744 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Tue, 30 Jun 2026 15:29:57 -0400 Subject: [PATCH 07/10] Update defunct-readme.sh to always exit with a 1 if any error occurs --- .github/tooling/defunct-readme.sh | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/.github/tooling/defunct-readme.sh b/.github/tooling/defunct-readme.sh index ab4c00223d..dee93b6cc2 100644 --- a/.github/tooling/defunct-readme.sh +++ b/.github/tooling/defunct-readme.sh @@ -39,6 +39,10 @@ git diff --diff-filter DR --name-status master \ echo "ERROR: file referenced: $ref" >&2 exit 1 done + + if [[ $? == 1 ]]; then + exit 1 + fi done exit From 706c1322b7fb182a5f7726b3747e0804df11d553 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams <58709355+silas-hw@users.noreply.github.com> Date: Thu, 2 Jul 2026 10:14:21 -0400 Subject: [PATCH 08/10] Add bash argument to exit immediately on failure Co-authored-by: G. Allais --- .github/tooling/defunct-readme.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/tooling/defunct-readme.sh b/.github/tooling/defunct-readme.sh index dee93b6cc2..7cf4e7b5d1 100644 --- a/.github/tooling/defunct-readme.sh +++ b/.github/tooling/defunct-readme.sh @@ -1,5 +1,5 @@ #!/usr/bin/env bash - +set -eu # This script searches through any READMEs which have # been removed (or renamed) from the current branch # (via a diff with master) and scans for references From 546e568e873d6b678e6b5e05166b93ee5dfa8299 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Thu, 2 Jul 2026 10:20:39 -0400 Subject: [PATCH 09/10] Add -r to read to not escape '\' --- .github/tooling/defunct-readme.sh | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/tooling/defunct-readme.sh b/.github/tooling/defunct-readme.sh index 7cf4e7b5d1..fd08d703e2 100644 --- a/.github/tooling/defunct-readme.sh +++ b/.github/tooling/defunct-readme.sh @@ -15,7 +15,7 @@ echo "Searching for deleted READMEs..." git diff --diff-filter DR --name-status master \ | awk '{print $2}' \ | grep '^doc/README/' \ - | while read file; do + | while read -r file; do echo "$file was deleted, scanning for references" # remove 'doc/' and '.agda, replace / with . @@ -35,7 +35,7 @@ git diff --diff-filter DR --name-status master \ # "-- see README.A for some notes. :-)" # or "-- see README.A" # but not "-- see README.A.Some.Sub.Module" - grep -r -E ".*$module([^\.].*)?$" | while read ref; do + grep -r -E ".*$module([^\.].*)?$" | while read -r ref; do echo "ERROR: file referenced: $ref" >&2 exit 1 done From cbd570cdb36cc6db51b3b904467b7b22e453c0c7 Mon Sep 17 00:00:00 2001 From: Silas Hayes-Williams Date: Thu, 2 Jul 2026 10:39:15 -0400 Subject: [PATCH 10/10] Update defunct-readme to take in comparison branch as an argument --- .github/tooling/defunct-readme.sh | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/.github/tooling/defunct-readme.sh b/.github/tooling/defunct-readme.sh index fd08d703e2..0f7ef2dc39 100644 --- a/.github/tooling/defunct-readme.sh +++ b/.github/tooling/defunct-readme.sh @@ -10,9 +10,17 @@ set -eu # # Silas Hayes-Williams, 2026 +if [[ "$1" =~ ^(-h|--help)$ ]]; then + printf "usage: defunct-readme [-h | --help] \n\n" + printf "Scan for all README files deleted or renamed on the +current branch (compared to ) and check for references in +remaining files. An error is thrown if any reference is found.\n" + exit +fi + echo "Searching for deleted READMEs..." -git diff --diff-filter DR --name-status master \ +git diff --diff-filter DR --name-status $1 \ | awk '{print $2}' \ | grep '^doc/README/' \ | while read -r file; do @@ -44,5 +52,3 @@ git diff --diff-filter DR --name-status master \ exit 1 fi done - -exit