Zulip Chat Archive

Stream: triage

Topic: PR #5591: feat(geometry/manifold/instances): sphere is a ...


view this post on Zulip Random Issue Bot (Jan 28 2021 at 14:24):

Today I chose PR 5591 for discussion!

feat(geometry/manifold/instances): sphere is a topological manifold
Created by @None (@hrmacbeth) on 2021-01-03
Labels: awaiting-author, merge-conflict

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

view this post on Zulip Heather Macbeth (Jan 28 2021 at 16:10):

Hmm, the bot is not very smart. The last dependency for this PR was merged this morning.

view this post on Zulip Rob Lewis (Jan 28 2021 at 16:36):

The bot isn't smart at all, don't put too much thought into its prods!

view this post on Zulip Bryan Gin-ge Chen (Jan 28 2021 at 16:56):

Would it help if we changed this line to use i.updated_at?

view this post on Zulip Rob Lewis (Jan 28 2021 at 17:00):

Sure, depending on what we want the behavior to be. If it goes off update time instead of post time maybe it's worth lowering the time delta a bit.

view this post on Zulip Bryan Gin-ge Chen (Jan 28 2021 at 17:08):

leanprover-community/azure-scripts#8 uses update time and delta of 7 days


Last updated: May 09 2021 at 15:11 UTC