From 95127066efeffbd0ceddbda2e5cd8f755e74dd2e Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Wed, 29 Mar 2023 02:46:55 +0000
Subject: [PATCH] chore(scripts/list-attributes.sh): script to track attributes
 semireducible/irreducible (#18165)

This script generates the data for #18164
---
 scripts/list-attributes.sh | 15 +++++++++++++++
 1 file changed, 15 insertions(+)
 create mode 100755 scripts/list-attributes.sh

diff --git a/scripts/list-attributes.sh b/scripts/list-attributes.sh
new file mode 100755
index 0000000000000..eb83da538a10c
--- /dev/null
+++ b/scripts/list-attributes.sh
@@ -0,0 +1,15 @@
+#!/usr/bin/env bash
+
+# This script generates the data for mathlib#18164
+
+URL_BASE="https://github.com/leanprover-community/mathlib/blob"
+SHA=$(git rev-parse HEAD)
+
+IFS=":"
+git grep -n "local attribute \[semireducible\]\|attribute \[irreducible\]" | \
+	grep -v 'src/tactic\|src/meta\|test' | \
+	while read fn ln rest; do
+		grep --silent "SYNCHRONIZED WITH MATHLIB4" $fn || \
+			echo "$URL_BASE/$SHA/$fn#L$ln"
+	done
+