coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] option to disable partially qualified Require Imports

From: Ralf Jung <jung AT mpi-sws.org>
To: coq-club AT inria.fr, Guillaume Melquiond <guillaume.melquiond AT inria.fr>
Subject: Re: [Coq-Club] option to disable partially qualified Require Imports
Date: Fri, 18 Sep 2020 17:05:52 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT jupiter.mpi-klsb.mpg.de
Ironport-phdr: 9a23:gBzGYh2m5IAPFkP1smDT+DRfVm0co7zxezQtwd8ZsesWLvjxwZ3uMQTl6Ol3ixeRBMOHsq0C07Sd7f+oGTRZp8rY7jZaKN0EfiRGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkJ6KevvB4Hdkdm82fys9J3PeQVIgye2ba9vIBmsogjdq8sbjZF+JqswxRfEo3lFcPlSyW90OF6fhRnx6tqx8ZJ57yhcp/ct/NNcXKvneKg1UaZWByk8PWAv483ruxjDTQ+R6XYZT24bjBlGDRXb4R/jRpv+vTf0ueR72CmBIM35Vqs0Vii476dqUxDnliEKPCMk/W7Ni8xwiKVboA+9pxF63oXZbp2ZOOZ4c6jAZt4RW3ZPUdhNWCxAGoO8bpUAD+wdPeZDsoLxo0ICoQaiCQWwAe/izCJDiH3r0q0gy+kvDB/I3AIgEdwNvnrbotr6O6UOXu6616TI0TbOYulK1Tvh5oXFcBYsquyMU7JqdsrRzFEiGR/fgVWUp4zuIjeb1vkLs2iU8uFtUuCvi3MhqwF+uTWvw98siojQioIOxFHE7j91wIEvJd23UUN2Z8OvH5RMuS+ALYR2Xt8iTH9yuCY80rALuJ61cDUJxZg72hPSdeGKfouJ7x/sVOudPDh2iX14db+9iBu/8ketx+7zW8S231tHoSVLn9fQu34C1RHd6smKR/1g9Umv3jaP0hrc6uBCIU0sjqrbN4Qhwr82lpocq0jDBSj2lF3zjK+Od0Uo4/Oo6ur8Yrn8oZ+cLYB0hwfjOaotgsyyGfk0PwYKUmSB5Oix0Kfv8E74TblQk/E7krHVvZLYKMgBu6K0BxNZ3pw+5xu+ADqqysoUkWcHIV9DZRmJlZLmO0vUL/D9Ffq/g0qjkDNsx/3ePL3hH43NLnnfkLj/Z7Zx8UtcyBIyzdxG5JJUDqoBL+npVk/0rNzYAQU1PBGqzOr/CdV90J0RWX6XD6OEPq7ftUWE6v8rLuWWZ4IYuSzxJ+Ul6vL2iH82g14dfa2n3ZsNb3C4G+xrI0eEYXrqjdcMCmIKvhI/TODzk12DXyVTa2y1X6Im6TE3EJimApvbRoCxnLyB2z+2HphIaWBCE1CMDHbod4KCW/oXaSOSI8phnSceVbe7UYMh1BeutBX7y7V9NObU9DcYv4r51Ndp/+3TiQ0y9TtsAsuB1GGNVnh4kX8MRz8rx69yuld9y1eG0ahgmfNUD91T5/VTUgc7L5HQ1eJ6C8qhEj7GK9yOUROtRsisKTA3VNM4hdEUJw5SBtSmihne2ifiJrIRjqGKA5o4uvbTwnn1I89gznuA0aQllkQnRc1DHWygnK92sQbJUd3niUKcwpyjcapU/jPL+y/Xz3eIs2ldSA81SrreG3cFaR2F/pzC+kreQur2WvwcOQxbxJvHc/MSM4y7vRB9XP7mfe/mTSe0kma0CwyPw+rXPo/yeiAGwz6bD1ILwVlKoSS2cDMmDyLkmFrwSSR0HAu0MUb08Kxlt2j9SVU7nVnTMh9RkoGt8xtQvsSyDvMe2rVe5XUjti11AFunmdfOCp+DoxFrOqBEbpUx7QUf2A==

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.

; Ralf

On 18.09.20 17:01, Guillaume Melquiond wrote:
> Le 18/09/2020 à 16:46, Ralf Jung a écrit :
>> (Probably the
>> language designer had a good reason and this was solving a concrete
>> problem, but
>> putting the blame on the library is just unfair. And you haven't argued
>> for why
>> Coq's semantics make any sense, either.)
>
> The reason is the standard library of Coq. It is important to understand
> how painful it would be to use if Imports had to be fully qualified.
> Here is a quiz for you. Which of the following are correct?
>
> 1.a Require Coq.List.List.
> 1.b Require Coq.Lists.List.
>
> 2.a Require Coq.Reals.Reals.
> 2.b Require Coq.Reals.Real.
>
> 3.a Require Coq.Derive.Derive.
> 3.b Require Coq.derive.Derive.
>
> 4.a Require Coq.Btauto.Btauto.
> 4.b Require Coq.btauto.Btauto.
>
> 5.a Require Coq.String.String.
> 5.b Require Coq.Strings.String.
>
> So, when we introduced the From-Require syntax, we decided that the user
> should never have to learn all these idiosyncrasies, which we have to
> preserve for backward compatibility.
>
> Sure, if you are using your own standard library, then you do not need
> to bother about it. But Coq's developers do not have this luxury.
>
> Best regards,
>
> Guillaume
>

--
Website: https://people.mpi-sws.org/~jung/

Re: [Coq-Club] option to disable partially qualified Require Imports, (continued)