Anton Trunov (Nov 20 2021 at 08:41): Anton Trunov (Nov 20 2021 at 08:41):A proposal by Andrej Bauer: http://math.andrej.com/2021/11/20/proof-assistants-stackexchange-site. I hope this is not duplicate here
Anton Trunov (Nov 21 2021 at 12:10):The proposal successfully reached the commitment stage, let's help the proposal reach the beta stage!
Théo Zimmermann (Nov 23 2021 at 14:00):The proposal has completed the commitment stage. This means that the site will go into private beta soon. People can still commit to be invited to the private beta.
Théo Zimmermann (Nov 23 2021 at 14:06):During the private beta, it would make sense to try to migrate some Frequently Asked Questions, both from https://github.com/coq/coq/wiki/The-Coq-FAQ and that people have encountered here in Zulip or in Discourse / Coq-Club. As I wrote in a much upvoted comment in a previous discussion, people can self-answer their questions on Stack Exchange, so this means that Zulip users answering questions and noticing that some of them are frequently asked can create a corresponding (canonical) question / answer on Stack Exchange.
Karl Palmskog (Nov 23 2021 at 14:22):since Stack Exchange considers new users pariah, I would recommend that people with a lot of SE reputation to do all this work (otherwise I think it will get stuck in the various pariah filters they have)
Théo Zimmermann (Nov 23 2021 at 14:43):Stack Overflow works like you say and is pretty unwelcoming. But the good thing of this being a new site is that it will have much fewer barriers of entry and basically everyone will start on equal footing (long time SO users will have to rebuild their "reputation" on this new site).
Karl Palmskog (Nov 23 2021 at 14:45):but it looked to me like reputation from other SE carries over? Otherwise, why does it rank commits by reputation?
Théo Winterhalter (Nov 23 2021 at 14:46):Usually when you join a new SE site, you only get a boost of 100 points for being reputable on other sites.
Théo Zimmermann (Nov 23 2021 at 14:50):Indeed, @Théo Winterhalter is correct. I should have put "virtually" in front of "equal footing" for this reason.
Karl Palmskog (Nov 23 2021 at 14:51):sigh, it seems people with no rep don't even show up in the committed list... Apparently some artifact due to account email verification.
Karl Palmskog (Nov 23 2021 at 14:59):"Academic or Research-Level Student" seems a bit over-used, as was already pointed out by Andrej: https://twitter.com/andrejbauer/status/1462337362843914240
Ha ha, @pigworker marked himself as "Academic or Research-Level Student". What potions has he been drinking? And I bet he's lurking somewhere around here.
- Andrej Bauer (@andrejbauer) Théo Zimmermann (Nov 23 2021 at 15:01):I think that many of us interpreted this as "Academic OR (Research-Level Student)" and not as "(Academic or Research-Level) Student". English. Sigh!
Karl Palmskog (Nov 23 2021 at 15:03):yes, I also think that's how some non-native speakers may have read it. And then others will interpret it as false modesty... sigh indeed
Théo Zimmermann (Nov 23 2021 at 15:06):But isn't Conor McBride (a.k.a. "pig worker") a native English speaker? Do you think that it's really false modesty on his part or is it proof that this phrase has several interpretations, including for native English speakers?
Karl Palmskog (Nov 23 2021 at 15:07):he is a native speaker and he was likely trolling a bit as Andrej says. So probably no misunderstanding on his part. He may even have been prompted to select it due to the ambiguity.
Théo Winterhalter (Nov 23 2021 at 15:18):On the other hand I was afraid of appearing as pompous for selecting expert because I understood the item as "student".
Karl Palmskog (Nov 23 2021 at 15:27):anyway, I'm looking forward to the fair and balanced answers on subject reduction and the like...
As I wrote in my note, the main advantage of SE questions is their insanely high ranking in search engines. I don't really get how it can be a place where people actually hang around (other than for winning the reputation rat race)
Théo Winterhalter (Nov 23 2021 at 15:50):I mean, if I'm not the person who asked the questions, then SE questions is the only place I know where I can easily go and check out the answer that worked. If I wanted to race for reputation, I probably wouldn't hang on the Coq SE though. :)
Karl Palmskog (Nov 23 2021 at 16:57):the point is that (in my opinion), nobody should "go and check" SE. You should use your favorite search engine, find the SE answer, read it, then get out...
Karl Palmskog (Nov 23 2021 at 16:57):I wouldn't be surprised if the company behind SE has some special deal with Google et al.
Théo Winterhalter (Nov 23 2021 at 16:58):I check it to answer questions.
Karl Palmskog (Nov 23 2021 at 16:59):but why do that, if you're not into the reputation stuff?
Théo Zimmermann (Nov 23 2021 at 16:59):To help others?
Théo Zimmermann (Nov 23 2021 at 16:59):What is wrong with willing to help?
Karl Palmskog (Nov 23 2021 at 17:00):I think Théo Zimmermann suggested the best approach: instead of waiting for people to ask SE questions, pre-ask and pre-answer (since we already know most of the time what questions are and will be)
Karl Palmskog (Nov 23 2021 at 17:00):I don't mind people helping, but I don't think SE is the best way to do that
Théo Zimmermann (Nov 23 2021 at 17:03):Karl Palmskog said:
I don't mind people helping, but I don't think SE is the best way to do that
It depends on whom you want to help and in what context. The principle of SE is that questions (not just answers) should be of high quality. Unfortunately, the reputation game isn't working so well since people will rush to answer basic questions to get the most rep points. But I think that in the context of a smaller community, it can work better than it does on SO.
Ana de Almeida Borges (Nov 23 2021 at 17:04):Karl Palmskog said:
I don't mind people helping, but I don't think SE is the best way to do that
What do you think the best way to help?
Théo Zimmermann (Nov 23 2021 at 17:05):BTW, we already have an active SE integration here in the Coq Zulip for every question tagged Coq. I expect it should work fine for the new site once we are out of private beta.
Karl Palmskog (Nov 23 2021 at 17:05):as I implied above, I think the best way to help is to curate good questions / answers via other forums, then self-ask, self-answer on SE to get their insane search engine priority
Théo Zimmermann (Nov 23 2021 at 17:07):I agree, though this is not conflicting with answering good questions with good answers when they happen to be posted.
Théo Zimmermann (Nov 23 2021 at 17:08):And with the Zulip integration, following the questions being asked shouldn't be too difficult.
Karl Palmskog (Nov 23 2021 at 17:08):I see your point of view, but I still worry about flood of basic repeated questions (crowd detection of duplicates is hard) and reputation mining
Théo Zimmermann (Nov 23 2021 at 17:10):Ah OK, this is where our expectations for the future of this site differ. I expect a bump in the number of questions per day, but probably not to the point that it will become a flood. But if it does, then this will need another management strategy.
Théo Zimmermann (Nov 23 2021 at 17:11):Anyway, the site will be what we do of it. If we see people asking very basic and repeated questions, we can decide to redirect them to Zulip chats for more interactive help sessions, while focusing on answering the good questions that will help a lot of people in the future.
Karl Palmskog (Nov 23 2021 at 17:12):I also hope that longer answers will be tolerated, I've seen quite lot of shooting down exposition on SE (in fact this is encouraged by winner-takes-all reputation points)
Théo Zimmermann (Nov 23 2021 at 17:16):My experience is with answering questions on low-activity sites or tags and in this case, there is not such a rush to be the first to answer, so long answers are well-received and encouraged. In fact, even if you post an answer after one has been marked as accepted, the asker can still change the accepted answer, or the new answer can still receive many upvotes.
Karl Palmskog (Nov 23 2021 at 17:19):just to clarify if someone still wonders, I meant
why do that
in the sense of
why pick that particular option/method of helping people, among all the ones available
which I think should be reasonable to ask, even if we assume "helping is good" in general
Karl Palmskog (Nov 23 2021 at 17:24):hmm, when the PA SE goes into beta, we may even consider having a Zulip stream dedicated to it, or what do you think @Théo Zimmermann? Could be a good way of coordinating good answers (and questions).
Tim Carstens (Nov 23 2021 at 17:26):I'm optimistic about this experiment. Stack Overflow's impact & utility for working engineers cannot be denied. (Other platforms surely exist; I'd be excited to see proposals for their use as well.)
The creation of a new subsite will create new ways for people to participate in the community. IMHO the "worst case" is that the subsite winds up consisting of the same people who are already on all of the mailing lists and Zulip chats. Or another "worst case:" the site never gets enough traffic to move out of Beta, or is eventually deleted due to inactivity. To me, the real measure of success will be whether or not it grows & scales.
Théo Zimmermann (Nov 23 2021 at 17:27):Karl Palmskog said:
hmm, when the PA SE goes into beta, we may even consider having a stream dedicated to it, or what do you think Théo Zimmermann? Could be a good way of coordinating good answers (and questions).
That's a terrific idea (if enough people are willing to participate in this coordination effort). Please upvote Karl's post if you'd be interested in joining such a stream.
Karl Palmskog (Nov 23 2021 at 17:27):the main reason to coordinate I see is that we don't want duplicate effort, e.g., both Théo Z. and I working to answer some Coq proof engineering question in parallel
Tim Carstens (Nov 23 2021 at 17:29):It would be great if there was enough sustained interest that duplicate effort winds up being a problem :sweat_smile: I like your proposal because I'm worried that questions will go unanswered after the initial excitement wears off! (Upvoted)
Théo Zimmermann (Nov 23 2021 at 17:31):@Tim Carstens Look at this: https://stackexchange.com/filters/299857/questions-tagged-coq-on-stackexchange-sites. Questions about Coq on SE sites already get answered as of today. I don't expect this will change, except if we get too many questions for what experts are ready to answer.
Karl Palmskog (Nov 23 2021 at 17:32):I also saw that to get out of beta, there has to be sustained activity, they even give beta stacks a "grade" in each activity measure: https://area51.stackexchange.com/proposals/125174/cardano
5.9 questions per day: Okay – 10 questions per day on average is a healthy beta, 5 questions or fewer per day needs some work. A healthy site generates lots of good content to make sure users keep coming back.
Théo Zimmermann (Nov 23 2021 at 17:33):These measures are outdated according to a response on the Proof Assistants proposal. Let me find the link.
Théo Zimmermann (Nov 23 2021 at 17:33): Li-yao (Nov 23 2021 at 17:33):The "pre-ask question" model only works for question of a rather general scope. There are techniques that really only make sense in the context of concrete examples, which are best illustrated when askers provide the examples that are relevant to them, when they don't have the expertise or the time to read CPDT and figure out what is relevant and how to apply it.
Tim Carstens (Nov 23 2021 at 17:33):@Théo Zimmermann Excellent point :+1:
Karl Palmskog (Nov 23 2021 at 17:35):@Li-yao but we do have many examples across Coq-Club, Disourse, Zulip, etc. I agree about using examples, but I think there are low-level specific questions that are common also.
Théo Winterhalter (Nov 23 2021 at 18:00):Do you think that simply answering people's question is counter-productive? I think that even ill-asked questions are of value, because they might reflect how others might think of a problem the way experts don't.
When on the side of finding a solution to my problem, sometimes, finding someone else's struggle helped understanding what my own problem was.
Karl Palmskog (Nov 23 2021 at 18:35):I think it's obvious that many questions (on SE and elsewhere) are very poorly formulated, such that they are nearly unsalvageable. In particular, it's often clear the user has made little effort to produce a small example that reproduces or illustrates their problem. We are as a community mainly interested in the collection of quality questions & answers, not that each user gets their personal question answered.
People who answer questions have limited time which means there can be a substantial opportunity cost to answer bad questions for the community.
Li-yao (Nov 23 2021 at 18:40):Even with a database of quality Q&A I wouldn't know how to search it without already knowing the answer.
Karl Palmskog (Nov 23 2021 at 18:41):search engines are pretty good at setting that up (i.e., good at searching SE), and I think there are probably code-based interfaces to the SE API based on learning and so on. Could be worth looking into, but I still think the quality Q&A is the main thing.
Stefan Monnier (Nov 23 2021 at 19:49):While I think that technically SX has managed to be very useful for a lot of technical questions (BTW, I access it via DuckDuckGo and they seem to have just as much of a deal with them as with Google ;-), I'm worried about the fact that those questions&answers are locked in some company's servers. That's why I largely stopped contributing to it. If only we could archive the data elsewhere.
Karl Palmskog (Nov 23 2021 at 19:59):they have an interface/API to retrieve both questions and answers, and the license is CC-BY-something. In my opinion a "Coq Stack Exchange Working Group" could make sure all Coq questions and answers are regularly backed up (but preferably only the quality ones).
Théo Zimmermann (Nov 23 2021 at 20:37):Indeed, CC BY-SA version 2.5, 3.0 or 4.0 depending on the date of the latest revision (and the UI and the API provide this information) as was explained in a post you shared earlier in a previous discussion (https://meta.stackexchange.com/questions/347758/creative-commons-licensing-ui-and-data-updates/).
Stefan Monnier (Nov 23 2021 at 21:02):they have an interface/API to retrieve both questions and answers
So I heard but I still haven't seen a tool that performs actual usable backups (e.g. that can produce some kind of read-only barebones mirror). I haven't actively looked for it, admittedly.
Paolo Giarrusso (Nov 25 2021 at 01:06):@Stefan Monnier Not exactly what you're asking, but such "backups" are clearly done in practice (at least for StackOverflow). That's visible when googling a question and seeing Google find an SO clone.
Paolo Giarrusso (Nov 25 2021 at 01:06):(which, BTW, seems unlikely to ever happen if SX had a special deal!)
Paolo Giarrusso (Nov 25 2021 at 01:07):there are multiple servers with snapshots of SO questions, thanks to the CC-BY license.
Paolo Giarrusso (Nov 25 2021 at 01:08):those are presumably made by less reputable companies, but it seems to confirm backups are essentially possible.
Eric Taucher (Nov 25 2021 at 07:55):A StackExchange chat room for the ProofAssistants proposal has been setup: https://chat.stackexchange.com/rooms/131732/proofassistants-temp
Théo Zimmermann (Nov 25 2021 at 11:00):The most useful info I could get so far from this chat room is an estimation that the private beta could start on the 7th or the 14th of December and the public beta should happen 3 weeks later, but probably after Christmas.
Eric Taucher (Dec 09 2021 at 12:15):Proof Assistants private beta launch will take place in January 2022
Since we want all proposals to have the best chances of thriving as possible, the Community Team has decided to postpone this proposal's launch into private beta to January 2022, in an attempt to minimize the impact of the upcoming end-of-year holidays in the site's chances of success.
Additionally, the proposal sped through its definition and commitment phases, which we believe hasn't allowed for some discussions that usually take place during those phases — such as deciding on a name and URL for the site — to come to a consensus. As such, we invite those of you who've committed to this proposal to try to have those conversations between now and the first couple of weeks of January 2022. At that time the Community Team will help y'all tie whatever loose ends need to be tied, and prepare the site for launch into private beta.
Théo Zimmermann (Dec 09 2021 at 13:25):No better way to kill momentum, but go figure...
Last updated: Jun 01 2023 at 12:01 UTC