Zulip Chat Archive

Stream: triage

Topic: issue #2376: omega is slow with nonstandard 7


view this post on Zulip 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
Labels: meta

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

view this post on Zulip Kevin Buzzard (Nov 14 2020 at 15:00):

How about I close this issue and just copy the example into #1484?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Reid Barton (Nov 14 2020 at 15:09):

Right

view this post on Zulip Reid Barton (Nov 14 2020 at 15:10):

not sure if some kind of tagging organization would help

view this post on Zulip Reid Barton (Nov 14 2020 at 15:11):

e.g. we could close all omega issues with wontfix, or maybe just mark them somehow?

view this post on Zulip Rob Lewis (Nov 14 2020 at 15:29):

@Mario Carneiro you had thoughts about reimplementing omega a while back, has that been set aside?

view this post on Zulip 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