Skip to content

chore: migrate merge-conflicts workflow to GitHub App#1651

Merged
kim-em merged 1 commit intomainfrom
migrate-merge-conflicts-to-app
Feb 3, 2026
Merged

chore: migrate merge-conflicts workflow to GitHub App#1651
kim-em merged 1 commit intomainfrom
migrate-merge-conflicts-to-app

Conversation

@kim-em
Copy link
Copy Markdown
Collaborator

@kim-em kim-em commented Feb 3, 2026

This PR migrates the merge-conflicts workflow from using MERGE_CONFLICTS_TOKEN (personal access token from mathlib-merge-conflicts-bot) to the mathlib-merge-conflicts GitHub App.

This is part of the migration away from bot accounts following GitHub ToS notice (Ticket #4052373).

Before merging:

  1. Install the mathlib-merge-conflicts app on the batteries repo: https://github.com/organizations/leanprover-community/settings/apps/mathlib-merge-conflicts → Install App → batteries
  2. Add secrets to batteries at https://github.com/leanprover-community/batteries/settings/secrets/actions:
    • MATHLIB_MERGE_CONFLICTS_APP_ID = 2784000
    • MATHLIB_MERGE_CONFLICTS_PRIVATE_KEY = (same key as mathlib4)

🤖 Prepared with Claude Code

Migrate from MERGE_CONFLICTS_TOKEN (personal access token) to mathlib-merge-conflicts GitHub App.

This is part of the migration away from bot accounts following GitHub ToS notice.

🤖 Prepared with Claude Code
@github-actions github-actions bot added the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Feb 3, 2026
ghost pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request Feb 3, 2026
@ghost ghost added the builds-mathlib label Feb 3, 2026
@ghost
Copy link
Copy Markdown

ghost commented Feb 3, 2026

Mathlib CI status (docs):

@bryangingechen
Copy link
Copy Markdown

Thanks! I can confirm that the app has been installed to batteries and the secrets appear to be present. LGTM.

@kim-em kim-em added this pull request to the merge queue Feb 3, 2026
Merged via the queue into main with commit f2ae513 Feb 3, 2026
3 checks passed
@github-actions github-actions bot removed the awaiting-review This PR is ready for review; the author thinks it is ready to be merged. label Feb 3, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants