public PRs

Stream: general

[Mario Carneiro]

I'd like to introduce a slight change in PR management on mathlib. In order to support third party contribution to PRs, I would like to introduce "PR branches" to mathlib. The basic idea is, if there is a PR that is currently in review, for which you are not the author, and you would like to help get it into mathlib, just ask to have it made public on the PR page, and I will add it as a branch on the mathlib repo. This way, if a PR is stalled, you can get it back on track. I think this will make collaboration on WIPs easier, although it will probably confuse GitHub a bit, because of the way PR pages are set up. If you PR to a PR branch, make sure to reference the original PR # so that we can navigate between them through GitHub.

[Simon Hudon]

Would it be useful to have a separate account for those WIP? That way you can have a stricter separation between the PRs. The added benefit is that you may promote more maintainers for that account

[Mario Carneiro]

an interesting idea, I hadn't thought about having a public fork

[Mario Carneiro]

You may or may not recall that mathlib was once https://github.com/leanprover/library_dev . When we first moved from library_dev to mathlib, the idea was that library_dev might contain more experimental stuff or stuff that doesn't quite compile, but that never really happened

[Simon Hudon]

I vaguely remember. I think a PR account might have to refrain from having a master branch. It would really be only a waiting room for big PRs

[Mario Carneiro]

well, if it's a fork of mathlib then it will have a master branch, that is just tracking mathlib

[Simon Hudon]

Yeah exactly. I would just refrain from merging anything into master that leanprover/mathlib doesn't have

[Mario Carneiro]

I'm liking the idea so far. @Jeremy Avigad What do you think about this? I can create a lean-sandbox user account, fork mathlib, and just give write access to anyone who wants it. People can still use the PR system on the sandbox account if they want, or create branches and PR them to mathlib.

[Simon Hudon]

I recently created https://github.com/leanprover-community/lean-mode-contrib to host community contributions to lean-mode. It could double as a home for mathlib PRs

[Mario Carneiro]

sounds good

[Mario Carneiro]

is lean-mode-contrib a fork of something?

[Simon Hudon]

Not quite. I thought I'd make it a mode that adds to lean-mode. I'm replicating some functionalities from company-coq. And now that the repo exists, I think I'll start adding some of my own scripts (like shortcuts for adding common libraries to your leanpkg.toml file).

[Simon Hudon]

Now that you ask, it might work if I just make it a fork of lean-mode with added features.

[Jeremy Avigad]

@Mario Carneiro no objection here.

[Mario Carneiro]

Great! @Kevin Buzzard What do you think about migrating for_mathlib to this new repo?

[Simon Hudon]

I suggest we choose a couple of maintainers for that repo. I already sent you and Johannes an invitation. I can send others.

[Mario Carneiro]

I can be a maintainer, but I expect there won't be much maintaining going on

[Mario Carneiro]

mostly it's just branch organization and such

[Mario Carneiro]

Since the idea is to have it free for all, it's up to individuals to maintain their own branches as they see fit

[Mario Carneiro]

I am inspired in part by metamath's "mathbox" infrastructure, although in that case the mathboxes are required to compile at all times but are otherwise organized at the discretion of the user

[Simon Hudon]

In principle, the maintainers will have to accept pull requests too. That's why I would err towards more maintainers rather than fewer.

I've never heard of the mathbox. Do you have a reference for it?

[Mario Carneiro]

http://us.metamath.org/mpeuni/mmtheorems.html#19

[Kevin Buzzard]

I don't really understand this proposal (that's not some implied criticism -- I just actually mean I don't understand it). I've just looked through the perfectoid for_mathlib directory and I see stuff I wrote and then forgot about, stuff which would be trivial to PR into mathlib, stuff which I half-wrote (quotient rings) and then someone else wrote better and which might already have been PR'ed -- after our discussion yesterday I'm wondering whether actually it might introduce some kind of order into the system if some of the really basic stuff like quotient additive groups and quotient rings should get into mathlib ASAP (indeed some of it might be there already). One thing I certainly don't want is for us to end up in the situation where people are relying on me to do things, as I already have far too much to do. As you know Mario I have started making tiny mathlib PRs, just dipping my toe in as it were; the stuff I put in "for_mathlib" myself is just stuff which I feel like it would be too much effort for me to PR into mathlib. On the other hand I'm coming round to the idea that perhaps working from the bottom up is actually a good idea (rather than what we're currently doing, which is working top down, bottom up and in the middle all at once).

I think the problem I currently have with the mathlib set-up (which is I think why I started the "for-mathlib" directory) is the following. Let's say I realise I need 50 lines of code about e.g. topological groups, which is not in mathlib, but which would very naturally live in an existing mathlib file, e.g. analysis/topology/topological_structures.lean. The thing is, I want them now. I could either edit topological_structure.lean and make a PR, which would take me a long time because mathlib has conventions I don't know about or don't understand, and then there would be some to-ing and fro-ing whilst people told me that I've proved this lemma in a stupid way, and that lemma is just by simp, and that lemma is already there, and that lemma never uses inverses so it should really be in the topological monoid section -- and then I have to find time to edit everything etc etc to try and fix it up -- and this process can easily go on for weeks. During that time I find it really hard to actually access my own work, because it is "in limbo" -- it's not in mathlib and so it's not in my project. It's much easier just to write for_mathlib/topological_structures.lean and prove the lemmas I want, with their bad names and bad proofs and superfluous hypotheses, because then I can start using them immediately, because I'm not really interested in these lemmas anyway, I'm far more interested in doing the "meat" which is the perfectoid spaces, and in some sense I just want someone else to prove these basic facts about topological groups, someone who knows what they're doing and will do it right the first time. Unfortunately the set of such people is pretty small and they all have their own things that they're doing. I'm not motivated to PR, because of this.

Will the proposed system offer some sort of alternative approach which gets me out of this hole?

[Mario Carneiro]

One thing I certainly don't want is for us to end up in the situation where people are relying on me to do things, as I already have far too much to do.

The idea here is to allow other people to work on your PRs

[Mario Carneiro]

Let's say I realise I need 50 lines of code about e.g. topological groups, which is not in mathlib, but which would very naturally live in an existing mathlib file, e.g. analysis/topology/topological_structures.lean. The thing is, I want them now.

I am fully aware of this situation, I often have to deal with it myself. The solution I came up with for this is to have a pending directory or file, which serves basically the same purpose as your for_mathlib. The difference is that I PR first, and then put something as close as possible to my PR into this pending area during the review period. That way, once the PR is accepted all I have to do is delete the relevant portion from the pending area.

[Mario Carneiro]

(mathlib used to have a pending directory, but I removed it since lean core no longer accepts PRs.)

[Kevin Buzzard]

I see. So basically you're saying that I'm doing it wrong, and I am beginning to learn from my own experience that the "code now, PR later" approach has its disadvantages (e.g. I think that my partially written quotient ring code might be obsolete -- did Chris PR this? I still struggle with quotients; I have a ≈ 0↔ ⟦a⟧ = ⟦0⟧ : by sorry in my code at some point). I think it's far easier (for me at least) to understand other people when they say "do it my way not your way", once I've begun to realise the disadvantages of my way.

[Johan Commelin]

Which is a pity. It would be awesome if they would accept one final PR that moved all of core into mathlib.

[Mario Carneiro]

I'm not saying you have to PR everything as soon as it is written. But once you decide you have something you want to get into mathlib, it moves from where it currently is, probably some random file in your project, to the for_mathlib area and also into a PR, possibly [WIP]. Then you get feedback on your stuff, and if you make any updates to the PR you can either copy them to your local version or just leave the pending area out of date and update later (if you think it will affect your project I would recommend you update sooner rather than later).

[Mario Carneiro]

I think it's far easier (for me at least) to understand other people when they say "do it my way not your way", once I've begun to realise the disadvantages of my way.

I know I have a bad habit of asking people to "do it my way not your way", but I try to explain what the major issues are. The main problem is that making bad design decisions can be very expensive time-wise, without even alerting you to the possibility that the cost is avoidable. So when I hear that you've been struggling with an issue for several months and just working around it, my heart goes out to you and I wish I could have saved you from that.

[Johan Commelin]

Is this public repo already available?

[Mario Carneiro]

it is now https://github.com/leanprover-community/mathlib

[Johan Commelin]

Ok, cool! And how would one create a new public PR branch on it?

[Johan Commelin]

Should one ask for push access in this topic?

[Mario Carneiro]

yeah, that seems fine

[Mario Carneiro]

okay I think I figured it out. You should now be a "collaborator" on leanprover-community/mathlib

[Mario Carneiro]

I just sent invites to everybody who has ever been reasonably active on mathlib. If you didn't get one just ask

[Simon Hudon]

If you want to use leanprover-community/mathlib to create a PR, I propose you start by creating a branch from leanprover/master. Do not commit to leanprover-community/master directly, that branch is only meant to track leanprover/master.

[Patrick Massot]

Let me check I understand correctly what I'm meant to do. I close my current norm PR. Push my norm branch to this new repository, open a new PR from there, right?

[Scott Morrison]

Yes, that's about right!

[Sean Leather]

The shared mathlib fork doesn't seem to add much benefit over any other mathlib fork. You could easily use your own. It really is just a bit more convenient is that it has an established “trusted” set of collaborators, so that anyone in that group can contribute to anyone else's work. But if you want to work with only a different set of collaborators, you can also set up your own fork. But it's also a bit more questionable in that there's no clear policy for who does what with what branches, which can cause problems if people have different assumptions or don't communicate changes to each other.

[Patrick Massot]

Clearly it assumes quite a bit a trust, but let's see how it goes (I'm pretty optimistic here).

[Sean Leather]

I think I'd do this differently. Instead of a mathlib fork, I'd suggest a sort of mathlib nursery, which is a library that has mathlib as a dependency. The collaborators would be set up as they are now, but the library source would be initially empty and added to by anyone on the master branch. Then, everybody moves WIP stuff into the mathlib-nursery. Once somebody's happy with part of their work, they can get feedback from others and somebody can PR that to mathlib. When the PR makes it into mathlib, the mathlib dependency commit is updated and the work is removed from mathlib-nursery.

[Patrick Massot]

Too late, I opened https://github.com/leanprover/mathlib/pull/241 Let's see how this idea works out

[Sean Leather]

The main difference is that everybody works on mathlib-nursery/master instead of multiple mathlib branches.

[Sean Leather]

Actually, maybe mathlib-nursery and this mathlib fork can coexist and both be useful.

[Patrick Massot]

The advantage of the current proposal is we don't have to move things into their final position

[Sean Leather]

So, work starts in the nursery and then moves to the fork.

[Patrick Massot]

And now Mario has to work on norms in order to prove his new workflow is useful :wink:

[Sean Leather]

The advantage of the nursery is that things can change and you don't need to worry about final positions. :smile:

[Patrick Massot]

My experience is that the moving to final position phase is very boring and time consuming

[Sean Leather]

And now Mario has to work on norms in order to prove his new workflow is useful :wink:

But the leanprover-community/mathlib doesn't add anything to what you're doing. You could always have allowed the mathlib collaborators access to your branch.

[Sean Leather]

What it does allow is non-mathlib collaborators to work on your branch.

[Patrick Massot]

Right, so you should work on that branch, mess it up and prove Mario was wrong.

[Patrick Massot]

no, wait

[Sean Leather]

Alternatively, if it was in a nursery, I could already be using it within the nursery. :wink:

[Patrick Massot]

Say Kenny works on it

[Patrick Massot]

or Chris, and prove Mario was right

[Kenny Lau]

work on what

[Johan Commelin]

You should do Patrick's homework :rolling_on_the_floor_laughing:

[Patrick Massot]

https://github.com/leanprover-community/mathlib/tree/norms

[Patrick Massot]

That's a new branch is the new mathlib fork where everyone from the community can improve on a PR

[Mario Carneiro]

The "nursery" idea is closer to the original purpose of library_dev

[Mario Carneiro]

Both options have their uses. I think the main factor is whether you want to work in a project that has a mathlib dependency, or in mathlib itself. For mathlib PRs of course the second option is better

[Mario Carneiro]

For offshoot projects and experiments, a separate project is maybe nicer to work with, although you lose the ability to modify bits of mathlib to accomodate the work

[Sean Leather]

Both options have their uses. I think the main factor is whether you want to work in a project that has a mathlib dependency, or in mathlib itself. For mathlib PRs of course the second option is better

Yeah, agreed. I think it would be nice to have a community-based nursery for stuff not ready for PR.

[Sean Leather]

So, there could be a staged process:

1. throw it in the nursery, let other people use it or work on it
2. when matured, create a community mathlib PR for it

[Sean Leather]

By definition, what's in the nursery is immature.

[Kevin Buzzard]

Whilst I have no understanding of the ins and outs of this new proposal, I think that there's a lot to be said for trying a random new thing and seeing how it turns out.

[Kevin Buzzard]

OK so I want to try and get some of this for_mathlib stuff out of the perfetoid repo and into mathlib. I want to start with https://github.com/kbuzzard/lean-perfectoid-spaces/blob/master/src/for_mathlib/add_submonoid.lean that file, which is Johan Commelin literally translating https://github.com/leanprover/mathlib/blob/master/group_theory/submonoid.lean into additive notation. There is also an add_subgroup.lean file which is the corresponding translation of subgroup.lean. Do I PR to mathlib? Do I push to mathlib-community?

[Kevin Buzzard]

This is the other file I would like to get into mathlib: https://github.com/kbuzzard/lean-perfectoid-spaces/blob/master/src/for_mathlib/add_subgroup.lean, a translation of https://github.com/leanprover/mathlib/blob/master/group_theory/subgroup.lean .

[Mario Carneiro]

literal translation of files to additive notation is what to_additive is for

[Kevin Buzzard]

OK. So what do we do?

[Kevin Buzzard]

Because at the end of the day I want to quotient out an additive group by a subgroup and it's time to make progress.

[Kevin Buzzard]

because what I really want is to quotient out a ring by an ideal and then borrow some properties from the group quotient.

[Kevin Buzzard]

because what I really want is to prove some basic results about valuations, and I need ring quotients.

[Mario Carneiro]

PR it

[Kevin Buzzard]

PR the two files I just linked to? To mathlib or the community one?

[Mario Carneiro]

do it from the community fork if you think someone else is going to clean it up for you

[Kevin Buzzard]

What if I don't have a clue if someone else is going to clean it up for me and I don't know how to do it myself either?

[Mario Carneiro]

then I will clean it up or it will languish

[Kevin Buzzard]

And should I then make the perfectoid repo depend on community mathlib instead of regular mathlib?

[Mario Carneiro]

No, you should keep the stuff in for_mathlib and develop the PR independently

[Kevin Buzzard]

I see. Thanks!

[Kevin Buzzard]

So after git push --set-upstream origin additive-subgroup-theory github thinks I'm about to submit a PR to mathlib. Is that what I am supposed to be doing?

[Kevin Buzzard]

My origin is git@github.com:leanprover-community/mathlib.git

[Kevin Buzzard]

i.e. is this just a regular PR to mathlib, but from the community fork rather than my own personal fork?

[Mario Carneiro]

yes

[Simon Hudon]

@Sean Leather I like the idea of a nursery. It makes it easier to get features used faster. The only downside is that you can't adapt any existing features of mathlib. I wonder if it might grow into a huge mess. Maybe we can still try to keep it clean.

[Simon Hudon]

I'm tempted in creating that nursery. Any objections?

[Sean Leather]

I'm tempted in creating that nursery. Any objections?

Go for it. I'll share the responsibility for keeping it clean. If you don't get around to it, I will create it.

[Mario Carneiro]

I'm on board

[Simon Hudon]

Done! You two should have received an invitation. And I think we can include move people still

[Sean Leather]

Got it. Are you going to initialize it with a README.md?

[Mario Carneiro]

You could initialize it with the content of library_dev

[Sean Leather]

One minimal requirement that I would have and would state on the README.md is that the code should build successfully for a given commit of mathlib and Lean version and not have any sorrys. I don't think it's an issue if the code changes significantly over time, but it's a pain for others if it doesn't build.

[Mario Carneiro]

I think that is too strict a requirement. Perhaps it should build but sorry is allowed?

[Sean Leather]

The problem is that sorrys infect downstream code and clutter the error and warning messages.

[Mario Carneiro]

Mathlib already has that requirement, and I know it stops me from publishing stuff early because I think the work is not done yet

[Mario Carneiro]

but for something that brands itself as a "nursery", it should explicitly accept unfinished work

[Sean Leather]

Would it resolve your concern if you're allowed to use non-master branches for that code?

[Sean Leather]

You still have to accept that the library is shared and not private.

[Simon Hudon]

Here it is: https://github.com/leanprover-community/mathlib-nursery

[Sean Leather]

So I think it's appropriate to ask collaborators to minimize the burden.

[Johan Commelin]

"The features are available a library in the meantime." typo in the README

[Mario Carneiro]

A sorry in the middle of the code doesn't hurt anyone, and it is still being checked for correctness

[Mario Carneiro]

I would rather just filter out sorry warnings

[Johan Commelin]

But I don't think it is too much trouble to do everything in non-master branches, right?

[Simon Hudon]

@Johan Commelin It is work in progress, I'll get it right eventually ;-)

[Mario Carneiro]

Well, the nursery is different since it's not tracking mathlib

[Johan Commelin]

If you make me a collaborator, you could delegate that (-;

[Mario Carneiro]

it needs a master branch, and everyone should be not too far away from it

[Johan Commelin]

Hmmm. I don't understand nurseries.

[Johan Commelin]

(Never went to one as a toddler.)

[Sean Leather]

A sorry in the middle of the code doesn't hurt anyone, and it is still being checked for correctness

I disagree. It adds overhead in terms of messages.

I would rather just filter out sorry warnings

How?

[Mario Carneiro]

awk script?

[Sean Leather]

Also, I'd like to see my own sorry messages and not those of others

[Mario Carneiro]

then don't compile or depend on others

[Mario Carneiro]

we can have the travis build just ignore sorries

[Sean Leather]

Well, the nursery is different since it's not tracking mathlib

But it is, isn't it? https://github.com/leanprover-community/mathlib-nursery/blob/master/leanpkg.toml#L8

[Sean Leather]

I'd really rather not have sorrys in the first place. I don't think that's too strong a requirement.

[Simon Hudon]

It depends on mathlib but does not track it

[Mario Carneiro]

I mean in the git sense - it's not a fork

[Sean Leather]

Well, forks also don't track in any sense that I can think of. :wink:

[Mario Carneiro]

I can tell you for sure that there are people who work with sorries for long periods, on projects that would be appropriate for this nursery

[Mario Carneiro]

and this was also how library_dev worked

[Mario Carneiro]

Even in mathlib it feels like too strong a requirement sometimes. It's just that lean has a completely stupid reporting mechanism for sorry

[Sean Leather]

The downstream warnings are definitely too much.

[Mario Carneiro]

they make sense in server mode but not in lean --make

[Mario Carneiro]

I recall in one instance I defined a sorry' axiom just to avoid the loud warnings

[Sean Leather]

Personally, I'd rather be free of sorry warnings. But I understand that others may have different opinions, so, as a compromise, I propose that we make master free of sorrys and allow them in non-master branches.

[Sean Leather]

I recall in one instance I defined a sorry' axiom just to avoid the loud warnings

That seems like a reasonable compromise, too.

[Simon Hudon]

i find sorry' to be a terrifying option

[Mario Carneiro]

Unfortunately it's a bit too quiet

[Sean Leather]

It's like sorry with a tear. :cry:

[Simon Hudon]

Also, I'd like to minimize the number of branches so that it can be useful as a library

[Mario Carneiro]

what about sorry' being a notation for a tactic that uses an axiom and also prints "using sorry"

[Sean Leather]

what about sorry' being a notation for a tactic that uses an axiom and also prints "using sorry"

Interesting...

[Simon Hudon]

Isn't that just as loud as sorry?

[Mario Carneiro]

no downstream warnings this way

[Simon Hudon]

I see. That's a better option. I think I still prefer having master be sorry-free and the rest be fully sorry

[Simon Hudon]

or sorry allowed. Also called Canadian.

[Sean Leather]

Eh?

[Simon Hudon]

(there was no moose)

[Mario Carneiro]

I think I would rather have different projects on different folders of the same branch, because it is much easier to browse

[Mario Carneiro]

and each project will have their own style of maintenance, which may or may not include sorry stuff

[Simon Hudon]

I agree. I would just put temporary versions in branches until the sorries are substituted

[Sean Leather]

So, let's see the desires here:

• Minimize sorrys
• Minimize number of branches
• Prefer directories over branches

[Mario Carneiro]

That may never happen though - I'm thinking of projects with really long term undefined assumptions

[Sean Leather]

I agree with all of those, but the sorry is the one that can affect others the most.

[Mario Carneiro]

like Kevin's top-down formalization projects

[Sean Leather]

I would just put temporary versions in branches until the sorries are substituted

Yes, that's what I'm thinking.

[Mario Carneiro]

it is utterly unreasonable to just say "no getting in here until you're done"

[Sean Leather]

But “unfinished” is not the same as “no sorrys.”

[Mario Carneiro]

In a top-down formalization, it is often impossible to have one without the other

[Mario Carneiro]

unless you use a hack that is equivalent to sorry

[Mario Carneiro]

and I don't want to encourage that

[Simon Hudon]

I must say I'm on the fence

[Sean Leather]

Not everything should go into mathlib-nursery.

[Sean Leather]

It's easy enough to create another repository for other projects.

[Mario Carneiro]

Right

[Sean Leather]

I think mathlib-nursery should be for things that are intended for mathlib and shareable with others.

[Simon Hudon]

What would you put in the nursery, @Sean Leather ?

[Sean Leather]

Things with sorry are not ready to be shared with others.

[Sean Leather]

Kevin's for_mathlib stuff, for example.

[Mario Carneiro]

I think xena would disagree with you on that point

[Sean Leather]

I think xena would disagree with you on that point

I don't understand you.

[Mario Carneiro]

I think the whole lean-perfectoid-spaces project is conceivably within scope for the nursery

[Mario Carneiro]

it is a multiple person project with aspirations to be in mathlib someday, which depends on mathlib but is not properly a part of it right now

[Johan Commelin]

I think xena would disagree with you on that point

I don't understand you.

Xena is one big repo where a dozen people are all working on different projects and using each others stuff. And half of the time it doesn't even build. People really don't care about a few sorries in there.

[Mario Carneiro]

exactly

[Mario Carneiro]

that's what I want to see in the nursery

[Mario Carneiro]

except maybe for the "not building" part

[Simon Hudon]

But we do want it to build at least most of the time, no?

[Johan Commelin]

It is a nursery: toddlers beat each other up, steal each others toys, say sorry, and continue playing together.

[Johan Commelin]

Says the guy who never went there, but has a house with 3 toddlers running around.

[Johan Commelin]

Right, I suggest that mathlib-toddlers at least make sure that their stuff builds. After all, we're grown-ups.

[Johan Commelin]

But even grown-ups should say sorry sometimes.

[Johan Commelin]

Ok, so now comes the fun part!

[Johan Commelin]

What is the punishment for pushing a commit that doesn't build?

[Sean Leather]

Okay, other than Johan taking an analogy too far (:wink:), my idea of a mathlib-nursery is a place where projects that are working can be nursed into shape for mathlib.

[Mario Carneiro]

You broke it, you fix it

[Sean Leather]

So, first you start with your own repository, then you move bits and pieces into the nursery, then you PR to mathlib.

[Johan Commelin]

But that is what the community fork is already doing...

[Sean Leather]

Yes, that's for the PR part.

[Mario Carneiro]

if a fix doesn't appear forthcoming, some annoyed third party may comment out your file

[Johan Commelin]

Right. And if my witt vectors compile, but they take 15 seconds?

[Johan Commelin]

Same treatment, I guess...

[Kenny Lau]

if a fix doesn't appear forthcoming, some annoyed third party may comment out your file

since it would take seconds to even compile the first line of their code

[Simon Hudon]

I'm off to bed. I trust you guy will find a vision you agree on for the nursery

[Sean Leather]

Optimism. :wink: Good night!

[Simon Hudon]

What can I say? I'm monotonically increasing!

[Simon Hudon]

Good day to you, sir!

[Johan Commelin]

Wait! What do you mean with _ in "There should be no sorrys or _."?
We debated the sorrys (and I still think they should be allowed). But what is this _ being forbidden? That's used all over the place in mathlib. I think you mean a specific use of _, but I'm not sure which...

[Mario Carneiro]

I assume the kind of _ that causes "could not synth placeholder" errors

[Sean Leather]

I just put that in the readme as a starting point. We can continue to debate everything. Nothing is set in stone.

[Sean Leather]

Yes, I meant unsolved goals. I'll change it, or someone else could rephrase it.

[Sean Leather]

I've hopefully improved on the wording.

[Johan Commelin]

Does it make sense that if a PR from the community fork is merged that the person who merges (i.e. Mario or Johannes) also deletes the branch on the community fork?

[Johan Commelin]

That keeps the list of branches clean, and it also helps to keep an overview of which branches you can/should work on.

[Johan Commelin]

Or can we have incremental merges from branches on the community fork?

[Johan Commelin]

For example, can/may I work on the docs-theories branched, after it is merged? Or should I start a docs2 branch?

[Mario Carneiro]

Once a branch has been merged, you should at least rebase / remove merged commits from the branch if you want to keep working on it, but there is no harm in retaining the branch name unless it is confusing to you

[Mario Carneiro]

Or you could just add a merge commit to the new master and keep working

[Johan Commelin]

Right, so if I missed the fact that the branch was merged into the official mathlib, then I mess up the repo...

[Mario Carneiro]

well, the merge commit will probably clobber all the work on the branch anyway

[Mario Carneiro]

and as long as I am squash merging it doesn't really matter how messy the branch gets

[Mario Carneiro]

I would be fine with deleting branches after a merge (and github gives me a big button to do exactly that), but it is conceivable that I merge before they are really done

[Mario Carneiro]

For example, I have seen Chris make a PR and then a few more commits come in the next day or two - if I merge those early, then Chris will be in a weird position, even moreso if I delete his branch

[Mario Carneiro]

If I don't delete the branch (or even if I do, I guess), he can recreate the branch from his local copy, add some more commits, and PR again to post the new material

[Johan Commelin]

Right. So in the end... it doesn't really matter, and I can happily push some commits?

[Mario Carneiro]

yeah, basically

[Johan Commelin]

Ok. That's good to know. I'll be offline again for a couple of days, and I still need to read up on the recent additions to the docs. But I hope to add some stuff later on.

[Mario Carneiro]

and I will be traveling this weekend and in germany next week, not sure how much free time there will be