Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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


Chronological Thread 
  • From: Ralf Jung <jung AT mpi-sws.org>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] option to disable partially qualified Require Imports
  • Date: Thu, 17 Sep 2020 17:40:36 +0200
  • Authentication-results: mail3-smtp-sop.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:0qbz5hcSSwcEC2ANNjuAWeESlGMj4u6mDksu8pMizoh2WeGdxcS4Zx7h7PlgxGXEQZ/co6odzbaP7Oa4BSdQud7B6ClELMUSEUddyI0/pE8JOIa9E0r1LfrnPWQRPf9pcxtbxUy9KlVfA83kZlff8TWY5D8WHQjjZ0IufrymUoHdgN6q2O+s5pbdfxtHhCanYbN1MR66sRjdutMZjId/KKs90AfFr3RHd+lV2W9jOFafkwrh6suq85Nv7iVdt+g9+8JcVKnxYrg1Q6FfADk6KW4++dfltQPETQuB53scVnsZnx9VCAXb7x/0Q4n8vDLiuuVyxCeVM8v2TaspWTu59KdkVAXoiCYcODEn9mzcl9F9g7haoBKloBx/3pLUbYSIP/dwYq/RYdUXTndHU81MVSJOH5m8YpMSAeQfM+ZWr4rzqVUAohSxBwajGOzhxyRUhnL1x6A2z/gtHA/E0QEmAtkAsG7UrNLwNKoKTe661q3IzTveZP1SxDf97ofIeQ0mrPGOQLJwd8XRxFIqFwPdj1WcsJflPj2O1ugXtGib9eVgWPuphmU6pA5/viKhyd0wionVmI0V0FbE+D13zYg1KtC1VFN2bNy4HJZUqi2UOYh7T80/Tmxrtyg3yb8LtYK6cSQU1Jgq2xHSZvKJfoSV/h/uSuicLDRmiH9rfr+0mhW88VC4x+HhWMS51ExGojdBn9XWtX0A1gbf5tWHR/dl/Eqs2yyD2x3Q5+xAO0w4i7fXJ4Qjz7M/kJcYrF7NETXsmErsia+bbkUk9fas6+TgerjmpIKcN5d1igHiLKsugNazAeEgMggPRmSb+uC81Kb48kHjRbVKlvI2nrPEv5/EPcgbp6i5DBFJ0os79hqyATOr3M4FkXQDNl5IexOKg5L0N1zOOPz4CO2wg1WokDdl3fDGObjhD43PLnjelrfhcq1w60tEyAoy1Nxf/JxVCqobLPL0QE/xu8TUDgUlPAys3+bnFNJ925sCVmKIG6+VKb/dsVuV5u00OOSMf48UuDPlK/c//fLujHk5mUUcfaazx5cXZmq4TbxaJBCSZmOpidMcG08LuBA/Rarkkg6sSzlWMky7W6x0xCw9B8ryD5rFSaiomL3ExzigWJpMaTYVWRi3DX70etDcCL83YyWIL5o5y2FWZf2aU4YkkCqWmkr6xr5gdLeG+DAAtI7uzp5w/+yWlhUp/3pxF8vb32zfFzglzFNNfCc/2eVEmWI4z16C1aZihPkBTo5W//IMSRghc5nGwL4jUoygakf6Zt6MDW2ebJC+GzhoFYA0295LeFlmXdK4gUKb0g==

Hi,

> Le 17/09/2020 à 16:19, Abhishek Anand a écrit :
>> I used to think that using disjoint logical prefixes for different
>> libraries and always using fully qualified names in Require Imports
>> would suffice for avoiding errors due to incorrect files being imported.
>> However, it was recently pointed out to me that this is not sufficient:
>> Suppose we have 2 .vo files, one with fully qualified name A.B.C and
>> another with fully qualified name B.C.
>> Now we suddenly have no reliable way to Import the latter file unless
>> there is a way to tell `Require Import` that the name should be
>> interpreted in a fully qualified manner.
>> Is there a workaround for this?
>
> You can use:
>
> From A Require B.C.
> From B Require C.
>
> If you have three files named A.C, A.B.C, and B.A.C, then there is no
> foolproof way to load A.C. But this is the author of library A being
> malicious. Just stop using library A.

I cannot see any malice here, maybe just slightly messy naming.
But Coq should support unambiguous imports no matter how messy or questionable
the naming choices of any library involved are.

I've had quite weird problems in the past caused by stale .vo files being
picked
up by ambiguous imports, so I'd be all for a way to ensure that all imports
are
unambiguous. (In fact I am quite surprised that ambiguous imports exist at
all,
that seems quite contrary to Coq's usual design geared towards precision. No
other language I work or worked with has ambiguous imports the way Coq does --
Python, Java, C++, Rust all do not have this problem.)

Kind regards,
Ralf



Archive powered by MHonArc 2.6.19+.

Top of Page