leanproject port command

Stream: mathlib4

[Johan Commelin]

@Yakov Pechersky I like your PR here https://github.com/leanprover-community/mathlib-tools/pull/147
I'm not really sure what you meant with the git credentials comment. Can you please clarify?

[Johan Commelin]

It would be good to get this merged, I think.

[Yakov 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.

[Reid Barton]

I think the tool would already be very useful if it just pushes to a branch (if the user approves), which should cause git to prompt the user for any credentials it might need. Then the "go here to open a PR" link should be displayed in the output as well.

[Yakov Pechersky]

Great, so it's almost there! The branch and the seed commits are created. I'm on :palm_tree::dolphin::octopus: vacation right now, so I'm not able to contribute code for the next two weeks or so.

[Yakov Pechersky]

I'm not sure if "git push --set-upstream..." is something gitpython does in a way that exposes the credentials prompt, or if it has to be configured with credentials already.

[Eric Wieser]

I think the tool would already be very useful if it just pushes to a branch

Wouldn't it be better to just have all the branches ready to go for when the user needs them, as a nightly job run by mathport?

[Eric Wieser]

Then the user / leanproject port just runs git reset --hard mathport/some.file.name

[Johan Commelin]

@Mario Carneiro wanted the first commit on the branch to be done by the user that opens the PR, so that the user gets proper git credits.

[Johan Commelin]

If leanproject port is reasonably fast, then I think we don't need to have the branches ready to go.

[Johan Commelin]

@Eric Wieser If you think this looks ready to go, then I suggest we merge it.

[Reid Barton]

Has anyone tested that it still works? I just mean, because the PR is from a month ago.

[Eric Wieser]

Johan Commelin said:

Mario Carneiro wanted the first commit on the branch to be done by the user that opens the PR, so that the user gets proper git credits.

Ah, I'd forgotten about that. Maybe I'll try and fix bors.

[Eric Wieser]

(https://github.com/bors-ng/bors-ng/issues/1393)

[Reid Barton]

In any case the automatic branch creation job would pretty much consist of running this same script

[Eric Wieser]

Either way, the bot could still create the branches, and then leanproject could just run git commit --amend --author ...

[Eric Wieser]

The less we put in leanproject, the easier it is to change how things work without having users on old versions making a mess

[Yakov Pechersky]

Last I tried the command, it worked. It only consumes info, doesn't send info back