Comment author: @Zimmi48

The list of pages on the wiki can be seen in the right panel on any wiki page.
A lot of them (probably the majority of them) are completely outdated.

Some pages only contain broken links. Example: https://github.com/coq/coq/wiki/Tactic-Fix
Some pages are so outdated that they contain misleading information. Example: https://github.com/coq/coq/wiki/CoqStyle. Such a page BTW if it was up-to-date, should be in the developers documentation in the main repo.

Do personal pages on Cocorico still make sense (especially when they contain only an e-mail address)? My personal opinion is no.

This page proposes a better subst tactic. If it is really better, it should go into the standard library / be integrated to the subst tactic itself; otherwise the page should just be deleted: https://github.com/coq/coq/wiki/Tactic-SubstPlusPlus
Other similar example: https://github.com/coq/coq/wiki/Tactic-DecomposeRecords

Some documentation found on Cocorico should be moved to other platforms.

It is not sane when a wiki page is created one day and never changed then... Example: https://github.com/coq/coq/wiki/GenericTactics. A blog post is a more appropriate platform in that case because it is clearly dated and people can understand better how this can be outdated content. Also, it clearly gives the responsibility of the updating to the author instead of diluting it. Yves Bertot recently advertised a shared blog platform https://project.inria.fr/coqexchange/ that could serve this purpose.
When a page contains only code, like this one https://github.com/coq/coq/wiki/ArithmeticExpressionParser, it should get versioned somewhere that is tested so that it can be updated. We can envision several possible outcomes for such small contributions. If it is valuable enough and fits in, it could go to the standard library. If the author wants to, it could go in a GitHub repository / gist, and the author would take care of the maintenance. Or it could be considered a contrib that should be maintained by the Coq team (if deemed valuable but does not fit in the standard library). For such small contributions, we should introduce a new shared repository, say coq/libraryextensions.
When a page is about something external to Coq, it should be moved to the documentation of this external thing. Example: https://github.com/coq/coq/wiki/CoRN
Some pages have nothing to do on the wiki and if they contain any form of valuable information it should be in the reference manual instead: https://github.com/coq/coq/wiki/TypeClasses

Some pages are just useless, but I've already started deleting some of these.

And I personally don't think that the wiki is a good venue for having discussions. They can be useful to take notes of a discussion happening somewhere else (like during a meeting). Issues are a more appropriate place to have actual discussions.

I've only been talking in this bug report of pages which should be IMHO deleted / moved elsewhere. Some pages that do make sense on a wiki should also be curated but that shall be the subject of another bug report (it will be also easier to find them if there is less noise around).

❗️ Note: edited after the move to GitHub wiki with correct links.

Lots of pages on the wiki should be deleted / moved elsewhere #5681

Description

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions