about PR

Stream: new members

[Alex Zhang]

I wrote several more lemmas about inverse matrices connecting some existing lemmas built-in, which will then be helpful for proving things like (A ⊗ B)⁻¹ = A⁻¹ ⊗ B⁻¹ (at least for my own defined version, I noticed there is another PR regarding Kronecker product).
Unfortunately, I am extremely new to PR (also extremely new to GitHub actually), would it be better to post my code here for a precheck?

[Eric Wieser]

For anything more than about 50 lines, the best way to share it (without going as far as submitting a PR) is usually via https://gist.github.com

[Eric Wieser]

Which requires a github account, but does not require knowledge of how to use git itself.

[Alex Zhang]

Thanks for letting me know the proper way for posting my code. And yes, I do have an account.

[Alex Zhang]

https://gist.github.com/l534zhan/3fb4a73857eff68ad1ba230b848040df

[Alex Zhang]

Here is the code!

[Eric Wieser]

A quick trip: your conj_transpose exists already on square matrices as docs#star, although that doesn't help much for rectangular matrices

[Eric Wieser]

And a style remark: : and := should have spaces either side in the mathlib style.

[Eric Wieser]

Otherwise that looks good

[Eric Wieser]

The real question is how much of that is already in mathlib and just hard to find

[Alex Zhang]

Thanks! I will modify the style. Yes, my defn is for a general matrix. Perhaps I will add a bridge to the already existing one for square matrices.

[Alex Zhang]

May I get the write access to non-master branches of the mathlib repository? My userid is l534zhan @Eric Wieser

[Kevin Buzzard]

What's your github userid?

[Alex Zhang]

I added my id above.

[Eric Wieser]

Invite sent!

[Alex Zhang]

Received with thanks!!

[Alex Zhang]

I have made a PR adding a single lemma.
image.png
I have given it the label easy.
Is there any other label I need to give it?

[Ruben Van de Velde]

awaiting-review is a good one

[Alex Zhang]

Is there anything else I need to do other than waiting?

[Eric Wieser]

I'll go look at #8179 now

[Alex Zhang]

If I am to contribute a large portion to an existing file. Am I supposed to add my name to the existing file header?
For example, if the header is

/-
Copyright (c) 2015 Joe Cool. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Joe Cool.
-/

should I add my name to the first line and the third line or the third line only?

[Anne Baanen]

I believe the first line is not supposed to be modified, so the third line only.

[Anne Baanen]

(The correct format, for easy parsing, is Authors: Joe Cool, Alex Zhang, separated by commas and no . at the end, by the way.)

[Eric Wieser]

The rough idea is that you should add yourself to the author list if you're a good person to ask about the contents of the file (as well as having authored parts of it)

[Kalle Kytölä]

A practical newbie-question about PRs. The tutorial video "Making pull requests to mathlib" explains very clearly how to make a single PR, from a newly created branch of mathlib. I'd like to know what is the recommended way to make multiple PRs (perhaps even simultaneously).

One obvious way would to create a new branch for every PR and follow the tutorial. But it seems like this might result in an unnecessarily large number of branches of mathlib. Is this an issue at all, if all my branches are in a "subfolder", say if all are of the form kkytola/*? Should I in fact create a new branch for every PR? :dizzy:

[Kalle Kytölä]

There are two reasons I ask.

The more immediate one is that in my second ever PR #8329, it seems also my very first PR shows as diff, although the first PR #8187 had already been merged to master (I made both from the same branch). I tried to also merge master back to my branch before making the second PR. I have no idea why it shows the old differences, since these should be neither differences to my own branch nor to master. :anguished:

There is also a more general reason I am asking this. Here I will be assuming that I just messed up something when creating two consecutive PRs from the same branch, and this otherwise this could have been done cleanly. But what is the best way to do multiple simultaneous (small) PRs? If it is desirable to avoid a large number of separate branches, how should this be done? I imagine there could be two different cases: simultaneous PRs that don't depend on each other (say touch different files that don't import each other), and simultaneous PR's of which one depends on another. I have noticed the dependent PR tag in Github, but how it should be handled on the level of branches?

[Eric Wieser]

Branches are cheap, especially since bors will delete the branch for you after the PR is merged

[Anne Baanen]

Making multiple branches is indeed the correct way to do it! Git is smart enough to recognize when two branches share identical files, so branching is a very "cheap" operation.

[Eric Wieser]

But putting them in a "folder" starting with your username is usually a good idea, as you mention

[Eric Wieser]

Since then there's no risk of you picking a branch name someone else is using and clobbering their work

[Anne Baanen]

(In fact, branches are not much more than a name + reference to a commit, so you can create hundreds of branches without fear.)

[Anne Baanen]

If you want to make simultaneous PRs, that do not depend on each other, make sure to git checkout master before creating a new branch. That way, your previous commit will not be included in the history of the new branch.

[Eric Wieser]

Also make sure to rerun leanproject get-cache after checking out master before working on the second branch, as you might have a messy cache left from the first branch.

[Anne Baanen]

To fix #8329, the following steps should be enough:

• git checkout kkytola/first_pr
• git fetch origin
• git merge origin/master
• git push

[Eric Wieser]

(does vscode modify the cache?)

[Kalle Kytölä]

Thank you so much for incredibly fast and helpful answers, Eric and Anne!

I'll try to fix my PR as proposed by Anne.

[Anne Baanen]

Kalle Kytölä said:

Thank you so much for incredibly fast and helpful answers, Eric and Anne!

You are welcome, and thanks to you for contributing to mathlib! (I need something to do while my code is compiling!)

[Kalle Kytölä]

Doing Anne's fix, I realize my mistake was I forgot the origin in origin/master when I tried to merge to master before the second PR (I essentially only ever used git on my own computer, complete newbie with PRs). So master had not in fact been merged back to my branch... This would have been avoided by a fresh branch, so that's what I think I will do in the future.

[Anne Baanen]

Kalle Kytölä said:

I'll try to fix my PR as proposed by Anne.

Looks good now :octopus:

[Anne Baanen]

Kalle Kytölä said:

Doing Anne's fix, I realize my mistake was I forgot the origin in origin/master when I tried to merge to master before the second PR. So master had not in fact been merged back to my branch... This would have been avoided by a new branch, so that's what I think I will do in the future.

I already suspected something like that :) Especially when you're just starting out, it is hard to distinguish between master and origin/master and what GitHub calls master at this moment (all of these are different!)

[Kalle Kytölä]

Wait, so master is my local branch master, I guess? And origin/master is the branch master in the remote something, where the repository mainly lives (sorry, technical accuracy with this is obviously not my forte). But isn't that in GitHub? So why would GitHub's master be yet different?

[Anne Baanen]

origin/master wass the most recent version of master branch, at the most recent point in time that Git fetched the branches from the remote repository called origin (i.e. in our case, GitHub)

[Anne Baanen]

By including git fetch origin in the above list of commands, I made sure that this was as up to date as possible

[Anne Baanen]

Otherwise if you hadn't run git pull or git fetch in between, you might still have the version of origin/master from before #8187 was merged!

[Yakov Pechersky]

What's important to know about git is that it is everything is specified by some hash. Everyone agrees on what hash represent what set of files/changes. Each hash can have a number of labeles assigned to it. However, different users can disagree about what label is on what hash! So a branch is just a new label. Your master might be behind the master someone else has, if you haven't incorporated their changes (and updated to what hash the master label points).

[Yakov Pechersky]

Those git pull and git fetch commands basically say, "retrieve the changes that happened upstream", where pull means "and also update my labels".

[Yakov Pechersky]

Because you cloned from github, your upstream is github. It doesn't need to be in the general case, but for mathlib, that is what makes sense.

[Yakov Pechersky]

I just looked at my git log and saw

*   commit eaffefa2412fad5da091f344761d09532ef0c0b3 (origin/kkytola/first_pr)
|\  Merge: 5bb2c00d0 b577bb2cd
| | Author: Kalle-swift <kalle.kytola@aalto.fi>
| | Date:   Fri Jul 16 01:02:28 2021 +0300
| |
| |     Merge remote-tracking branch 'origin/master' into kkytola/first_pr
| |
| * commit b577bb2cd1f96eb47031878256856020b76f73cd (origin/staging, origin/master, origin/lean-3.31.0, origin/HEAD)
| | Author: Rémy Degenne <Remydegenne@gmail.com>
| | Date:   Thu Jul 15 21:23:27 2021 +0000
| |
| |     feat(measure_theory/conditional_expectation): define condexp_L2, conditional expectation of L2 functions (#8324)

[Yakov Pechersky]

which shows all the different labels people have

[Yakov Pechersky]

So your label of what master is might differ from what my label, or github's label is. And when you say git merge master, it merges based on what your label is at the moment.

[Yakov Pechersky]

Even if you said git merge origin/master, it would merge what you thought the origin/master label to be at the moment. That step doesn't say "let me first check what it is at origin." Because then how would git work when you're not connected to the internet?

[Anne Baanen]

In fact, you don't even need to connect to a website like GitHub in order to share commits: the Linux kernel, which Git was originally created for, sends all their commits by email

[Patrick Massot]

Kalle Kytölä said:

Is this an issue at all, if all my branches are in a "subfolder", say if all are of the form kkytola/*?

Putting a / in a branch name is an incredibly bad idea. git itself won't be confused but you will probably, and there there is no guarantee that leanproject won't. You can replace that / with an underscore for instance.

[Eric Wieser]

I don't agree with that statement at all (edit: I misread it as claiming git would be confused). My visual git client even groups together such branches under a subfolder.

[Eric Wieser]

Many projects use such a branch naming structure to group "maintenance" branches that correspond to old releases (not that mathlib has any interest in releases!)

[Patrick Massot]

Eric, in France almost half the population is reluctant to get a Covid vaccine, mostly because the government insists so much so it must be trap. That's about 35 million people are dead wrong. Those things happen.

[Kalle Kytölä]

Are there some instructions on creating dependent PRs? Will it work if I create a branch out of another branch from which an existing PR has been made and then select a tag?

[Johan Commelin]

@Kalle Kytölä What do you mean with "select a tag"?

[Johan Commelin]

The rest of what you said sounds good. It should just work.

[Kalle Kytölä]

I meant from the "label"s (sorry, not "tag"s) on GitHub in the PR. I though I had seen one indicating dependence, but I now didn't find it.

[Johan Commelin]

@Kalle Kytölä aha, you mean blocked-by-other-PR.

[Johan Commelin]

That's handled by a bot.

[Johan Commelin]

If you create a new PR, there is some text in the PR form input box thingy. It explains how to mark another PR as dependent PR.

[Kalle Kytölä]

Thank you!

[Johan Commelin]

See the top post of #9748 for a random example