feat: port command

[pechersky]

Copies file from mathlib3port to mathlib4, creating a branch,
committing the new file, updating Mathlib.lean,
and replacing Mathbin with Mathlib

---

$ leanproject port algebra.big_operators.pi  ~/math/mathlib4 ~/math/mathlib3port
$ git log ...
commit 27d4ee5ad2ea913453abaceb55cceeda6624fd0f (HEAD -> ypechersky/port-algebra-big_operators-pi)
Author: Yakov Pechersky <ypechersky@treeline.bio>
Date:   Sun Nov 20 12:07:30 2022 -0500

    Rename imports in ported file from Mathbin to Mathlib

 Mathlib/Algebra/BigOperators/Pi.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

commit 50dcacf55991c40f3bc1209381c458da18154a1c
Author: Yakov Pechersky <ypechersky@treeline.bio>
Date:   Sun Nov 20 12:07:30 2022 -0500

    Include file in import of all files

 Mathlib.lean | 1 +
 1 file changed, 1 insertion(+)

commit fbf87f42c21621f1359698726ac13e4f3aa3d2cb
Author: Yakov Pechersky <ypechersky@treeline.bio>
Date:   Sun Nov 20 12:07:30 2022 -0500

    Initial file copy from mathport

    mathlib3 hash: 39af7d3bf61a98e928812dbc3e16f4ea8b795ca3

 Mathlib/Algebra/BigOperators/Pi.lean | 127 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 127 insertions(+)

commit d199195546fcb037cf89ec396d1fbc54bd046815 (origin/master, origin/HEAD, master)
[...]

[pechersky]

We could assume the user has credentials stored in ~/.git-credentials, otherwise prompt the user for their creds.

[jcommelin]

We could assume the user has credentials stored in ~/.git-credentials, otherwise prompt the user for their creds.

Is this what happens automatically? Or do you need to implement that?

[pechersky]

Should this command make actual PRs, and push? If so, one needs to have credentials to do so (for github). One could assume the credentials are stored already or prompt for them. Or just rely on the user to do the git commands themselves. I haven't planned that far.

[jcommelin]

I think it's enough if this command prepares a branch, together with the first commit.
Then users can do a git push and create a PR themselves.

[PatrickMassot]

Thanks for you contribution. We are closing all pull requests and issues since this tool no longer has any relevance in the Lean 4 era. This repository will now be archived.