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, ...
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).
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.
In principle, the integration would not support renaming the topic of marking as resolved / unresolved.
But are you suggesting that we should prefer a stream?
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: Dec 01 2023 at 06:01 UTC