Skip to content

Mathlib3 Synchronisation

Jump to bottom
Jon Eugster edited this page Mar 29, 2023 · 10 revisions

Forward Porting mathlib3 changes

This pages describes how to forward-port changes to mathlib3 files that touch a ported file.

  1. First, the PR in mathlib3 goes through the normal review process. Wait until it is merged and the changes are present in Mathport (might need about a day).

  2. In your local mathlib4 copy, create a new branch forward-port-XXX. XXX could be the mathlib3 PR number, the file name or anything.

  3. The Port Dashboard lists all files that are out of sync. You can forward-port a single file, but often it might be necessary/desirable to forward-port multiple files at once (e.g. all files touched by the same mathlib3-PR). To do so just repeat the following steps for each file you want to port.

  4. Check the Port-Dashboard that there is no open PR for this file yet.

    • Note that in race conditions they show up delayed, check the PR-queue as well.
    • PRs where the label mathlib3-pair is missing don't show up. FIx this by adding the label.
    • Placeholder PRs are not necessary anymore, but some still exist. Empty placeholder PRs that do not modifify the file in question don't show on the Port-Dashboard. Fix this by pushing a comment -- TODO: sync to the files that will be synced later.

  5. Open the file's site by clicking on it's name, e.g. topology.basic.

  6. On the left, you see the "Changes in mathlib3". The last synced PR is marked (last sync). If there are more than one unported changed for your file, you must either port all of them or the oldest ones. You must not skip any intermediate changes!

  7. The middle column shows you the Mathport output which you can use for porting. See the Porting Wiki for general porting instructions and make changes in mathlib4 to match the mathlib3 content.

  8. Once you ported all changes, update the SHA at the top of the ported file to the one it tells you in the blue box below the mathlib3-changes. (or if you did not port all changes, the SHA up to which you did port them)

  9. Create a mathlib4-PR with the label mathlib3-pair and add the link from the blue box into the PR description. It looks something like:

    * [`topology.basic`@`88b8a77d63a702923d9bee05e9e454ebc22aa766`..`e8da5f215e815d9ed3455f0216ef52b53e05438a`](https://leanprover-community.github.io/mathlib-port-status/file/topology/basic?range=88b8a77d63a702923d9bee05e9e454ebc22aa766..e8da5f215e815d9ed3455f0216ef52b53e05438a)

  10. If you want to include other files in your PR (e.g. from the same mathlib3-PR) repeat the steps 4. - 9. for all these files.

Clone this wiki locally