I'll keep that in mind though if I work with folks in the UK at some point.
I'll keep that in mind though if I work with folks in the UK at some point.
It's really quite self centred to create new problems for the entire world because of a taxi driver. Think about how many people will now have to double search for things, or change scripts, or waste time because they didn't realise new tool=old tool. It's a huge new technical debt being created here. Coq is software, it's been around for many years, so the old name will never die. People will be dealing with half baked renames and duplications forever.
Immature people will find ways to be immature and annoying no matter what - the difference between adults and children is we're supposed to be able to deal with it and keep things in proportion. That doesn't seem to be happening here and it's a pity.
Please don't accuse others of "not engaging in good faith" when they just outlined to you the rational basis for their viewpoints. It's just an ad-hominem insult. My engagement is in entirely good faith: I think you (and others making these demands) are refusing to consider the impact of your demands on other people, externalizing costs unnecessarily and generally acting in anti-social ways, whilst claiming the exact opposite.