porting tool assistance

Stream: mathlib4

[Yakov Pechersky]

Yakov Pechersky said:

Load the yaml. Check that the file indicated hasn't yet been ported or claimed, according to the yaml. Git checkout branch on mathlib 4. Copy file from mathport to mathlib4 directory (possibly modifying Mathlib.lean). Git push new branch. Read the mathport repo Readme for the hash. Use the gh cli to make a PR. Add a port label. Update the wiki yaml with the PR number and mathlib3 hash.

A start at: https://github.com/leanprover-community/mathlib-tools/pull/147

[Yakov Pechersky]

The companion PR to support a yaml-style wiki page is at https://github.com/leanprover-community/mathlib-tools/pull/148

[Yakov Pechersky]

For pr147, making the PR itself seems hard because one needs to login as the user.

[Eric Wieser]

Do we need to have the tool create the PR? Instead we could just let the user do that, and have CI update the wiki page

[Yakov Pechersky]

That sounds fine to me

[Yakov Pechersky]

Do you think the git push --set-upstream ... should also be the user's responsibility, or the tool's?

[Yakov Pechersky]

https://github.com/leanprover-community/mathlib-tools/pull/149 adds hyperlinks to the PRs in flight to the pdf graphs to make it easier to track/contribute