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

[SkySkimmer]

Conclusion? Should we add this as a call topic?

[Zimmi48]

My plan is now:

• rename the coqbot account to ROCQbot
• rename the coqbot-app to ROCQbot-app
• change the logos
• no transition period during which both coqbot and ROCQbot would be supported (much simpler to implement without, since it just means modifying coqbot-config.toml and the README IINM)
• as far as I recall, only the Rocq Prover developers actually use the @coqbot commands, not the other projects that rely on the bot, so we don't need a lot of communication about the change
• do not change the Heroku URL to avoid breaking all the webhooks
• we also need to rename the @rocq-prover/coqbot-maintainers team at some point (and its references in the code)

[SkySkimmer]

rename the coqbot account to ROCQbot

why the capitalization?

[Zimmi48]

Just because rocqbot looks awful to my eyes and I was inspired by the Rocq Prover logo which is ROCQ all caps. But not a strong opinion either, so this is open to alternatives (such as rocq-bot) and/or a vote.
BTW, if we want autocompletion to work better and not conflict with the @rocq-prover teams, we could also call it bot-rocq or butler-rocq or whatever.