Coq: The FAQ should be moved to the wiki

[Zimmi48]

The FAQ is very outdated but it's still useful. It is still well referenced and people are still looking at it for answers.
It used to be generated from sources in the Coq repository but recently the web version and the TeX version have diverged.
Finally it is hard to contribute to.

What I propose is to remove the FAQ from the repository and the website and move it to the wiki. The current webpage would redirect to the new wiki page. This would solve most of the problems listed above, and by making it easier to contribute to we can hope to get help in making it less outdated.

Currently the FAQ is very long and has many sections. I guess it would make sense to have several distinct page. In particular "Talking with the Rooster" could get its own page (and possibly a less cryptic name).

Help wanted. Anyone can contribute.

[mattjquinn]

Théo, I saw your reply to the Coq Club email thread about this. I have some experience with Coq and some time to work. Can you reply with the guidance you said you had on this?

[Zimmi48]

Wonderful! So, first of all there are two sources for the FAQ:

• In this repository, in the doc/faq folder, the output being FAQ.v.pdf
• In the https://github.com/coq/www repository (pages/faq.html), the output being https://coq.inria.fr/faq.

A first step could consist in identifying the differences in content between the two (if possible without spending too much time on this).
There is at least one difference which is this figure axioms by @herbelin (which BTW does not render well at all in the PDF output I linked above). I don't personally find this figure very readable, but maybe it could be kept until someone can improve it.

A second step would be converting either source into Markdown to be able to import it into the wiki (and patch it as necessary not to lose content from the other source).
I think I would also separate this FAQ into several pages (because it is so long).
The Coq wiki https://github.com/coq/coq/wiki is editable by anyone so you can just create the new FAQ pages at this point.

It could be interesting to do some clean-up / removal of questions that do not make sense anymore, but this can very well be done in a second step with help from other people.

Finally the last steps would be opening PRs on this repo and on https://github.com/coq/www to remove the old FAQ sources, ping one of the maintainers at this time to redirect https://coq.inria.fr/faq to the wiki page, and possibly advertise the reborn FAQ on Coq-Club and in the README.

Do not hesitate to comment here on your progress / hurdles and ask for help if needed.

[Zimmi48]

BTW one way of checking the differences would be through git log -p doc/faq/ in this repo vs git log -p --follow pages/faq.html in https://github.com/coq/www. With these commands we can see indeed that the FAQ has been fixed multiple times and inconsistently on both sides.

[mattjquinn]

Thanks for the guidance Théo. I've merged the differences together into a collection of Markdown files and added everything to the wiki, with the main entry page being here:

https://github.com/coq/coq/wiki/The-Coq-FAQ

Everything is a new page except for Extraction; there's already a more comprehensive extraction page in the wiki than existed in the FAQ, so I simply merged the few sentences from the latter into the former.

One thing to note is that the image in this section:

https://github.com/coq/coq/wiki/The-Logic-of-Coq#what-axioms-can-be-safely-added-to-coq

is linked to from my own personal account; we'll need to upload that image to this repository somewhere and change the link accordingly.

[Zimmi48]

Thanks for this impressive work! The result looks amazing!
I see that you have fixed quite a few links in passing, thank you for this as well.

One thing to note is that the image in this section:

https://github.com/coq/coq/wiki/The-Logic-of-Coq#what-axioms-can-be-safely-added-to-coq

is linked to from my own personal account; we'll need to upload that image to this repository somewhere and change the link accordingly.

I've just imported the image using git command-line and fixed the link.

Let me know if you intend to follow-up with the pull requests removing the FAQ from the sources and the website or would like someone else to do this.

I'll ping @letouzey in person tomorrow to redirect https://coq.inria.fr/faq to https://github.com/coq/coq/wiki/The-Coq-FAQ (unless he notices this comment before).

[mattjquinn]

No problem, glad to hear that everything looks good.

I've created the coq/www PR here: https://github.com/coq/www/pull/56

And the coq/coq PR is here: https://github.com/coq/coq/pull/6377

[Zimmi48]

@mattjquinn Thanks again for your contribution. I'll send an e-mail announcing the rebirth of the Coq FAQ on Coq-Club soon.