Théo Zimmermann (Feb 15 2022 at 07:59): Théo Zimmermann (Feb 15 2022 at 07:59):In https://coq.zulipchat.com/#narrow/stream/237655-Miscellaneous/topic/Proof.20Assistant.20StackExchange.20Proposal, @Karl Palmskog had proposed to create a stream dedicated to coordination on posting good quality questions / answers to the upcoming Proof Assistants Stack Exchange. This site is now in private beta https://area51.stackexchange.com/proposals/126242/proof-assistants, and it has received so far only 8 Coq questions (compare this to 8 Isabelle questions, 9 Agda questions and 23 Lean questions). These numbers could be much improved to better reflect the liveness of our community, in particular by doing what we had discussed, i.e., recording good FAQ questions on this Stack Exchange (one can even post the question and the answer themselves if they wish). Before acting on Karl's proposal and creating such a coordination stream, I figured that we could have a go at this as part of the Hackathon (with people who are registered for the private beta). (OTOH, the intersection between the people registered to the Stack Exchange site and to the Hackathon might be too small for this to work out...) WDYT?
Théo Zimmermann (Feb 15 2022 at 08:20):Beyond Coq questions (or their lack thereof), there are several generic questions for which answers are available for several proof assistants but not for Coq. See in particular:
Théo Zimmermann (Feb 15 2022 at 09:08):This one question might also lack complete answers for Coq: https://proofassistants.stackexchange.com/questions/74/proof-assistants-with-support-for-creating-executable-software-artifacts
Ana de Almeida Borges (Feb 15 2022 at 09:15):One thing that I see happen with SE is that there are many common answers for what on the surface look like different (and not necessarily generalizable) questions.
Ana de Almeida Borges (Feb 15 2022 at 09:15):Now that I think about it, this probably means it would be useful to have a page listing common troubleshooting instructions. Is there such a thing?
Théo Zimmermann (Feb 15 2022 at 09:19):I don't think it exists, no.
Ana de Almeida Borges (Feb 15 2022 at 09:23):Anyway, somewhat coordinating this seems like a good idea. I'm part of the private beta, maybe we can try to find out who else is too.
Cyril Cohen (Feb 15 2022 at 09:24):I'm also on the private beta, but I'm a shy user of the stackexchange network :sweat_smile:
Ana de Almeida Borges (Feb 15 2022 at 09:31):I guess the idea of this new SE is that there can be 1) questions whose answers are independent of the proof assistant, 2) questions that make sense to ask for any proof assistant bue have different answers for each and 3) questions that make sense only for a specific proof assistant.
Théo Zimmermann (Feb 15 2022 at 09:31):I think the main thing we need right now is more Coq questions, in particular expert questions.
Ana de Almeida Borges (Feb 15 2022 at 09:32):So questions that fall under 3)
Théo Zimmermann (Feb 15 2022 at 09:32):2) questions that make sense to ask for any proof assistant bue have different answers for each
I think this one category is really an artifact from the beginning but should not be so common in the long-term.
Théo Zimmermann (Feb 15 2022 at 09:32):Most of such questions that were asked were really being too vague and not specific enough.
Pierre-Marie Pédrot (Feb 15 2022 at 09:33):I think I am too expert to have questions about Coq unfortunately... Or that's about really horrible details nobody wants to hear about, including myself. Is there anything to be done?
Ana de Almeida Borges (Feb 15 2022 at 09:33):Yes, I'm also confused by what is meant by "expert questions".
Théo Zimmermann (Feb 15 2022 at 09:34):My point is that we should ask questions that we already know the answer of.
Théo Zimmermann (Feb 15 2022 at 09:34):But that come up often and are interesting.
Pierre-Marie Pédrot (Feb 15 2022 at 09:34):I see two typical questions that keep coming back on various channels but I don't know whether it makes sense to ask them in all generality.
Théo Zimmermann (Feb 15 2022 at 09:35):I meant "expert" just to say that they should be above the very basics of "How do I install Coq" and "How do I import Arith".
Pierre-Marie Pédrot (Feb 15 2022 at 09:35):That's 1. writing match annotation for dependent typing and 2. the evergreen nested fixpoints trick
Théo Zimmermann (Feb 15 2022 at 09:35):More like "How do I set modes for typeclasses" (that kind of stuff). And yes, your suggests are great PMP.
Ana de Almeida Borges (Feb 15 2022 at 09:35):Théo Zimmermann said:
I meant "expert" just to say that they should be above the very basics of "How do I install Coq" and "How do I import Arith".
Is there any reason why those shouldn't be there anyway?
Théo Zimmermann (Feb 15 2022 at 09:36):No reason to exclude them Ana. It's just that this site won't need us for these questions to eventually find their way.
Théo Zimmermann (Feb 15 2022 at 09:36):Whereas putting more advanced questions about Coq right now will help people understand the kind of (advanced) things they can ask and hope to get answers to.
Ana de Almeida Borges (Feb 15 2022 at 09:39):Some frequent answers I give and will have to think how to come up with good questions for: 1. Coq can't unify those two seemingly equal terms because there are hidden coercions; 2. You can't apply that lemma because you are confused about the associativity of the notations and it doesn't actually match. 3. The lemma you are looking for can be found by being smarter about how you Search
Théo Zimmermann (Feb 15 2022 at 09:41):I guess the best way for this kind of questions is to use a specific example in the question, and try to make the answer as general as possible.
Karl Palmskog (Feb 15 2022 at 10:02):"expert questions" might be more accurately "facts known to experts", i.e., take something that requires deep understanding about Coq and post it in question-answer form of reasonable size.
Théo Zimmermann (Feb 15 2022 at 10:07):Yes, and do not hesitate to only post the question if you know the answer but only have time or energy to write the question. This will already be a useful contribution.
Karl Palmskog (Feb 15 2022 at 10:32):one example of a question that arguably needs expert summary: "What is the state of [support for] coinductive types and coinductive reasoning in Coq?"
Karl Palmskog (Feb 15 2022 at 10:40):@Pierre-Marie Pédrot if I ask the question, could you say something about your current PR and view of subject reduction? From what I've seen, Gimenez was aware of the tradeoff, so it's surprising to me that everyone was surprised and went all in on primitive projections.
Karl Palmskog (Feb 15 2022 at 11:18): Tomás Díaz (Feb 15 2022 at 12:48):I'm a bit confused with the types of questions "possible" (not that I have any rn). Should they be more theoretical? Can they be more practical (like many of the ones we see here in the zulip stream), e.g. "I'm failing to prove this in Coq, how do I XXX?"? Should these latter go in a more traditional "SE" stack? etc.
Karl Palmskog (Feb 15 2022 at 12:49):my understanding is that both "high-level" philosophical questions and "how do I do X" are welcome. But for Coq, we are here (in this topic on the Zulip) more interested in getting the high-level questions out there and answered. People will come along and ask "how do I do X" anyway.
Karl Palmskog (Feb 15 2022 at 12:52):for example, just asking an intelligible question about the guard condition used by Coq arguably takes an understanding of the scientific literature. People generally don't just show up and ask, "wouldn't the following guard condition solve problem X". Yet, people reading the Stack Exchange can benefit from seeing the question, and it can become a reference people point to.
Karl Palmskog (Feb 15 2022 at 12:55):(I found PMP's old slides on coinduction at least: https://www.pédrot.fr/slides/rapido-06-15.pdf)
Théo Zimmermann (Feb 15 2022 at 13:13):To add to Karl's answer: Obviously learners are welcome to ask any question that they stumble upon while learning Coq. What experts can do is to try to use their experience of answering similar kind of questions to try to make good FAQ that they can point to in the future.
Théo Zimmermann (Feb 15 2022 at 13:15):Also: regarding the Proof Assistants SE vs others SE (such as Stack Overflow), I think we can expect that most questions on proof assistants should eventually find their home in the Proof Assistants site, although Coq questions on other sites will never be closed as off-topic just because a new Proof Assistants site exists (and thus we can expect to continue seeing some on Stack Overflow).
Pierre-Marie Pédrot (Feb 15 2022 at 13:45):@Karl Palmskog I've written a detailed answer
Karl Palmskog (Feb 15 2022 at 13:46):thanks, that is exactly the kind of answer I think we can point to when people ask about coinduction (or other advanced topic)
Jason Gross (Feb 15 2022 at 15:32):There is also my answer to https://proofassistants.stackexchange.com/a/461/129 which leaves a question for those more knowledgeable than I:
The firstorder tactic in Coq is an "experimental extension of tauto to first-order reasoning." The tauto tactic "implements a decision procedure for intuitionistic propositional calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff [Dyc92]". Perhaps one of the Coq developers can speak to the theory behind firstorder.
Jason Gross (Feb 15 2022 at 16:06):@Pierre-Marie Pédrot If you have the time and inclination, do you want to dump all of your knowledge about Coq performance into an answer to https://proofassistants.stackexchange.com/questions/589/what-is-known-about-performance-bottlenecks-in-proof-assistants ?
Pierre-Marie Pédrot (Feb 15 2022 at 16:11):pfout, that's a vast, almost bottomless topic
Théo Zimmermann (Feb 15 2022 at 16:50):Some people seem to dislike people self-answering: https://proofassistants.meta.stackexchange.com/questions/33/policy-on-self-answers
I'm not sure how this discussion will be settled, but in any case, the strategy where one person spends time working on a good question and one person spends time working on a good answer (even if there was some coordination) might be better then...
Karl Palmskog (Feb 15 2022 at 16:53):yeah if we work through the Zulip, we can easily avoid this, people can just outline questions and answers and different people post
Théo Zimmermann (Feb 17 2022 at 17:25):There's an unanswered question about Proof General here: https://proofassistants.stackexchange.com/questions/636/how-do-i-turn-off-the-aggressive-auto-indent-in-proof-general-coq
Ana de Almeida Borges (Feb 17 2022 at 17:37):Nice, I also want to know the answer to that question! For now I have added my partial solution.
Karl Palmskog (Feb 21 2022 at 13:08):@Théo Zimmermann so what do we do with this topic now? Should it be a running topic in the #Coq users stream?
Karl Palmskog (Feb 21 2022 at 13:09):(ideally we'd like to have an integration that posts questions with the tag coq in the topic)
Théo Zimmermann (Feb 21 2022 at 13:16):There's already an integration that posts all the questions on Stack Exchange with the tag coq in https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/New.20Stack.20Exchange.20question. It will likely pick up the Proof Assistants coq questions as soon as the site goes in public beta.
Théo Zimmermann (Feb 21 2022 at 13:16):As for where we should coordinate now, I have no idea if that should be a running topic in #Coq users or a dedicated and separate stream.
Karl Palmskog (Feb 21 2022 at 14:07):I propose as a default that we move the topic to users.
Notification Bot (Feb 21 2022 at 14:08):This topic was moved here from #Coq Hackathon and Working Group, Winter 2022 > Proof Assistants Stack Exchange coordination by Karl Palmskog.
Karl Palmskog (Feb 21 2022 at 14:08):if there is a lot of activity here (not overwhelming so far), I think we create a new stream
Karl Palmskog (Feb 21 2022 at 14:09):for what it's worth, I have on my todo to summarize incremental compilation/checking in Coq
Karl Palmskog (Feb 21 2022 at 14:10):we also wait (possibly forever) for PMP to produce a tome of knowledge about proof assistant performance bottlenecks
Pierre-Marie Pédrot (Feb 21 2022 at 14:25):I don't think that the SO format is very good for the performance issue discussion
Karl Palmskog (Feb 21 2022 at 14:26):I agree in general terms. It's better for low-level performance questions like: "what is faster in practice in a toy proof assistant, pure de Bruijn variable substitution or locally nameless?"
Pierre-Marie Pédrot (Feb 21 2022 at 14:29):The answer for that one is probably YMMV and thus falls in the "opinion" tarpit
Karl Palmskog (Feb 21 2022 at 14:29):well, in case it varies, one can at least sometimes say what it varies with...
Karl Palmskog (Mar 23 2022 at 10:23):I saw this question about the architecture of the four color theorem Coq proof on StackExchange: https://proofassistants.stackexchange.com/questions/1105/how-does-the-formal-proof-of-the-four-color-theorem-work
I made a comment linking to the fourcolor repo in Coq-community, but I don't have enough insight to give a good answer. Highlighting it here in hopes that someone can confirm/deny what the question-asker says.
Théo Zimmermann (May 13 2022 at 16:39):FTR, there is a question on bidi type checking that was left unanswered for some weeks and has now a bounty on it: https://proofassistants.stackexchange.com/questions/1343/how-do-coqs-bidirectionality-hints-affect-type-checking
Any expert that could answer?
Ana de Almeida Borges (Jun 09 2022 at 10:15):Some questions do not have the coq tag but are still relevant for the Coq community, both in the sense of being interesting, and in the sense of some of us being able to answer. These are mostly theoretical questions, or questions asking for comparisons between several different proof assistants. I only see them when I visit a coq-tagged question and then end up browsing the website.
What are your opinions on creating a zulip bot / stream that notifies us of more theoretical tags (such as inductive-type, type-theory, implementation, reference-request, etc)? It could in principle be done such that interested people could subscribe and everyone else could ignore it. Or is this just my preference and I should find a different way to get notified?
Théo Zimmermann (Jun 09 2022 at 10:22):Currently, the bot reports on every new question with tag coq on any Stack Exchange website (thus we get those coming from both Proof Assistants SE and Stack Overflow). But given the low level of activity on Proof Assistants SE (1.6 question / day), we could consider having a bot that just posts about every question on this site. The only drawback would be that we would double-post any Proof Assistants SE questions about Coq. That being said, we should probably not post these questions to the #Coq users stream. Maybe one solution to avoid spamming by default would be to create a dedicated stream for Stack Exchange.
Ana de Almeida Borges (Jun 09 2022 at 10:35):Would it possible to have the bot report on every question except the ones tagged coq?
Ana de Almeida Borges (Jun 09 2022 at 10:35):Creating a new stream sounds reasonable
Théo Zimmermann (Jun 09 2022 at 11:42):Yes, we can do any kind of filtering that RSS feeds on Stack Exchange allow us to do. The Zulip bot relies on the RSS feed.
Meven Lennon-Bertrand (Jun 10 2022 at 09:30):Having a stream dedicated to SE questions sounds like a good idea to me. It might be interesting to tag here people that could be able to answer a question but do not regularly look at what happens on SE, or to discuss questions/answers in a more interactive way (SE is not very good for follow-up discussions or ideas exchange before writing one).
Last updated: Sep 30 2023 at 06:01 UTC