Migration to PRs from forks

In June 2025, Mathlib switched its contribution model. Instead of requesting PRs to be made from branches on the main repository, Mathlib now follows the "standard" model on Github: PRs must be made from forked repositories. (For more information on working with PRs from forks, please see our Git Guide for Mathlib4 Contributors.)

For the open PRs that existed before this transition, there are two options:

1. If maintainers do not request changes to the PR, then it can be merged in its current state (as PR from a branch on the main repository).
2. If the PR needs changes, then it should be migrated to a PR from a fork. The script scripts/migrate_to_fork.py can assist with this process.

What the script does

The script handles existing PRs: If you have an open PR from the main repo, it can:

• Setup a personal fork of the main repo for you
• Create a new PR from your fork with the same title, description, and labels
• Collate comments from the original PR in a comment on the new PR (*)
• Close the old PR with a migration notice
• Preserves draft status: If your original PR was a draft, the new one will be too

(*): unfortunately preserving authorship is practically impossible

How to run the script

For each PR that you want to migrate:

• Checkout your PR branch
• Merge a recent version of master into your PR branch, if the script is not available at scripts/migrate_to_fork.py
• Run the interactive script, answer the questions
• Post to Zulip in #mathlib4 > Feedback on scripts/migrate_to_fork.py if you run into problems