Homepage update?

[patrick-nicodemus]

This webpage is not yet official but when Coq 9.0 is released users will be able to search this website for Coq packages related to what they are looking for.
https://rocq-prover.org/p/coq-hott/latest

The "homepage" link for Coq-HoTT that page directs to homotopytypetheory.org. I am wondering if that URL should be updated to point to this Github repository? The Homotopy Type Theory book and the associated Univalent Foundations collaboration are closely related to this project but my feeling is that the 'project homepage' should be something a bit more narrow or project-specific (for example, the Alectryon documentation at hott.github.io/Coq-HoTT can be found from this site, but not from homotopytypetheory.org) This Github repository of course links back to homotopytypetheory.org in the first link of the main README, so it is still easy to find that site.

[jdchristensen]

I agree that the homepage link should point to this github repo. @Alizter will know where that data comes from.

[patrick-nicodemus]

Actually this is a currently relevant issue because the same concerns apply to the opam page for the Coq-HoTT package.

[Alizter]

This comes from dune-project. If you update that and do dune build @install it should update the .opam files too. When we next cut a release, we will have the updated URLs.

I have already cut a v9.0 release https://github.com/HoTT/Coq-HoTT/releases/tag/V9.0 here, so we should send a PR to coq-opam-archive when rocq 9.0 is released, with the URL modified. See our releases here: https://github.com/coq/opam/tree/master/released/packages/coq-hott

[Alizter]

Also note that "bug-reports" points to the "correct" website.