Stefan Haan (Nov 18 2022 at 07:47): Stefan Haan (Nov 18 2022 at 07:47):Would it be possible to mirror the #coq IRC channel on libera.chat to Zulip? This would make it easier to connect to the larger Coq community using established internet standards like IRC, XMPP, ...
Théo Zimmermann (Nov 18 2022 at 09:09):It looks like some integration like this is possible https://coq.zulipchat.com/integrations/doc/irc, but it requires some bridge software to run. I do not think that we have an appropriate place to run this software for the Coq team, but it would be fine by me if someone volunteers to run it on their personal server. In principle, bots can also be created by non-admin users (let me know if that's not the case). The IRC messages could reach a dedicated stream (in which case, people need to subscribe to see the messages) or just an IRC topic in the #Coq users stream (it's easy to mute topics for those that do not want to follow the messages).
Théo Winterhalter (Nov 18 2022 at 14:07):Note that it's easy to mute but it's also easy to unmute it for everyone by renaming a thread or marking as resolved / unresolved.
Théo Zimmermann (Nov 18 2022 at 14:34):In principle, the integration would not support renaming the topic of marking as resolved / unresolved.
Théo Zimmermann (Nov 18 2022 at 14:35):But are you suggesting that we should prefer a stream?
Théo Winterhalter (Nov 18 2022 at 14:36):Oh you're right. So no not necessarily. But I would probably end up muting such a thread / stream precisely because it is unstructured (moving from Gitter was a very good idea in my mind).
Last updated: Jun 10 2023 at 06:31 UTC