Zulip Chat Archive
Stream: triage
Topic: issue #1465: Probably `setup_tactic_parser` can be integr...
Random Issue Bot (Feb 05 2021 at 14:20):
Today I chose issue 1465 for discussion!
Probably setup_tactic_parser can be integrated to use open_locale instead
Created by @Keeley Hoek (@khoek) on 2019-09-20
Labels: feature-request, meta
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jan 23 2022 at 14:16):
Today I chose issue 1465 for discussion!
Probably setup_tactic_parser can be integrated to use open_locale instead
Created by @Keeley Hoek (@khoek) on 2019-09-20
Labels: meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Mar 13 2022 at 14:12):
Today I chose issue 1465 for discussion!
Probably setup_tactic_parser can be integrated to use open_locale instead
Created by @Keeley Hoek (@khoek) on 2019-09-20
Labels: meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Apr 05 2022 at 14:14):
Today I chose issue 1465 for discussion!
Probably setup_tactic_parser can be integrated to use open_locale instead
Created by @Keeley Hoek (@khoek) on 2019-09-20
Labels: meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (May 11 2022 at 14:21):
Today I chose issue 1465 for discussion!
Probably setup_tactic_parser can be integrated to use open_locale instead
Created by @Keeley Hoek (@khoek) on 2019-09-20
Labels: meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Oct 07 2022 at 14:36):
Today I chose issue 1465 for discussion!
Probably setup_tactic_parser can be integrated to use open_locale instead
Created by @Keeley Hoek (@khoek) on 2019-09-20
Labels: t-meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Dec 07 2022 at 14:09):
Today I chose issue 1465 for discussion!
Probably setup_tactic_parser can be integrated to use open_locale instead
Created by @Keeley Hoek (@khoek) on 2019-09-20
Labels: t-meta, feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Johan Commelin (Dec 07 2022 at 14:19):
If we migrate to Lean 4, is this still relevant?
Mario Carneiro (Dec 07 2022 at 14:36):
Presumably quite a lot of issues won't be relevant
Mario Carneiro (Dec 07 2022 at 14:36):
we will need to go over them afresh
Johan Commelin (Dec 07 2022 at 14:41):
This bot allows us to reconsider one issue per day (-;
Scott Morrison (Dec 07 2022 at 21:57):
Could we just turn off the triage bot for mathlib3, and switch it over to mathlib4?
Scott Morrison (Dec 07 2022 at 21:58):
It's not like it is generating much response lately.
Yaël Dillies (Dec 07 2022 at 21:58):
I have been fixing quite a few of my PRs because of it, actually.
Bryan Gin-ge Chen (Dec 07 2022 at 21:59):
If / when we want to switch, here's the PR: https://github.com/leanprover-community/azure-scripts/pull/14
Eric Wieser (Dec 07 2022 at 22:04):
@Yaël Dillies: due to the PR bot, or the issue bot?
Yaël Dillies (Dec 07 2022 at 22:04):
PR bot
Last updated: Dec 20 2023 at 11:08 UTC