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?
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:
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
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.
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?
I don't think it exists, no.
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.
I'm also on the private beta, but I'm a shy user of the stackexchange network :sweat_smile:
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.
I think the main thing we need right now is more Coq questions, in particular expert questions.
So questions that fall under 3)
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.
Most of such questions that were asked were really being too vague and not specific enough.
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?
Yes, I'm also confused by what is meant by "expert questions".
My point is that we should ask questions that we already know the answer of.
But that come up often and are interesting.
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.
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".
That's 1. writing match annotation for dependent typing and 2. the evergreen nested fixpoints trick
More like "How do I set modes for typeclasses" (that kind of stuff). And yes, your suggests are great PMP.
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?
No reason to exclude them Ana. It's just that this site won't need us for these questions to eventually find their way.
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.
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
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.
"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.
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.
one example of a question that arguably needs expert summary: "What is the state of [support for] coinductive types and coinductive reasoning in Coq?"
@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.
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.
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.
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.
(I found PMP's old slides on coinduction at least: https://www.pédrot.fr/slides/rapido-06-15.pdf)
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.
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).
@Karl Palmskog I've written a detailed answer
thanks, that is exactly the kind of answer I think we can point to when people ask about coinduction (or other advanced topic)
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.
@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 ?
pfout, that's a vast, almost bottomless topic
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...
yeah if we work through the Zulip, we can easily avoid this, people can just outline questions and answers and different people post
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
Nice, I also want to know the answer to that question! For now I have added my partial solution.
@Théo Zimmermann so what do we do with this topic now? Should it be a running topic in the #Coq users stream?
(ideally we'd like to have an integration that posts questions with the tag
coq in the topic)
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.
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.
I propose as a default that we move the topic to users.
This topic was moved here from #Coq Hackathon and Working Group, Winter 2022 > Proof Assistants Stack Exchange coordination by Karl Palmskog.
if there is a lot of activity here (not overwhelming so far), I think we create a new stream
for what it's worth, I have on my todo to summarize incremental compilation/checking in Coq
we also wait (possibly forever) for PMP to produce a tome of knowledge about proof assistant performance bottlenecks
I don't think that the SO format is very good for the performance issue discussion
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?"
The answer for that one is probably YMMV and thus falls in the "opinion" tarpit
well, in case it varies, one can at least sometimes say what it varies with...
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.
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?
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
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?
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.
Would it possible to have the bot report on every question except the ones tagged
Creating a new stream sounds reasonable
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.
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