Zulip Chat Archive

Stream: general

Topic: new steam for PR discussions


view this post on Zulip Scott Morrison (Oct 07 2018 at 10:26):

I've just created a new stream, after a brief discussion with Mario, for discussion of current PRs.

view this post on Zulip Patrick Massot (Oct 07 2018 at 10:27):

Let me cast the first vote: Merge #397 Now!

view this post on Zulip Scott Morrison (Oct 07 2018 at 10:27):

My main idea is that it is a place for everyone-besides-Mario-and-Johannes to ask each other for help and reviews, without it constituting nagging Mario-and-Johannes.

view this post on Zulip Scott Morrison (Oct 07 2018 at 10:28):

I think it would also be helpful if many more of us participated in reviews of PRs. (I'm certainly too lazy here.)

view this post on Zulip Scott Morrison (Oct 07 2018 at 10:29):

And hopefully it's okay for anyone to give a "positive review" of a PR --- simply chiming in that they've either looked at the changes and they seem good, or even better that they've tried them out in some way.

view this post on Zulip Scott Morrison (Oct 07 2018 at 10:29):

This should then make it easier for Mario and Johannes to deal with the easy ones that don't need significant input from them.

view this post on Zulip Mario Carneiro (Oct 07 2018 at 10:29):

/me approves

view this post on Zulip Patrick Massot (Oct 07 2018 at 10:37):

Yes, I did try 397, it works here. We only miss a VScode one key stroke trick to insert {!!} and Ctrl-.

view this post on Zulip Patrick Massot (Oct 07 2018 at 10:38):

Oh, it's merged now!

view this post on Zulip Patrick Massot (Oct 07 2018 at 10:38):

Thanks!

view this post on Zulip Rohan Mitta (Dec 11 2018 at 12:51):

I've redone my Banach's Contraction Theorem PR (#428) to use the material pointed out by Patrick, I think it's ready now!

view this post on Zulip Johan Commelin (Dec 11 2018 at 15:19):

@Rohan Mitta There is a separate stream for PR's as announced in this thread. I created a thread there for your PR.

view this post on Zulip Johan Commelin (Dec 11 2018 at 15:19):

Here it is: https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/subject/.23428.20Banach.20Contraction/near/151452941

view this post on Zulip Rohan Mitta (Dec 13 2018 at 13:38):

Whoops! Thanks Johan


Last updated: May 10 2021 at 19:16 UTC