[Merged by Bors] - ci: remove special support for ProofWidgets4 cloud releases

[Vtec234]

This PR removes special support for ProofWidgets4 cloud releases. See leanprover-community/ProofWidgets4#165.

---

CI runs:
https://github.com/leanprover-community/mathlib4/actions/runs/23669823972
https://github.com/leanprover-community/mathlib4/actions/runs/23768342866

[github-actions]

PR summary 8807830d8b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

- getProofWidgets
- has_proofwidgets_dependency(checkout_dir:
- verify_proofwidgets_toolchain(checkout_dir:

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

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

---

⚠️ Workflow documentation reminder

This PR modifies files under .github/workflows/.
Please update docs/workflows.md if the workflow inventory, triggers, or behavior changed.

Modified workflow files:

• .github/workflows/build_template.yml

[Vtec234]

This was introduced in #31723. We no longer need to pin ProofWidgets4 to a specific tagged version after this PR. Indeed, all the other dependencies are required as main. But actually using a tagged version seems like good practice. So I see two options:

• Keep require proofwidgets at a tagged version, and keep this CI check.
• Use main, remove the CI check.

Btw, it seems to duplicate functionality of verify_proofwidgets_toolchain in scripts/verify_version_tags.py. But there are no references to that script (only meant to be run locally? introduced in #32162).

[marcelolynch]

I think it's good to remove this independently of using a tagged version or not.

[Vtec234]

IIRC the 'verify ProofWidgets lean-toolchain matches on versioned releases' step is supposed to make sure that the person bumping the Lean version remembers to update the tagged ProofWidgets as well. Do we not want that check anymore?

[marcelolynch]

I don't know the details here... why are these things coupled?

[Vtec234]

Ok, so I think it was because using the wrong version would fail to fetch the cloud release, consequently triggering rebuilds. It should no longer do so, so I normalized proofwidgets to be required from main like all the other dependencies.

[marcelolynch]

A minor comment, but looks good, thanks for this!

[marcelolynch]

I think it's good to remove this independently of using a tagged version or not.

[Vtec234]

bors r+

[mathlib-bors]

🔒 Permission denied

Existing reviewers: click here to make Vtec234 a reviewer

[bryangingechen]

Thanks!
bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

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