Théo Zimmermann (Jun 17 2020 at 11:56): Théo Zimmermann (Jun 17 2020 at 11:56):Hi @jco, you feel like the Discourse forum is dead? Can you share what makes you feel that way? If this is the case, this was certainly an unwanted consequence.
Théo Zimmermann (Jun 17 2020 at 11:57):@Cyril Cohen We might want to proceed to have Zulip notifications whenever there is a new topic on Discourse. And BTW, it might make sense to do the same for Stack Overflow and TCS Stack Exchange questions with the "coq" tag if such an integration exists.
jco (Jun 17 2020 at 11:58):Theo, apologies if I spoke out of turn. I did check the Discourse first, but looking under latest the last post is from 2 days ago (with some responses), the post before that is 5 days ago, then 6 days, (those have responses), but then there are a smattering of posts with no responses
jco (Jun 17 2020 at 11:58):so at a glance, it was hard to tell if it was dead or not. some posts have responses, some don't. velocity seemed low, wasn't sure if I'd be yelling into a void
jco (Jun 17 2020 at 12:01):integrating the various platforms seems like it would be pretty cool :)
Théo Zimmermann (Jun 17 2020 at 13:06):Thanks for the feedback.
Karl Palmskog (Jun 17 2020 at 13:13):I want to add that the material in Zulip is still firewalled to non-registered, which in some cases can be a genuine loss, e.g., the long thread on dependent pattern matching. Can one easily export certain conversations in some way?
Simon Hudon (Jun 17 2020 at 13:15):consider: https://zulipchat.com/help/export-your-organization
Simon Hudon (Jun 17 2020 at 13:15):this is what the Lean community does. (actually, it was implemented by @Rob Lewis from the Lean community)
Karl Palmskog (Jun 17 2020 at 13:17):we are aware of this (and regrettably don't have a corresponding setup on GitHub yet). A problem in my view is also that it doesn't make the material searchable beyond indexing by web spiders.
Théo Winterhalter (Jun 17 2020 at 13:19):For searchability and posterity I think StackOverflow is the best for now (at least in terms of what Google turns up when searching Coq).
Théo Zimmermann (Jun 17 2020 at 13:19):StackOverflow is only suited to Q&A, not to discussions.
Théo Zimmermann (Jun 17 2020 at 13:19):Discussions sometimes happen on SO in comments but they are rapidly showing their limits.
Karl Palmskog (Jun 17 2020 at 13:20):yes, I think they purposely make comments neigh-unreadable
Théo Zimmermann (Jun 17 2020 at 13:20):So while SO is indeed great for searchability and posterity of Q&A, that doesn't cover the whole use case.
Théo Zimmermann (Jun 17 2020 at 13:20):Karl Palmskog said:
yes, I think they purposely make comments neigh-unreadable
In fact, if you start a long discussion in comments, you have the platform suggesting you to move the discussion to a chat.
Théo Zimmermann (Jun 17 2020 at 13:22):Well, it makes total sense to me! It's just not what the platform is designed for.
Théo Zimmermann (Jun 17 2020 at 13:22):So SO is great but Discourse is also really important for long-term discoverability of discussions that do not fit the Q&A format.
Théo Zimmermann (Jun 17 2020 at 13:23):And Zulip allows a lot more interaction so the three use cases, while partly overlapping, are not exactly the same.
Anton Trunov (Jun 17 2020 at 13:24):Also, SO does not allow one to search in comments.
jco (Jun 17 2020 at 13:28):as a new user, I think my main concern was: "Where are the people?" Coq doesn't have a huge community, so I wanted to find it. This stuff can be lonely!
Rob Lewis (Jun 17 2020 at 13:30):Simon Hudon said:
consider: https://zulipchat.com/help/export-your-organization
This is not what the Lean community does (and not what I implemented). We use this, which builds an html archive that can be hosted, indexed, viewed anonymously, etc.
jco (Jun 17 2020 at 13:30):Having SO ping a stream here seems like a nice feature. And I mean, the conversations here could be exported to a special discourse forum periodically. I was on a discourse forum that did that -- in their case, they created discourse conversations for all of their old blog posts. you could def do that here, of course, you have to make sure people realize that everything they say in zulip (which is chat and thus feels ephemeral) will be backed up in such a way
Rob Lewis (Jun 17 2020 at 13:31):There are a bunch of bugs, some of which were introduced after I handed it over to the Zulip team. But it's more or less functional. It serves the purpose of making the chat indexable by search engines, which was my main goal.
Rob Lewis (Jun 17 2020 at 13:32):https://leanprover-community.github.io/archive/ is the archive in action.
jco (Jun 17 2020 at 13:33):nice! though if you do that, it's unclear what purpose discourse serves. zulip is threaded and, at least from my desktop, seems to allow longform conversation
Karl Palmskog (Jun 17 2020 at 13:33):jco said:
as a new user, I think my main concern was: "Where are the people?" Coq doesn't have a huge community, so I wanted to find it. This stuff can be lonely!
By proof assistant standards, the community is (very) large, but very distributed across different platforms and projects that don't have a ton of interaction.
Karl Palmskog (Jun 17 2020 at 13:35):Rob Lewis said:
https://leanprover-community.github.io/archive/ is the archive in action.
ah right, I was responding as if this was what Simon meant. I agree that spider indexing is a big step, but still far from ideal.
jco (Jun 17 2020 at 13:36):Karl Palmskog said:
jco said:
as a new user, I think my main concern was: "Where are the people?" Coq doesn't have a huge community, so I wanted to find it. This stuff can be lonely!
By proof assistant standards, the community is (very) large, but very distributed across different platforms and projects that don't have a ton of interaction.
Sure, fair enough. I just mean for someone who is not connected to the academic community, and is used to much larger communities (I know a lot of people in the scala community, for example). But fair enough. I think it's just about discoverability
jco (Jun 17 2020 at 13:38):But I googled coq, found inria, then found here, so it's not too bad!
Paolo Giarrusso (Jun 18 2020 at 21:44):Once the archive is added (which will take time but is probably needed anyway?) is it a problem if Discourse "dies"? Do other communities combine Zulip and Discourse? Unlike Gitter, Zulip seems to work well for both "IM" and as a forum :-)
Karl Palmskog (Jun 18 2020 at 22:00):there is no indication that there will be any (external) search for Zulip in the near future other than the frankly terrible web-crawled indexing by search engines after HTML export
Karl Palmskog (Jun 18 2020 at 22:02):for example, one can't even view all posts by a certain person. Hence, there are very strong reasons (in my opinion) to keep Discourse or something like it around for the foreseeable future
Enrico Tassi (Jun 19 2020 at 07:01):Are we archiving the zulip chat as plain HTML? There seem to be a zulip-archive out there, and I'm pretty sure standard search engines would provide decent search facilities on such an archive
Karl Palmskog (Jun 19 2020 at 08:25):@Enrico Tassi here is the archive for Lean's Zulip: https://leanprover-community.github.io/archive/
How would you find an exact list of all posts by (say) Sebastian Ullrich where he mentions Lean's kernel? Note that many/most HTML pages are huge, so pinpointing a specific page is often useless.
Rob Lewis (Jun 19 2020 at 08:59):The idea is that casual users won't be searching for something so specific. If they type something about Lean into Google, they appear on the crappy HTML archive, which lets them know that Zulip exists (and each post links to its corresponding Zulip post). If they want to do real search, they should log into Zulip and search here.
Of course it's not ideal that you have to log in to do a real search, a publicly visible/searchable Zulip channel would be better. But the Zulip org has been talking about that for years with no obvious progress so I'm not holding my breath.
Karl Palmskog (Jun 19 2020 at 09:07):@Rob Lewis then I think we agree both on the general Zulip situation and the strengths/limitations of the Zulip chat (and obviously I commend your work on getting HTML dumps). However, as a community grows, I think "laser-focused search" about previously discussed topics becomes important, in particular as reference points (I link a lot to Discourse threads here). For newbies, the Discourse feature which suggests similar posts as you are writing a new post is very nice.
Rob Lewis (Jun 19 2020 at 09:12):Sure, and ZUlip does most of that. You can link to individual posts and threads on Zulip, and the internal search is decent. The obvious downside is that you have to log in. You can also link to individual posts on the archive (click the timestamp). You can't easily get an archive link from native Zulip, which is annoying.
Rob Lewis (Jun 19 2020 at 09:13):It's definitely important to try and avoid "monster threads" on Zulip. We've been trying to kill our "noob questions" thread for a while because it's a black hole of information.
Rob Lewis (Jun 19 2020 at 09:15):IMO the worst thing to do for a small community is to spread discussion over lots of different forums. WHen some people are on the mailing list, some on Discord, some on StackOverflow, some here, then information becomes impossible to find.
Karl Palmskog (Jun 19 2020 at 09:15):login requirement would be a huge killer for us, e.g., posts on our Discourse have gone viral in the past
Rob Lewis (Jun 19 2020 at 09:15):This is obviously even more relevant for Lean than Coq since we have a smaller community. We've intentionally killed our mailing list.
Karl Palmskog (Jun 19 2020 at 09:17):I would also like the Coq-Club mailing list to be taken out of commission, but that's another battle
Enrico Tassi (Jun 19 2020 at 09:20):@Karl Palmskog If this is what you want as a search facility, then I agree with you that google is no SQL. I thought about search as I search the web for any technical problem with any piece of software and I don't care who answered or where.
Ralf Jung (Jul 05 2020 at 12:00):Paolo G. Giarrusso said:
Once the archive is added (which will take time but is probably needed anyway?) is it a problem if Discourse "dies"? Do other communities combine Zulip and Discourse? Unlike Gitter, Zulip seems to work well for both "IM" and as a forum :-)
Rust uses Zulip and discourse. But it's also a much bigger community.
Emilio Jesús Gallego Arias (Jul 05 2020 at 12:19):Zulip is pretty practical for example, for me to maintain my Dune topic
Last updated: Sep 28 2023 at 09:01 UTC