Rename the repository? about coq-hott

[jarlg]

The docs confirms the things mentioned, so renaming sounds fine to me (though I don't have any experience with it). It does say that actions/workflows need to be recreated for the "new" repo, just to mention that.

While we're at it, maybe update the "About" part of the repo to say something like "A Coq library for Homotopy Type Theory (HoTT)"?

[mikeshulman]

This seems like a good idea to me, but we should get some more input from other contributors.

[Alizter]

ping @HoTT/team-hott @jdchristensen @jarlg

[jdchristensen]

I'm not familiar with now renaming works, but as long as there is no disruption, renaming makes sense. I always refer to it as the Coq-HoTT library.

[mikeshulman]

I've renamed a repository before, and I think the old name is redirected and continues to work; it's not as if everyone has to change the names of their remotes in their local copies. But I assume new clones will use the new name, and the old repo site would be redirected to the new one.

[Alizter]

@jarlg I believe the actions warning is referring to repos that host a github action. So if I had in another repo's workflow uses: HoTT/HoTT@v1 I would have to rename this. Obviously the HoTT library is doing no such thing, so we need not worry.

[peterlefanulumsdaine]

I strongly support this renaming — with the current name, talking about the library is always a bit confusing and needs disambiguation. I’ve renamed repositories a couple of times before (private, with 2 or 3 collaborators iirc), and it went smoothly — in particular, the old address remained active for some while afterwards, as it’s supposed to.

One minor detail — capitalisation. Coq-HoTT, coq-hott, or something else? Both seem fine to me — obvious minor advantages to each (coq-hott is consistent with the opam package, Coq-HoTT consistent with our Github organisation name), but no major problems with either. I vote very marginally for Coq-HoTT, and to avoid bikeshedding, I promise not to discuss this point any further.

[SkySkimmer]

https://github.com/CoqHott/ exists but probably isn't big enough to confuse people

[spitters]

I'm not certain about the change. E.g. our library is called math-classes, but in opam it becomes coq-math-classes.
If we follow the same convention, HoTT would be fine.

I've heard a number of (american?) people say that the combination of HoTT and Coq gives them even more distracting thoughts than the name Coq itself. I'm not a native speaker myself and I do not have these associations, but it appears to be an issue for a number of people.

[mikeshulman]

I've heard a number of (american?) people say that the combination of HoTT and Coq gives them even more distracting thoughts than the name Coq itself. I'm not a native speaker myself and I do not have these associations, but it appears to be an issue for a number of people.

I think that Coq-HoTT would be better in this regard that HoTT-Coq. But it's certainly an issue. There was a discussion a while ago about the possibility of renaming Coq itself, but I haven't heard any more about it for a while.

On the other hand, there's no reason in principle why the name of this library has to involve either "HoTT" or "Coq". It's true that it's more descriptive that way, but on the other hand, calling it Coq-HoTT could be considered presumptuous, since there could in principle be many different Coq libraries for HoTT (and I know there are at least some others, although there doesn't seem to be quite the library fragmentation that there is for (Book-)HoTT Agda libraries).

[Alizter]

I like the name HoTT since for a long time we have called it "the HoTT library", therefore I don't think we would be an more presumptuous than before. I would suggest coq-hott since adding capital case letters in library names doesn't really follow the convention. Coq-Equations for example is capitalised this way and it causes a lot of confusion every time I need to type it accurately.

@spitters The reason this discussion came up at all is because there are a number of people wanting to contribute to the HoTT book and have confusingly come to HoTT/HoTT. With mathclasses this is not the case since there is nothing to be confused with.

If nobody has any objection, I will rename to coq-hott next week. I can also update the About info as @jarlg suggested.

[SkySkimmer]

AFAIK all opam packages are lowercase so I don't thnk it implies what the name should be

[Alizter]

Hmm after rereading the discussion I'm now convinced that Coq-HoTT is the way to go. Will do that tomorrow.

[Alizter]

It turns out that updating the name meant we had to update each of the checksums in our previously released opam packages due to changing URLs.

However nothing a few scripts could not handle: coq/opam#2376