wish: answer to @rocqbot

[gares]

so that we can get used to write that instead

[Zimmi48]

Preliminary question: do we want to rename coqbot to rocqbot or should we give it a different name? Personally, I don't think rocqbot is very esthetic. rocq-bot would perhaps be better, but we could also consider a new name that doesn't contain Rocq at all.

[Zimmi48]

Something else to consider:

Currently, on GitHub, we have a coqbot account and a coqbot-app GitHub App. It was not possible to name the App coqbot because of the existing coqbot account. But most of the actions are performed by the app nowadays (despite us calling the coqbot account for convenience when issuing commands). The only thing for which the account is still useful is to push on the run-bug-minimizer repo without having to request extended permissions for the app to do this.

After renaming, it would seem reasonable to have the App use the main name, and the personal account use a secondary name instead.

[gares]

I really don't know much about these technologies, I cannot really advise you here. I did not even think that the @something had to be a real account.

I just found myself writing @coqbot when I should have written @rocqbot or just @rocq.
I suggest @rocq and roll as an alias to @rocq merge now.

[Zimmi48]

After renaming, it would seem reasonable to have the App use the main name, and the personal account use a secondary name instead.

Actually, having @coqbot as a GitHub account instead of a GitHub App is useful so that we can @-mention it and get GitHub auto-complete. If we were to use the main name for the GitHub App, we could no longer benefit from this feature, and we would have to manually type the entire the new name when @-mentioning it. I wonder how this is not a problem in projects which only have an App as a bot.

[SkySkimmer]

The autocompletion isn't great IME, @coq will propose all the maintainer teams before coqbot

[SkySkimmer]

Looking at a random mtac2 PR from when they used bors, it doesn't use @ Mtac2/Mtac2#388