Zulip Chat Archive

Stream: triage

Topic: PR #4716: chore(category_theory/limits/preserves): preser...


view this post on Zulip Random Issue Bot (Nov 04 2020 at 14:15):

Today I chose PR 4716 for discussion!

chore(category_theory/limits/preserves): preserve limit of special shape
Created by @Bhavik Mehta (@b-mehta) on 2020-10-20
Labels: RFC, WIP

Is this PR still relevant? Any recent updates? Anyone making progress?

view this post on Zulip Johan Commelin (Nov 04 2020 at 14:30):

@Rob Lewis Can we configure the triage bot to choose PRs that are somewhat oldish?

view this post on Zulip Johan Commelin (Nov 04 2020 at 14:30):

This one is about two weeks old...

view this post on Zulip Bhavik Mehta (Nov 04 2020 at 15:05):

It's passively ongoing, I've taken out a part of it in #4857 and I'll cut up the original a bit more

view this post on Zulip Mario Carneiro (Nov 04 2020 at 15:27):

two weeks is the "oldish" cutoff

view this post on Zulip Johan Commelin (Nov 04 2020 at 15:32):

Hmm... can we move that to 1 month?

view this post on Zulip Johan Commelin (Nov 04 2020 at 15:32):

Actually, doesn't matter too much

view this post on Zulip Johan Commelin (Nov 04 2020 at 15:32):

Just "bad luck" that the bot chose something that's 2w+1d old

view this post on Zulip Rob Lewis (Nov 04 2020 at 16:05):

Two weeks seems old enough that a prod from the bot could have an affect. Makes more sense for some than others. But I think it' reasonable.

view this post on Zulip Bhavik Mehta (Nov 04 2020 at 16:16):

Could the bot use "last activity" rather than creation date? That PR had a push 4 days ago, so it feels odd to mark it as oldish

view this post on Zulip Rob Lewis (Nov 04 2020 at 16:19):

We could. The activity tracker is very sensitive. A bot updating a label counts as activity. It's basically a question of whether we prefer false positives or negatives.

view this post on Zulip Random Issue Bot (Jan 01 2021 at 14:29):

Today I chose PR 4716 for discussion!

chore(category_theory/limits/preserves): preserve limit of special shape
Created by @Bhavik Mehta (@b-mehta) on 2020-10-20
Labels: WIP

Is this PR still relevant? Any recent updates? Anyone making progress?


Last updated: May 18 2021 at 22:15 UTC