The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le 18/09/2020 à 17:05, Ralf Jung a écrit :
> So it sounds to me like the standard library was not designed very well in 
> terms
> of module names (no blame here, these things are much easier to realize in
> hindsight), and then to work around that language semantics were adjusted? 
> That
> does not sound very principled.

At some point, you have to be pragmatic and decide that aggravating your
users is not worth having a more principled language. Here is a concrete
example that happened just a few days ago.

Here is a question I could have added to my previous quiz:

6.a Require Coq.ring.Ring.
6.b Require Coq.setoid_ring.Ring.

As it happens, a Coq developer decided to remedy this discrepancy a few
days ago. Guess what? It broke about one quarter of the user libraries
we test in Coq's continuous integration.

It did not take long to decide that this change would just aggravate
users and was not worth it, despite being principled.

Best regards,

Guillaume