Skip to content

ci: remove special support for ProofWidgets4 cloud releases#37286

Closed
Vtec234 wants to merge 4 commits intoleanprover-community:masterfrom
Vtec234:rm-pw4-cache
Closed

ci: remove special support for ProofWidgets4 cloud releases#37286
Vtec234 wants to merge 4 commits intoleanprover-community:masterfrom
Vtec234:rm-pw4-cache

Conversation

@Vtec234
Copy link
Copy Markdown
Contributor

@Vtec234 Vtec234 commented Mar 27, 2026

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

Branch on this repo to exercise the CI: https://github.com/leanprover-community/mathlib4/tree/rm-pw4-cache .


Open in Gitpod

@github-actions
Copy link
Copy Markdown

PR summary 34f85c5f24

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

- getProofWidgets

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

@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 27, 2026

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

@Vtec234 Vtec234 changed the title build: remove special support for ProofWidgets4 cloud releases refactor: remove special support for ProofWidgets4 cloud releases Mar 27, 2026
@bryangingechen
Copy link
Copy Markdown
Contributor

bors try

mathlib-bors bot pushed a commit that referenced this pull request Mar 27, 2026

echo "✅ ProofWidgets source URL is allowed: $proofwidgets_url"

- name: verify ProofWidgets lean-toolchain matches on versioned releases
Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hm, actually this 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).

@Vtec234 Vtec234 changed the title refactor: remove special support for ProofWidgets4 cloud releases ci: remove special support for ProofWidgets4 cloud releases Mar 27, 2026
@Vtec234
Copy link
Copy Markdown
Contributor Author

Vtec234 commented Mar 27, 2026

Superseded by #37290.

@Vtec234 Vtec234 closed this Mar 27, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants