Zulip Chat Archive
Stream: triage
Topic: PR #18256: feat(group_theory/marking): Group markings
Random Issue Bot (Jun 19 2023 at 14:06):
Today I chose PR 18256 for discussion!
feat(group_theory/marking): Group markings
Created by @Yaël Dillies (@YaelDillies) on 2023-01-22
Labels: awaiting-author, t-algebra, modifies-synchronized-file
Is this PR still relevant? Any recent updates? Anyone making progress?
Yaël Dillies (Jun 19 2023 at 14:08):
Have been trying to work on it for several months. After 10-15min of editing, the file becomes terribly slow and restarting the server doesn't even help.
Scott Morrison (Jun 19 2023 at 21:46):
Maybe just restart it in lean4? Hopefully it's a largely independent set of mysterious slowdowns, and you might be lucky?
Eric Wieser (Jun 19 2023 at 22:22):
The change to the existing mathlib3 file could probably be merged safely if you want to split the PR, @Yaël Dillies
Yaël Dillies (Jun 19 2023 at 22:25):
In fact I could revert the PR to before @Sebastien Gouezel's suggestion and act on it once ported to Lean 4.
Yaël Dillies (Jun 19 2023 at 22:26):
The code compiled fine, it's just that the definition had no API (and writing the API is easy if you have a working infoview).
Random Issue Bot (Jul 28 2023 at 14:06):
Today I chose PR 18256 for discussion!
feat(group_theory/marking): Group markings
Created by @Yaël Dillies (@YaelDillies) on 2023-01-22
Labels: awaiting-author, t-algebra, modifies-synchronized-file, too-late
Is this PR still relevant? Any recent updates? Anyone making progress?
Last updated: Dec 20 2023 at 11:08 UTC