# \[Call for Help\] Learn Coq in Y minutes

**URL:** <https://discourse.rocq-prover.org/t/call-for-help-learn-coq-in-y-minutes/397>\
**Category:** Announcements\
**Created:** [August 22, 2019, 9:46am UTC](https://discourse.rocq-prover.org/t/call-for-help-learn-coq-in-y-minutes/397 "2019-08-22T09:46:41Z")\
**Posts on this page:** 9\
**Page:** 1

<div class="post-metadata">

**Author:** ![XVilka](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/xvilka/32/168_2.png) [@XVilka](https://discourse.rocq-prover.org/u/XVilka)\
**Post date:** [August 22, 2019, 9:46am UTC](https://discourse.rocq-prover.org/t/call-for-help-learn-coq-in-y-minutes/397/1 "2019-08-22T09:46:41Z")

</div>

A question for the Coq developers/users - are you interested in promoting Coq further? There is a famous site for newbies, allowing to learn something quickly up to the point to write something useful in it - [Learn X in Y minutes](http://learnxinyminutes.com/). Recently I searched for a quick introduction in Coq, but found none. It would be awesome, if someone knowing it will send a pull request to the corresponding [repository](https://github.com/adambard/learnxinyminutes-docs), solving [this issue](https://github.com/adambard/learnxinyminutes-docs/issues/3161).

(Initially posted at [OCaml Community](https://discuss.ocaml.org/t/coq-learn-coq-in-y-minutes/4278) forum)

---

<div class="post-metadata">

**Author:** ![mattam82](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/mattam82/32/11_2.png) [@mattam82](https://discourse.rocq-prover.org/u/mattam82)\
**Post date:** [August 23, 2019, 4:30pm UTC](https://discourse.rocq-prover.org/t/call-for-help-learn-coq-in-y-minutes/397/2 "2019-08-23T16:30:22Z")

</div>

Sounds like a fun way to advertise indeed, I guess one of the French developers/users can do it, but most are on vacation now 🙂

---

<div class="post-metadata">

**Author:** ![Zimmi48](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/zimmi48/32/7_2.png) [@Zimmi48](https://discourse.rocq-prover.org/u/Zimmi48)\
**Post date:** [August 24, 2019, 9:09am UTC](https://discourse.rocq-prover.org/t/call-for-help-learn-coq-in-y-minutes/397/3 "2019-08-24T09:09:21Z")

</div>

Thanks for advertising this issue. It would be definitely good to be on this site. IMHO this is more of a task for an enthusiast volunteer user to undertake because waiting for a Coq developer to address this is just going to take too long. Among the few Coq developers that care the most about documentation, the current priority is improving the reference manual.

Cf. also this extract of the contributing guide:

> [@Coq's Contributing guide](#):
>
> ### Writing tutorials and blog posts
> 
> Writing about Coq, in the form of tutorials or blog posts, is also a very important contribution. In particular, it can help new users get interested in Coq, and learn about it, and existing users learn about advance features. Our official resources, such as the [reference manual](https://coq.inria.fr/refman) are not suited for learning Coq, but serve as reference documentation to which you can link from your tutorials.
> 
> The Coq website has a page listing known [tutorials](https://coq.inria.fr/documentation) and the [wiki](https://github.com/coq/coq/wiki) home page contains a list too. You can expand the former through a pull request on the [Coq website repository](https://github.com/coq/www), while the latter can be edited directly by anyone with a GitHub account.
> 
> At the current time, we do not have a way of aggregating blog posts on a single page (like [OCaml planet](http://ocaml.org/community/planet/)), but this would probably be something useful to get, so do not hesitate if you want to create it. Some people use [Reddit](https://www.reddit.com/r/Coq/) for this purpose.

---

<div class="post-metadata">

**Author:** ![XVilka](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/xvilka/32/168_2.png) [@XVilka](https://discourse.rocq-prover.org/u/XVilka)\
**Post date:** [October 12, 2019, 8:55am UTC](https://discourse.rocq-prover.org/t/call-for-help-learn-coq-in-y-minutes/397/4 "2019-10-12T08:55:13Z")

</div>

Seems like someone [started to work already](https://github.com/philzook58/learnxinyminutes-docs/blob/master/learncoq.v) on this issue.

---

<div class="post-metadata">

**Author:** ![philzook58](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/philzook58/32/323_2.png) [@philzook58](https://discourse.rocq-prover.org/u/philzook58)\
**Post date:** [October 28, 2019, 2:50am UTC](https://discourse.rocq-prover.org/t/call-for-help-learn-coq-in-y-minutes/397/5 "2019-10-28T02:50:46Z")

</div>

Hi,

That’s my repo. Yup, I’m ever so slowly chugging along. I’ll make a post on here when I think it’s ready for comments.

---

<div class="post-metadata">

**Author:** ![philzook58](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/philzook58/32/323_2.png) [@philzook58](https://discourse.rocq-prover.org/u/philzook58)\
**Post date:** [November 1, 2019, 2:33pm UTC](https://discourse.rocq-prover.org/t/call-for-help-learn-coq-in-y-minutes/397/6 "2019-11-01T14:33:33Z")

</div>

I think I’ve got it into a reasonable form. If anyone wants to look over for inaccuracy, glaring omission, or other suggestions, I’d be much obliged.

[https://github.com/philzook58/learnxinyminutes-docs/blob/master/coq.html.markdown](https://github.com/philzook58/learnxinyminutes-docs/blob/master/coq.html.markdown)

---

<div class="post-metadata">

**Author:** ![XVilka](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/xvilka/32/168_2.png) [@XVilka](https://discourse.rocq-prover.org/u/XVilka)\
**Post date:** [November 12, 2019, 3:52am UTC](https://discourse.rocq-prover.org/t/call-for-help-learn-coq-in-y-minutes/397/7 "2019-11-12T03:52:59Z")

</div>

The pull request has been sent by @philzook58. Amazing job!  
See it here [https://github.com/adambard/learnxinyminutes-docs/pull/3759](https://github.com/adambard/learnxinyminutes-docs/pull/3759)

---

<div class="post-metadata">

**Author:** ![XVilka](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/xvilka/32/168_2.png) [@XVilka](https://discourse.rocq-prover.org/u/XVilka)\
**Post date:** [November 20, 2019, 4:00am UTC](https://discourse.rocq-prover.org/t/call-for-help-learn-coq-in-y-minutes/397/8 "2019-11-20T04:00:37Z")

</div>

And it was merged in master. Still not appeared on the main site yet though.

---

<div class="post-metadata">

**Author:** ![XVilka](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/xvilka/32/168_2.png) [@XVilka](https://discourse.rocq-prover.org/u/XVilka)\
**Post date:** [November 25, 2019, 5:53am UTC](https://discourse.rocq-prover.org/t/call-for-help-learn-coq-in-y-minutes/397/9 "2019-11-25T05:53:35Z")

</div>

Finally it is appeared on the main page: [https://learnxinyminutes.com/docs/coq/](https://learnxinyminutes.com/docs/coq/)