feat(scripts): add find-ci-errors.sh to diagnose widespread CI failures

[kim-em]

This PR adds a script that searches through recent failed CI workflow runs to find open PRs whose current CI contains a specific error string. Useful for diagnosing widespread CI issues affecting multiple PRs (e.g., infrastructure problems, toolchain bugs).

Usage:

# Find all PRs currently failing with a specific error
./scripts/find-ci-errors.sh "Error parsing args: cannot parse arguments"

# Find PRs and automatically add please-merge-master label to trigger rebuilds
./scripts/find-ci-errors.sh --please-merge-master "cannot parse arguments"

The --please-merge-master flag skips PRs with merge conflicts, and the label is automatically removed by CI once the build completes.

🤖 Prepared with Claude Code

[github-actions]

PR summary 402b97b2ca

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[bryangingechen]

I'm not opposed to this PR, but I also don't see myself using this script.

I think what I had in mind for the please-merge-master label was just that we'd have a policy of applying it to all open PRs whenever we made a change that would break CI globally.

By the way, I don't think it's a good idea to remove such a please-merge-master label when a build completes either: there could be situations where a build succeeds but still needs a merge of master (if it's in progress when the breaking change hits master for example) and builds can also fail to complete even after they've merged master. It might be better to store the first good commit after a breaking change somewhere and then have CI remove the label if the branch contains that commit.

If you think this will be useful, feel free to merge though!
bors d+

[bryangingechen]

Suggested change

# The label is automatically removed by CI once the build completes.

This isn't actually true (yet?) right?

[bryangingechen]

Suggested change

	except those with the `merge-conflict` label. The label is automatically removed
	by CI once the build completes.
	except those with the `merge-conflict` label.

[mathlib-bors]

✌️ kim-em can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.