Kenji Maillard (Feb 17 2022 at 13:38): Kenji Maillard (Feb 17 2022 at 13:38):I don't find getting started wiki page on Coq's faq that would give an overview of existing tools (emacs/PG, vscoq, coqIDE or others like pure coqtop ?) and how to set them up .
Should a new page be created for that purpose ?
@Tomás Díaz pointed out this page but it's geared toward setting up tools for working with ocaml.
Paolo Giarrusso (Feb 17 2022 at 13:41):Ideally user docs belong in the manual (and I thought there is something), but the wiki might indeed be easier to work on
Tomás Díaz (Feb 17 2022 at 13:42):isn't the manual more like a reference doc? (or maybe I'm thinking about a different manual)
Paolo Giarrusso (Feb 17 2022 at 13:44):the Coq manual plays both tutorial and reference, but nobody has setup a separate official tutorial
Kenji Maillard (Feb 17 2022 at 14:02):the manual is not really adequate to keep track and share knowledge on experimental tools/methodologies (e.g. using dune with emacs/PG today)
Théo Zimmermann (Feb 17 2022 at 14:30):Paolo Giarrusso said:
the Coq manual plays both tutorial and reference, but nobody has setup a separate official tutorial
There used to be an official tutorial, but it was not maintained (and meanwhile there were lots of great unofficial tutorials) so we removed it.
Kenji Maillard (Feb 17 2022 at 15:06):I created this getting started and added what I know on my setup (spacemacs + PG). Improvements and links welcomed !
Hanneli Tavante (Feb 17 2022 at 15:10):Sorry, what is the difference betweeen https://github.com/coq/coq/wiki/DevelSetup and https://github.com/coq/coq/wiki/Getting-Started ?
Hanneli Tavante (Feb 17 2022 at 15:10):(Ah, sorry ^2, I just read the discussion... Maybe https://github.com/coq/coq/wiki/DevelSetup is what you originally wanted? )
Kenji Maillard (Feb 17 2022 at 15:12):DevelSetup is about setting up ocaml, not coq, no ?
Hanneli Tavante (Feb 17 2022 at 15:13):I think it's about setting up the dev environment for Coq
Kenji Maillard (Feb 17 2022 at 15:13):I would expect that the first thing a newcomer to coq wants to learn is how to set up an environment to use coq rather than how to hack on coq.
And actually I am often puzzled about my own set up, so having a global place to keep information would be useful for me too.
Hanneli Tavante (Feb 17 2022 at 15:14):I agree that DevelSetup is not the most clear choice
Sam van G (Feb 18 2022 at 13:28):As a relatively new user, I agree that a Getting Started page with step by step "quick installation" instructions would be a great addition.
I think it could be good to also have a section on that page titled something like "If you want to try out Coq without installing anything", linking to a JSCoq instance. Do people agree?
If so, I would be happy to contribute to such a text.
Kenji Maillard (Feb 18 2022 at 13:33):Jscoq is mentioned on the official page so it should probably be added to the wiki as well
Sam van G (Feb 18 2022 at 15:01):I added some questions and answers to the getting started page.
The page is a bit hard to find for a beginner I think - only through FAQ -> Getting Started. Should there be a link on the main wiki page?
Sam van G (Feb 18 2022 at 15:05):Here are also some suggestions for three further questions that could be answered on the Getting Started page.
I have for now put these as comments at the end of that page, because I wasn't sure about the answers, but I think these questions could be very useful to answer. If you agree, maybe someone more knowledgeable than me wants to weigh in and write some short answers? E.g. @Théo Zimmermann?
Hanneli Tavante (Feb 18 2022 at 15:09):Related question: How much (if any) of this getting started should be reflected in the main webpage https://coq.inria.fr/ ? (see Learning about Coq + Running Coq + Contributing to Coq)
Sam van G (Feb 18 2022 at 15:19):@Hanneli Tavante I think the readability & usability of those sections on the main page could use improvement. I don't know what is the right workflow for suggesting improvements to the Coq main webpage though?
Jean-Christophe Léchenet (Feb 18 2022 at 15:47):The website has its own repository (https://github.com/coq/www), so you may work with issues and pull requests, I guess.
Théo Zimmermann (Feb 18 2022 at 17:34):Yes, please do feel free to open PRs on the www repo.
Théo Zimmermann (Feb 18 2022 at 17:34):We would like to do some major redesign in the future but in the meantime improving the content is already a good first step.
Théo Zimmermann (Feb 18 2022 at 17:35):I come from a mathematics background. What beginner resources in Coq do you recommend?
I come from a programming background. What beginner resources in Coq do you recommend?
It's too bad we didn't think to ask people about this in the survey. Because I think people who have learned Coq with these backgrounds would be the best to answer.
Théo Zimmermann (Feb 18 2022 at 17:36):For instance, I think that the MathComp book was thought to be more mathematician-oriented but in the end for some of them Software Foundations might be more approachable.
Théo Zimmermann (Feb 18 2022 at 17:36):As for where to look at some examples of Coq in action, I guess https://github.com/coq-community/awesome-coq would be a good place?
Théo Zimmermann (Feb 18 2022 at 17:38):Théo Zimmermann said:
I come from a mathematics background. What beginner resources in Coq do you recommend?
I come from a programming background. What beginner resources in Coq do you recommend?It's too bad we didn't think to ask people about this in the survey. Because I think people who have learned Coq with these backgrounds would be the best to answer.
We could ask about this next time we do a survey. In the meantime, we can insert such sections but make them collaborative (i.e., encourage people to add to them if they have good resources that have been useful to them depending on their background).
Hanneli Tavante (Feb 18 2022 at 17:38):Théo Zimmermann said:
I come from a mathematics background. What beginner resources in Coq do you recommend?
I come from a programming background. What beginner resources in Coq do you recommend?It's too bad we didn't think to ask people about this in the survey. Because I think people who have learned Coq with these backgrounds would be the best to answer.
There seems to be a common answer (not necessarily the best) that the Mathcomp book is a good resource for mathematicians, and Software Foundations (and Formal Reasoning about Programs) are more programming oriented.
Hanneli Tavante (Feb 18 2022 at 17:39):In the meantime, we can insert such sections but make them collaborative Do you mean maybe adding a link to the Getting Started Wiki on the main website and suggesting "If you have more references, please add them in the Wiki" or something?
Théo Zimmermann (Feb 18 2022 at 17:39):Yes, but I've read people with math background say that SF has been good for them.
Théo Zimmermann (Feb 18 2022 at 17:40):Hanneli Tavante said:
In the meantime, we can insert such sections but make them collaborativeDo you mean maybe adding a link to the Getting Started Wiki on the main website and suggesting "If you have more references, please add them in the Wiki" or something?
I just meant clarify on the wiki page that this list is a WIP and that people should feel free to add to them.
Sam van G (Feb 18 2022 at 19:36):I added reference to Zulip and Discourse and the Awesome Coq list, and a generic answer about "resources for background X", and a specific invitation to add to the page.
Sam van G (Feb 18 2022 at 19:40):This is only loosely related, but still: while I was looking up the Zulip link on Coq's official webpage, I noticed that all messages posted here are openly published online. I'm not sure if everybody who is writing here, especially beginners (like me), realize that their messages on this Zulip are on the internet forever (?) with their full name attached to it, potentially searchable / crawl-able (?). The interface initially gave me the impression that we are in a semi-private chatroom.
Putting aside for the moment the question of whether openly archiving all messages is at all desirable, I think it might be a good idea 1) to state this very clearly when people sign up for the Zulip in some welcome message 2) to state this in references to Zulip for beginners.
Has there been discussion about this open archive in the past in the community?
Kenji Maillard (Feb 18 2022 at 20:10):Yes, archiving of this zulip has been discussed in this stream at least @Sam van G .
Sam van G (Feb 18 2022 at 20:16):Thanks, Kenji. In that stream I see mostly technical discussion about the archiving and where to publicize it. The question I'm raising is more one of privacy concerns and whether everyone posting here is aware that they are essentially posting to a public forum.
Kenji Maillard (Feb 18 2022 at 20:28):That's a sensible concern, maybe that information (that these streams are made publicly available) could be added to the welcome bot by an administrator (it seems that the bot is somewhat configurable)
Paolo Giarrusso (Feb 18 2022 at 21:29):@Sam van G I think you are completely right that the open archiving should be clarified. And without wanting to detract from that, I also want to say that nobody _should_ hold beginner questions against you.
Théo Zimmermann (Feb 19 2022 at 11:54):Thanks for making these points and suggestions. There's already the information that the Zulip is archived everywhere Zulip is mentioned on the website but modifying the message of the welcome bot sounds like a good idea (I didn't even recall that there was a welcome bot).
Théo Zimmermann (Feb 19 2022 at 11:55):FTR, we hope that at the next major Zulip release we will be able to make the Zulip-forum anonymously browsable, and thus the archive will become redundant and will be removed.
Théo Zimmermann (Feb 19 2022 at 11:59):I didn't find how to modify the welcome bot but I did edit the organization description that shows up when people register or log in: image.png
Emilio Jesús Gallego Arias (Feb 21 2022 at 14:34):Maybe this is relevant https://github.com/coq/coq/pull/9824
Last updated: Jun 11 2023 at 00:30 UTC