Random Issue Bot (Nov 14 2020 at 14:16):
Today I chose issue 2376 for discussion!
omega is slow with nonstandard 7
Created by @Kevin Buzzard (@kbuzzard) on 2020-04-10
Is this issue still relevant? Any recent updates? Anyone making progress?
Kevin Buzzard (Nov 14 2020 at 15:00):
How about I close this issue and just copy the example into #1484?
Kevin Buzzard (Nov 14 2020 at 15:02):
Oh -- Rob already mentions this issue in #1484. How about I close this issue? Presumably that won't make Rob's comment https://github.com/leanprover-community/mathlib/issues/1484#issuecomment-611962821 magically disappear or be corrupted in any way? If someone with some github knowledge confirms closing #2376 won't break that link, this issue can be closed.
Reid Barton (Nov 14 2020 at 15:05):
I don't think closing issues as part of other issues that are grab bags is really helpful
Kevin Buzzard (Nov 14 2020 at 15:06):
One argument for closing it is that the specific problem which the issue raises was one which had arisen in a slightly artificial situation (I think caused by
fin_cases) and which might not show up much. Another argument for closing it is that we'll have one fewer issue. The issue with omega is unfortunately clear -- it needs to be rewritten. I cannot imagine anyone expending any energy in porting what we have to Lean 4.
Reid Barton (Nov 14 2020 at 15:07):
We could merge all open issues into one and that would reduce the number of issues too!
Reid Barton (Nov 14 2020 at 15:08):
but maybe in the case of
omega where we don't really expect anyone to fix the issues it's reasonable
Kevin Buzzard (Nov 14 2020 at 15:09):
I see. So you're arguing that "omega is broken" is somehow not a good issue, because there is a chance that someone might come along and fix some subset of them.
Reid Barton (Nov 14 2020 at 15:09):
Reid Barton (Nov 14 2020 at 15:10):
not sure if some kind of tagging organization would help
Reid Barton (Nov 14 2020 at 15:11):
e.g. we could close all omega issues with wontfix, or maybe just mark them somehow?
Rob Lewis (Nov 14 2020 at 15:29):
@Mario Carneiro you had thoughts about reimplementing
omega a while back, has that been set aside?
Mario Carneiro (Nov 14 2020 at 18:40):
I'm not actively working on it but I haven't given up on the idea
Last updated: May 09 2021 at 16:20 UTC