[Merged by Bors] - ci: bump actions/checkout to v7.0.0 by marcelolynch · Pull Request #41084 · leanprover-community/mathlib4

marcelolynch · 2026-06-26T16:37:30Z

Bumps actions/checkout to v7.0.0 across all workflows.

v7 refuses to check out fork-PR code under pull_request_target / workflow_run unless allow-unsafe-pr-checkout: true is set. Five steps intentionally check out fork-PR code in those contexts. Each is already hardened, the fork code is either built inside the landrun sandbox or run with only contents: read, while trust-rooted tooling is loaded from the base-repo checkout.

File	Step	Checked-out ref	Trigger
`.github/actions/setup-build-env/action.yml`	Checkout PR branch	`inputs.pr_branch_ref`	build_fork (`pull_request_target`)
`.github/workflows/build_template.yml`	`post_steps` checkout	`inputs.pr_branch_ref`	build_fork (`pull_request_target`)
`.github/workflows/PR_summary.yml`	Checkout code	`github.event.pull_request.head.sha`	`pull_request_target`
`.github/workflows/add_label_from_diff.yaml`	Checkout branch to label	`github.event.pull_request.head.sha \|\| github.sha`	`pull_request_target`
`.github/workflows/decls-diff.yml`	Checkout new commit	`steps.meta.outputs.new-sha`	`workflow_run`

Reapplies #41055 (reverted in #41078)

#41055 opted in the three workflow-file steps but missed the two on the fork-build path setup-build-env's Checkout PR branch (used by the build and test_lint jobs) and build_template.yml's post_steps checkout.

v7 refuses to check out fork PR code under pull_request_target/workflow_run unless allow-unsafe-pr-checkout is set. Set it on the five steps that intentionally check out fork PR code in those contexts. Each is already hardened — no persisted GITHUB_TOKEN, and the fork code is either built inside the landrun sandbox or run with only `contents: read`, while the trust-rooted tooling is loaded from the base-repo checkout: - .github/actions/setup-build-env/action.yml (build + test_lint jobs; landrun-sandboxed) - .github/workflows/build_template.yml (post_steps job; contents: read only) - .github/workflows/PR_summary.yml - .github/workflows/add_label_from_diff.yaml - .github/workflows/decls-diff.yml Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

github-actions · 2026-06-26T16:38:48Z

PR summary ea114f5aa7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff (regex)

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

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

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

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean -- pending)

Computed after the build finishes.

No changes to strong technical debt.

No changes to weak technical debt.

Current commit ea114f5aa7
Reference commit 571b8a8e54

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/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/PR_summary.yml
.github/workflows/actionlint.yml
.github/workflows/add_label_from_diff.yaml
.github/workflows/build_template.yml
.github/workflows/cache_test.yml
.github/workflows/check_pr_titles.yaml
.github/workflows/commit_verification.yml
.github/workflows/daily-master-tag.yml
.github/workflows/daily.yml
.github/workflows/decls-diff.yml
.github/workflows/docker_build.yml
.github/workflows/lake_cache_shadow.yml
.github/workflows/latest_import.yml
.github/workflows/long_file_report.yml
.github/workflows/maintainer_bors_wf_run.yml
.github/workflows/maintainer_merge_wf_run.yml
.github/workflows/nightly_bump_and_merge.yml
.github/workflows/nightly_detect_failure.yml
.github/workflows/nightly_merge_master.yml
.github/workflows/nolints.yml
.github/workflows/olean_report.yaml
.github/workflows/pr_check_downstream.yml
.github/workflows/pre-commit.yml
.github/workflows/publish_tools.yml
.github/workflows/remove_deprecated_decls.yml
.github/workflows/rm_set_option.yml
.github/workflows/shake.yaml
.github/workflows/technical_debt_metrics.yml
.github/workflows/update_dependencies.yml
.github/workflows/update_dependencies_zulip.yml
.github/workflows/validate_mathlib_ci_paths.yml
.github/workflows/weekly-lints.yml
.github/workflows/zulip_emoji_ci_status.yaml
.github/workflows/zulip_emoji_closed_pr.yaml
.github/workflows/zulip_emoji_labelling.yaml
.github/workflows/zulip_emoji_merge_delegate.yaml

bryangingechen · 2026-06-26T17:44:20Z

Thanks!
bors r+

Bumps `actions/checkout` to v7.0.0 across all workflows. v7 refuses to check out fork-PR code under `pull_request_target` / `workflow_run` unless `allow-unsafe-pr-checkout: true` is set. Five steps intentionally check out fork-PR code in those contexts. Each is already hardened, the fork code is either built inside the landrun sandbox or run with only `contents: read`, while trust-rooted tooling is loaded from the base-repo checkout. | File | Step | Checked-out ref | Trigger | |---|---|---|---| | `.github/actions/setup-build-env/action.yml` | Checkout PR branch | `inputs.pr_branch_ref` | build_fork (`pull_request_target`) | | `.github/workflows/build_template.yml` | `post_steps` checkout | `inputs.pr_branch_ref` | build_fork (`pull_request_target`) | | `.github/workflows/PR_summary.yml` | Checkout code | `github.event.pull_request.head.sha` | `pull_request_target` | | `.github/workflows/add_label_from_diff.yaml` | Checkout branch to label | `github.event.pull_request.head.sha \|\| github.sha` | `pull_request_target` | | `.github/workflows/decls-diff.yml` | Checkout new commit | `steps.meta.outputs.new-sha` | `workflow_run` | Reapplies #41055 (reverted in #41078) #41055 opted in the three workflow-file steps but missed the two on the fork-build path `setup-build-env`'s `Checkout PR branch` (used by the `build` and `test_lint` jobs) and `build_template.yml`'s `post_steps` checkout.

mathlib-bors · 2026-06-26T17:57:14Z

Pull request successfully merged into master.

Build succeeded:

- actions/attest-build-provenance: v4.1.0 -> v4.1.1 - actions/setup-python: v6.2.0 -> v6.3.0 - softprops/action-gh-release: v3.0.0 -> v3.0.1 - actions/cache: v5.0.5 -> v6.1.0 (ESM migration + read-only cache handling) - zulip/github-actions-zulip/send-message: v2.0.1 -> v2.0.2 - leanprover-community/privilege-escalation-bridge: v1.2.0 -> v1.3.0 - leanprover-community/gh-problem-matcher-wrap: pin to the node24 build (clears the Node 20 deprecation warning) - kim-em/github-actions-ensure-sha-pinned-actions: pin to v5.0.0 instead of a feature branch - dcarbone/install-jq-action: v3.2.0 -> v4.0.1 (default jq -> 1.8.2; mathlib's queries are unaffected) actions/checkout was already bumped to v7.0.0 on master (leanprover-community#41084). leanprover-community/lint-style-action is bumped separately. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

- actions/attest-build-provenance: v4.1.0 -> v4.1.1 - actions/setup-python: v6.2.0 -> v6.3.0 - softprops/action-gh-release: v3.0.0 -> v3.0.1 - actions/cache: v5.0.5 -> v6.1.0 (ESM migration + read-only cache handling) - zulip/github-actions-zulip/send-message: v2.0.1 -> v2.0.2 - leanprover-community/privilege-escalation-bridge: v1.2.0 -> v1.3.0 - leanprover-community/gh-problem-matcher-wrap: pin to the node24 build (clears the Node 20 deprecation warning) - kim-em/github-actions-ensure-sha-pinned-actions: pin to v5.0.0 instead of a feature branch - dcarbone/install-jq-action: v3.2.0 -> v4.0.1 (default jq -> 1.8.2; mathlib's queries are unaffected) actions/checkout was already bumped to v7.0.0 on master (leanprover-community#41084). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

- actions/attest-build-provenance: v4.1.0 -> v4.1.1 - actions/setup-python: v6.2.0 -> v6.3.0 - softprops/action-gh-release: v3.0.0 -> v3.0.1 - actions/cache: v5.0.5 -> v6.1.0 (ESM migration + read-only-token save fix; inputs unchanged) - zulip/github-actions-zulip/send-message: v2.0.1 -> v2.0.2 - leanprover-community/privilege-escalation-bridge: v1.2.0 -> v1.3.0 - leanprover-community/gh-problem-matcher-wrap: pin to the node24 build (clears the Node 20 deprecation warning) - dcarbone/install-jq-action: v3.2.0 -> v4.0.1 (default jq -> 1.8.2; mathlib's queries are unaffected) actions/checkout was already bumped to v7.0.0 on master (leanprover-community#41084). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

github-actions Bot added the CI Modifies the continuous integration setup or other automation label Jun 26, 2026

mathlib-bors Bot added the ready-to-merge This PR has been sent to bors. label Jun 26, 2026

mathlib-bors Bot added the bors-staging This PR is currently being built by bors on the staging branch. label Jun 26, 2026

mathlib-bors Bot changed the title ~~ci: bump actions/checkout to v7.0.0~~ [Merged by Bors] - ci: bump actions/checkout to v7.0.0 Jun 26, 2026

mathlib-bors Bot closed this Jun 26, 2026

marcelolynch mentioned this pull request Jun 26, 2026

chore(ci): bump pinned GitHub Actions to latest #41089

Open

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

[Merged by Bors] - ci: bump actions/checkout to v7.0.0#41084

[Merged by Bors] - ci: bump actions/checkout to v7.0.0#41084
marcelolynch wants to merge 1 commit into
leanprover-community:masterfrom
marcelolynch:ci/checkout-v7-redo

marcelolynch commented Jun 26, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Jun 26, 2026

Declarations diff (regex)

Uh oh!

bryangingechen commented Jun 26, 2026

Uh oh!

mathlib-bors Bot commented Jun 26, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

marcelolynch commented Jun 26, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jun 26, 2026

PR summary ea114f5aa7

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean -- pending)

⚠️ Workflow documentation reminder

Uh oh!

bryangingechen commented Jun 26, 2026

Uh oh!

mathlib-bors Bot commented Jun 26, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

marcelolynch commented Jun 26, 2026 •

edited

Loading