issue #2376: omega is slow with nonstandard 7

Stream: triage

[Random Issue Bot]

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?

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

I don't think closing issues as part of other issues that are grab bags is really helpful

[Kevin Buzzard]

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]

We could merge all open issues into one and that would reduce the number of issues too!

[Reid Barton]

but maybe in the case of omega where we don't really expect anyone to fix the issues it's reasonable

[Kevin Buzzard]

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]

Right

[Reid Barton]

not sure if some kind of tagging organization would help

[Reid Barton]

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

[Rob Lewis]

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

[Mario Carneiro]

I'm not actively working on it but I haven't given up on the idea

[Random Issue Bot]

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?

[Kevin Buzzard]

My understanding is that this is wontfix

[Yury G. Kudryashov]

Let's see if mathlib compiles without tactic.omega, see branch#YK-no-omega (I only remove an import, not the actual tactic).

[Yury G. Kudryashov]

It should because we don't import tactic outside of tests

[Johan Commelin]

There is a linter that checks against import tactic.omega

[Alex J. Best]

And also import tactic so there is no way to cheat it by importing tactic and getting omega transitively instead

[Yury G. Kudryashov]

Why do we have tactic.default? Is it for external projects?

[Alex J. Best]

So I don't really see the point of this, omega is a useful tactic still, even if it won't be ported any time I get to an annoying a - 1 - b + 1 = a - b in nat type goals I hit it with omega, even if I have to make a different proof if I PR to mathlib.

[Alex J. Best]

Its for development

[Alex J. Best]

I can just do import tactic then when I PR to mathlib the linter will complain and I'll minimize the imports

[Yury G. Kudryashov]

Then we should rewrite the comment at the top of tactic.default.

[Yury G. Kudryashov]

Closed #10909

[Rob Lewis]

Alex J. Best said:

So I don't really see the point of this, omega is a useful tactic still, even if it won't be ported any time I get to an annoying a - 1 - b + 1 = a - b in nat type goals I hit it with omega, even if I have to make a different proof if I PR to mathlib.

There's 0 hope of porting current omega to Lean 4, any Lean 4 version will be a full reimplementation and I don't know if that will happen before d-day.

[Alex J. Best]

I understand that

[Alex J. Best]

I'm just saying for the purpose of working on Lean 3 its still a useful way of checking is my goal true, or getting to a sorry free proof. Much like tidy or something where in many cases you replace it by a better proof before PRing

[Rob Lewis]

Oh, sure. I didn't see #10909, agreed that isn't necessary