[Merged by Bors] - ci: Add documentation/status page for workflows

[marcelolynch]

• Add a page with a description of each workflow, classified by trigger type and importance
• Add a workflow to push 'helpful' comments to PRs based on arbitrary criteria, use it to post a "don't forget to update the docs!" when modifying workflow files

Prepared with Codex

[github-actions]

PR summary 7c3e14e245

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 scripts/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).

[Vierkantor]

This looks broadly good to me now, thanks! If you fix the Shellcheck warnings then I'll do a final check.

[bryangingechen]

The shellcheck warning still seems to be present. (We should maybe change the action to fail on warnings too, if possible; edit: done in #35265 )

[bryangingechen]

LGTM. @Vierkantor did you still want to do a final check?

[Vierkantor]

Yes, thanks for the reminder. LGTM too!

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-CI job
• ci (staging) / Post-Build Step
• ci (staging) / Build
• ci (staging) / Lint style