ci: refactor commit_verification so it works on PRs from forks by bryangingechen · Pull Request #35113 · leanprover-community/mathlib4

bryangingechen · 2026-02-11T03:52:41Z

Currently the commit verification workflow fails when run on a PR from a fork because it tries to post a comment, but its GITHUB_TOKEN is read-only. Example failure

This PR refactors the commit verification workflow using the new leanprover-community/privilege-escalation-bridge, splitting it into two workflows where the second one (triggered by workflow_run has access to a GITHUB_TOKEN that can post comments).

We also make the workflow run the commit verification scripts from master rather than the PR branch to close a small security issue where someone could spoof verification / get the workflow to post arbitrary comments by modifying the scripts in their branch.

Prepared with codex.

.github/workflows/commit_verification.yml

github-actions · 2026-02-11T03:53:50Z

PR summary ca1d0aeba0

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

.github/workflows/commit_verification_wf_run.yml

marcelolynch · 2026-02-11T16:23:00Z

.github/workflows/commit_verification.yml

-        if: steps.check.outputs.has_special == 'true' && steps.verify.outputs.success == 'false'
-        run: |
-          echo "::error::Commit verification failed. See PR comment for details."
-          exit 1


We should still exit the job with an error in this case, no?

Well, I'm not sure if GitHub will show the downstream workflow in the PR with a red cross, or if people even look at that or only the comment (in other words: is it important to fail?)

Yeah, we can't exit this one with an error if we want the comment to be posted. (Well we could change the conditional in the workflow_run job so that it also runs if this job failed, but then we'd be mixing up other failures as well.) I think relying on the comment rather than the status of this job should be fine, although maybe a bit confusing. Happy to change if others think otherwise though!

I think relying on the comment rather than the status of this job should be fine

I definitely don't know what the customs are around this, so if this is what is going on already, ignore my comment, of course :)

This has been addressed, hasn't it? I see the exit 1 still present in the changes.

marcelolynch · 2026-02-11T16:24:27Z

.github/workflows/commit_verification_wf_run.yml

+          require_event: pull_request
+          fail_on_missing: false
+          extract: |
+            pr_number=meta.pr_number


Do you need to plumb pr_number? github.event.workflow_run.pull_requests[0].number seems to be available

I wasn't aware of that field, but upon searching it seems that it might not be available for PRs from forks? https://github.com/orgs/community/discussions/170144

Ah, okay. I think it's okay to get it from the bridge, but then maybe remove the github.event.workflow_run.pull_requests[0].number from the concurrency thingy above

.github/workflows/commit_verification.yml

marcelolynch · 2026-02-11T16:33:17Z

.github/workflows/commit_verification.yml

+      - name: Emit bridge artifact
        if: steps.check.outputs.has_special == 'true'
-        uses: peter-evans/create-or-update-comment@e8674b075228eee787fea43ef493e45ece1004c9 # v4
+        uses: leanprover-community/privilege-escalation-bridge/emit@v1


Is this only passing/parsing a JSON and some packaged payload from one workflow to the other? If so, I'd rename it to something more generic like workflow-pipe or workflow-bridge. Also a good candidate to host in a "ci-scripts" repository...

Yeah, more or less. I decided to make the name somewhat scary as a reminder that the main reason we're using this is to run workflows with more permissions so we should pay attention to security when using it.

I see! Personally I would still name it based on what it does rather than where we mean to use it -- I can think of 'communication' uses for this already beyond 'privilege escalation' (e.g., the separate-cache-job thing I was working on -- though arguably this is a sort of privilege escalation, or for example pushing some bridge-artifact that is then consumed by the 'send-to-telemetry' workflow!), it looks like a really neat little mechanism (and I'm surprised there's not a standard action for this already).

But I don't have strong feelings on this, so let's go ahead with this :) Maybe if we make a "CI utilities" repo we can migrate the action there and rename it appropriately

not completely sure, but I think this has been addressed, hasn't it?

marcelolynch · 2026-02-11T16:44:10Z

.github/workflows/commit_verification_wf_run.yml

+          source_workflow: Commit Verification
+          expected_head_sha: ${{ github.event.workflow_run.head_sha }}
+          require_event: pull_request
+          fail_on_missing: false


fail_on_missing here presumably means 'when artifact is missing'? But we should not continue if that's the case, right?

If there are no special commits, the preceding workflow will succeed but not pass on an artifact, so I don't think we should fail the step here; I tried to make it pass and then just skip everything afterwards.

Maybe we should pass an 'empty' artifact (namely only 'metadata for the bridge')? This way 'empty artifact' is always 'something weird happened', and the happy case can just be signalled with the same bridge-mechanism

marcelolynch · 2026-02-11T16:50:15Z

.github/workflows/commit_verification_wf_run.yml

+  verify:
+    name: Verify Transient and Automated Commits
+    runs-on: ubuntu-latest
+    if: ${{ github.event.workflow_run.conclusion == 'success' }}


Related to my other comment where we should fail the original one, in that case we should run still run on failure here but fail or not depending on the contents of the payload

…erification

marcelolynch · 2026-02-14T00:50:23Z

@bryangingechen I left some more comments but to your discretion, it looks pretty good to me either way

marcelolynch · 2026-02-14T00:51:13Z

.github/workflows/commit_verification.yml

+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        with:
+          ref: master
+          path: master-branch


I've been calling this tools-branch in my recent refactors, to make it very explicit that we only check it out to get scripts and stuff

@bryangingechen is this a suggestion which could be applied here easily? Seems reasonable to strive for consistency

joneugster

@bryangingechen it looks like there are still some suggestions by Marcelo to consider.

Some of them sound like you could also decide to declare them out-of-scope for this fix and leave them for a future clean-up, but I'm adding awaiting-author to give you the option to address these

joneugster · 2026-02-18T16:31:04Z

.github/workflows/commit_verification.yml

+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+        with:
+          ref: master
+          path: master-branch


@bryangingechen is this a suggestion which could be applied here easily? Seems reasonable to strive for consistency

.github/workflows/commit_verification.yml

joneugster · 2026-02-18T16:33:25Z

.github/workflows/commit_verification.yml

+      - name: Emit bridge artifact
        if: steps.check.outputs.has_special == 'true'
-        uses: peter-evans/create-or-update-comment@e8674b075228eee787fea43ef493e45ece1004c9 # v4
+        uses: leanprover-community/privilege-escalation-bridge/emit@v1


not completely sure, but I think this has been addressed, hasn't it?

joneugster · 2026-02-18T16:34:56Z

.github/workflows/commit_verification.yml

-        if: steps.check.outputs.has_special == 'true' && steps.verify.outputs.success == 'false'
-        run: |
-          echo "::error::Commit verification failed. See PR comment for details."
-          exit 1


This has been addressed, hasn't it? I see the exit 1 still present in the changes.

ci: refactor commit_verification so it works on PRs from forks

ee1e9fd

bryangingechen commented Feb 11, 2026

View reviewed changes

.github/workflows/commit_verification.yml Show resolved Hide resolved

github-actions bot added the CI Modifies the continuous integration setup or other automation label Feb 11, 2026

bryangingechen requested review from Vierkantor and joneugster February 11, 2026 11:02

bryangingechen commented Feb 11, 2026

View reviewed changes

.github/workflows/commit_verification_wf_run.yml Outdated Show resolved Hide resolved

Apply suggestion from @bryangingechen

2317cf3

marcelolynch reviewed Feb 12, 2026

View reviewed changes

bryangingechen mentioned this pull request Feb 13, 2026

chore: run lake shake --add-public --keep-implied --keep-prefix --fix #35233

Open

Merge remote-tracking branch 'upstream/master' into refactor-commit-v…

51eefbc

…erification

marcelolynch reviewed Feb 14, 2026

View reviewed changes

marcelolynch approved these changes Feb 14, 2026

View reviewed changes

joneugster reviewed Feb 18, 2026

View reviewed changes

joneugster added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 18, 2026

joneugster self-assigned this Feb 18, 2026

Comments

Conversation

bryangingechen commented Feb 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented Feb 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary ca1d0aeba0

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

marcelolynch commented Feb 14, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

joneugster left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

bryangingechen commented Feb 11, 2026 •

edited

Loading

github-actions bot commented Feb 11, 2026 •

edited

Loading