Zulip Chat Archive
Stream: triage
Topic: issue #2367: interval_cases bugs
Random Issue Bot (Feb 08 2022 at 14:17):
Today I chose issue 2367 for discussion!
interval_cases bugs
Created by @Kevin Buzzard (@kbuzzard) on 2020-04-09
Labels: bug, please-adopt, meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Mar 31 2022 at 14:13):
Today I chose issue 2367 for discussion!
interval_cases bugs
Created by @Kevin Buzzard (@kbuzzard) on 2020-04-09
Labels: bug, please-adopt, meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Dec 19 2022 at 14:08):
Today I chose issue 2367 for discussion!
interval_cases bugs
Created by @Kevin Buzzard (@kbuzzard) on 2020-04-09
Labels: bug, please-adopt, t-meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Kevin Buzzard (Dec 19 2022 at 14:15):
If we observe the same behaviour in mathlib4 then I would venture that this would be a new mathlib4 issue, so this is probably "thanks for the observation, but wontfix"?
Alex J. Best (Dec 19 2022 at 22:29):
it would be good to label these issues somehow, as "potentially mathlib4 relevant eventually" vs those which definitely wont be
Random Issue Bot (Feb 20 2023 at 14:09):
Today I chose issue 2367 for discussion!
interval_cases bugs
Created by @Kevin Buzzard (@kbuzzard) on 2020-04-09
Labels: bug, please-adopt, t-meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Kevin Buzzard (Feb 20 2023 at 14:27):
My understanding is that these are being dealt with in mathlib4
Random Issue Bot (Jun 04 2023 at 14:06):
Today I chose issue 2367 for discussion!
interval_cases bugs
Created by @Kevin Buzzard (@kbuzzard) on 2020-04-09
Labels: bug, please-adopt, t-meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Kevin Buzzard (Jun 04 2023 at 22:49):
Both of these issues do not appear to exist in the Lean 4 version of the tactic, so I propose closing this issue. Is this the correct thing to do?
Ruben Van de Velde (Jun 04 2023 at 23:14):
I don't really understand why these were turned on again; I'd be inclined to pause them until the port is done
Eric Wieser (Jun 05 2023 at 00:06):
I turned on these bots when I turned on all the other CI scripts that timed out after 90 days
Eric Wieser (Jun 05 2023 at 00:07):
I agree they're not providing much value
Kevin Buzzard (Jun 05 2023 at 09:20):
They're definitely providing some entertaniment value.
Random Issue Bot (Jul 01 2023 at 14:07):
Today I chose issue 2367 for discussion!
interval_cases bugs
Created by @Kevin Buzzard (@kbuzzard) on 2020-04-09
Labels: bug, please-adopt, t-meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Kevin Buzzard (Jul 02 2023 at 03:12):
I closed it.
Last updated: Dec 20 2023 at 11:08 UTC