Zulip Chat Archive
Stream: triage
Topic: issue !4#9410: RewriteSearch.lean flaky tests?
Random Issue Bot (Jun 14 2024 at 14:10):
Today I chose issue 9410 for discussion!
RewriteSearch.lean flaky tests?
Created by @Mario Carneiro (@digama0) on 2024-01-03
Labels:
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jul 26 2024 at 14:09):
Today I chose issue 9410 for discussion!
RewriteSearch.lean flaky tests?
Created by @Mario Carneiro (@digama0) on 2024-01-03
Labels:
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Nov 12 2024 at 14:12):
Today I chose issue 9410 for discussion!
RewriteSearch.lean flaky tests?
Created by @Mario Carneiro (@digama0) on 2024-01-03
Labels:
Is this issue still relevant? Any recent updates? Anyone making progress?
Mario Carneiro (Nov 12 2024 at 14:27):
ping @Kim Morrison
Kim Morrison (Nov 14 2024 at 02:14):
Yes, I've been thinking about what to do with rw_search.
- rename it to
rw??, in the hope that someone starts using it :-) - see if anyone wants to adopt it and make it better
- failing to find evidence of either of the above, move it out of mathlib
Random Issue Bot (Dec 29 2024 at 14:12):
Today I chose issue 9410 for discussion!
RewriteSearch.lean flaky tests?
Created by @Mario Carneiro (@digama0) on 2024-01-03
Labels:
Is this issue still relevant? Any recent updates? Anyone making progress?
Johan Commelin (Jan 02 2025 at 10:53):
#11768 also introduces rw??
Last updated: May 02 2025 at 03:31 UTC