Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

Commit

Permalink
chore(scripts/list-attributes.sh): script to track attributes semired…
Browse files Browse the repository at this point in the history
…ucible/irreducible (#18165)

This script generates the data for #18164
  • Loading branch information
jcommelin committed Mar 29, 2023
1 parent 3e17545 commit 9512706
Showing 1 changed file with 15 additions and 0 deletions.
15 changes: 15 additions & 0 deletions scripts/list-attributes.sh
Original file line number Diff line number Diff line change
@@ -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

0 comments on commit 9512706

Please sign in to comment.