search

coq / coq.github.io

Source files of the coq.inria.fr website
https://coq.inria.fr/
Other
15 stars 37 forks source link

remove related-tools page and links to it, point to Awesome Coq instead #176

Closed palmskog closed 3 years ago

palmskog commented 3 years ago

The "Related Tools" page is completely out of date with respect to modern tools for Coq and built on Coq. I think the Awesome Coq project is now in such a good shape (100+ entries, 100+ GitHub stars) that it can take over the role of Related Tools completely. Hence, this PR removes Related Tools and all links to it, and points to Awesome Coq where appropriate.

cc: @Zimmi48 @anton-trunov

Zimmi48 commented 3 years ago

I'm supporting of the idea. The Related Tools page has always been a hell to maintain and recently we have been talking of removing it and linking to the wiki. I think that linking to awesome-coq is a better choice.

Zimmi48 commented 3 years ago

cc @coq/core in case you have an opinion (in case there is no opposition, I propose to merge by the end of next week).

palmskog commented 3 years ago

Please add a redirection from Related Tools to Awesome Coq. See https://github.com/coq/www/blob/master/aliases.footer.conf.

I added a redirect to the tools section of Awesome Coq in ab67226. I can't test locally if it works, but I tried to follow the pattern for redirects used for Nahas' tutorial.