Zulip Chat Archive
Stream: triage
Topic: issue #1484: unexpected failures with `omega`
Random Issue Bot (Oct 13 2021 at 14:18):
Today I chose issue 1484 for discussion!
unexpected failures with omega
Created by @Rob Lewis (@robertylewis) on 2019-09-24
Labels: bug, meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Scott Morrison (Oct 13 2021 at 20:27):
Random Issue Bot said:
unexpected failures with
omega
Created by Rob Lewis (@robertylewis) on 2019-09-24
Labels: bug, metaIs this issue still relevant? Any recent updates? Anyone making progress?
Could we just mark this as wontfix and close? omega is not going anywhere, and will need a complete reimplementation for Lean4.
Rob Lewis (Oct 13 2021 at 21:16):
Happy to mark it wontfix, but I think it's fine to keep it open, only as a sign that these issues are known
Rob Lewis (Oct 13 2021 at 21:18):
I tried to use omega in class, like, an hour ago and got embarrassed when it failed. Serves me right though
Kevin Buzzard (Oct 13 2021 at 22:11):
Rehearsal is sometimes key ;-) I spent the tube journey into work today going through a proof and finding out which route made it look the slickest, then just unrolled it in front of 30 students in a kind of "look it's so easy and intuitive" way :-)
Patrick Massot (Oct 13 2021 at 22:13):
It also works with traditional lectures. Tomorrow morning I need to prove characterization and existence of free groups. This is definitely worthy of rehearsal.
Random Issue Bot (Jan 03 2022 at 14:17):
Today I chose issue 1484 for discussion!
unexpected failures with omega
Created by @Rob Lewis (@robertylewis) on 2019-09-24
Labels: bug, wontfix, meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Feb 19 2022 at 14:12):
Today I chose issue 1484 for discussion!
unexpected failures with omega
Created by @Rob Lewis (@robertylewis) on 2019-09-24
Labels: bug, wontfix, meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Feb 02 2023 at 14:09):
Today I chose issue 1484 for discussion!
unexpected failures with omega
Created by @Rob Lewis (@robertylewis) on 2019-09-24
Labels: bug, wontfix, t-meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jun 16 2023 at 14:07):
Today I chose issue 1484 for discussion!
unexpected failures with omega
Created by @Rob Lewis (@robertylewis) on 2019-09-24
Labels: bug, wontfix, t-meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Yury G. Kudryashov (Jun 16 2023 at 14:53):
Should we close it as "wontfix"? AFAIR, we removed all uses of omega in mathlib.
Last updated: Dec 20 2023 at 11:08 UTC