Web site hott.github.io/HoTT?

[herbelin]

Hi, wasn't there a site https://hott.github.io/HoTT at some time (as e.g. linked from https://github.com/HoTT/Coq-HoTT/wiki#documentation)? It currently returns a 404 error (comparatively, https://hott.github.io/M-types works).

[Alizter]

The repo was renamed to Coq-HoTT so likely the links need to be updated too.

The Hott part of the website links need to be changed to Coq-HoTT.

[herbelin]

Thanks! I did not realized that the repository changed its name. I updated the wiki main page.

By the way, would a redirection of the HoTT web page to Coq-HoTT be possible? Or at least having https://hott.github.io/HoTT pointing to a page telling to update the links to https://hott.github.io/Coq-HoTT?

[herbelin]

Ah, apparently, the HoTTCore.svg and HoTT.svg on the main wiki page have also to be updated so that HoTT is replaced by Coq-HoTT in the url bound to the nodes of the graph.

[herbelin]

Note that there are issues also with some proviola pages such as https://hott.github.io/Coq-HoTT/proviola-html/HoTT.Categories.Adjoint.html or https://hott.github.io/Coq-HoTT/proviola-html/HoTT.Categories.html. They are not found but this is maybe a proviola bug as other similar proviola pages work. Moreover, the corresponding coqdoc and alectryon pages work.