Skip to content

Mathlib3 Synchronisation

Jump to bottom
Eric Wieser edited this page May 19, 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 "out-of-sync" page on 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). If possible, try not to port multiple mathlib3 PRs in the same forward-port PR, as this can make review harder. 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 either. Fix this by adding the label.
    • Placeholder PRs are not necessary anymore, but some still exist. Empty placeholder PRs that do not modify the file in question don't show up 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 page by clicking on its 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! Usually, porting just the oldest change is sensible.

  7. The middle column shows you the Mathport output which you can use for porting. If you hover over your change in the mathlib3 column, it will highlight possibly-corresponding commits in this column. Generally, the oldest of these commits will be the one you want (the other will just be noise caused by mathlib4 changes). Mathport output regenerates around 02:00UTC every day; so if you don't see your change, try again tomorrow. See the Porting Wiki for general porting instructions and make changes in mathlib4 to match the mathlib3 content.

  8. Make sure the changes you ported include updating the SHA at the top of the file. This should have been in the mathport diff that you copied from.

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

Reviewing forward-port PRs

  1. Choose a forward-port PR to review

    • Visit the out-of-sync page, and look at the PR numbers in the right column.
    • Check that the PR you clicked on doesn't depend on any other PRs; if so, those should be reviewed first

  2. Visit the diff page for the PR:

    • If everything has gone well with the bot, each forward-ported file will have added comments that say things like image Unfortunately, these are not clickable; you will have to copy out the URL manually. The one above leads here.
    • If the bot is having a tantrum (or there are more than 10 files being forward-ported), click "Detect changes to header SHAs", then "Add annotations", then "run the script". This will show output like 
      Notice: See https://leanprover-community.github.io/mathlib-port-status/file/topology/sets/compacts?range=dc6c365e751e34d100e80fe6e314c3c3e0fd2988..8c1b484d6a214e059531e22f1be9898ed6c1fd47
      These links are clickable!
    • The author may have posted links for you in the description. These links may be incorrect! If you click them, you should verify that the commits they link to match the SHA in the files in the diff.

  3. Check that every file in the PR comes with such a link; if the link is missing, it means the author either forgot to update the SHA, or that the SHA was somehow correct (which should be explained in the PR description)

  4. Click each link in turn.

    • The page you arrive at will show the original mathlib3 change highlighted in red, and the version being synced to highlighted in green. Your job is to check that everything between the red change (exclusive) and the green change (inclusive) has been ported!
    • To do this, you look for the corresponding entry in the "mathlib3port" column in the center, and verify that the author hasn't missed any hunks.

    image

  5. After reviewing that the author has faithfully ported the automatic changes, check that any ported comments and declarations have been adjusted to match mathlib4 naming conventions.

  6. Approve the PR!

Clone this wiki locally