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 +