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, Théo Zimmermann <theo AT irif.fr>
Subject: Re: [Coq-Club] option to disable partially qualified Require Imports
Date: Fri, 18 Sep 2020 13:25:58 +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:FW9cYx8v8+yU1/9uRHKM819IXTAuvvDOBiVQ1KB21+ocTK2v8tzYMVDF4r011RmVBNqds6wP0LGe8/i5HzBZv9DZ6DFKWacPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3wOgVvO+v6BJPZgdip2OCu4Z3TZBhDiCagbb9oIxi6sAfcutMKjYZjJao8xBXEqWZMd+hK2G9kP12ekwv968uq4JJv7yFcsO89+sBdVqn3Y742RqFCAjQ8NGA16szrtR3dQgaK+3ARTGYYnAdWDgbc9B31UYv/vSX8tupmxSmVJtb2QqwuWTSj9KhkVhnlgzoaOjEj8WHXjstwjL9HoB+kuhdyzZLYbJ2TOfFjZa7WY88USnRdUcZQTyxBA52zb40TD+oaIO1Uq5Dxq0YSoReiAAWhAv7kxD1ViX/sxaA0zvovEQ/G0gIjEdwBvnvbo9fpO6kdSu210KrFwC/fY/9K1zrw6o7FeQ0hr/GWWrJwdNLcx1U1GAPBgFWbtIjrPy6T1uQCrmOW6OhgVf+pi24osAxxpyCvxsY1honSiIMV0UrI9SJjwIY6PNC1TlNwbtG4HpVKrS6aK5d2Td04Q2FuoCs0xbMItJ6ncCUJ1Zkqxx7SZv+afoWI/x7uW+KcLDdmiX9mZL6zmhK//Va+x+P8SMW53ktGoyRBn9fMuH0ByxPe586aQfVz+Ueh3CyA1wHV6uxcJEA0javbJ4c6wr8+jZofq0PDHjX5mEjwkaSYdV0k9/C15+npZrjqvIKQOotuhgz9M6kigNGzDOQgPgUMXWWX4/mw2bn/8UHjXblHj/I7nrPHvJzEJckWoLOyDRVP3YY58Rm/Ci+r0NQGknkDK1JIYBCHj5XxO1HPPPD3E+2/j06pkDdzxvDKJ77hApHWLnfYirvheK5960FGxAUu099T/5NUCrcfL/LvQkL9qdLVAxsjPwCpx+vrEtZw24IEVW6SAqKVKKbSvkWJ5uIrLemMfogVuDPlJvgn+v7ui3A5lEQYfamx3JsbcWu4H/p9I0mDZnrsmNgBHX8QvgUiVOzqlEGCUTlLanmuWKI8/yg3B56iDYfeXY+gm6eB3Se+Hp1OfG9KEFGMEXHyd4WFQfgAciySItUy2gADALOmUsoq0QyknA780btuaOTOvmUktRPk4+p04ujejxQ78zo8W9id3malTnt1kCUGXWll8rp4pBlHw1ONmYplhfMQQd5O4fxhVx87cIXD1Kp9Ed+kCVGJRcuAVFvzGobuOjo2VN9khoZWOx8sSeXntQjK2m+RO5FQkrWKAJIu9aeFhCr0P8c40Gndkq47gAt/G5cdBSidnqd6sjPrKcvRiUzAzPSvbaVZxzHWsmCZwjjW5RwKYEtLSazAGEsnSA7WoND+vB6QTaK2CKgqKE1E0c/HKa9RYJvslVoASPqxYNk=

Hi Théo,

>> 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.)
>
> With Dune, this won't be an issue anymore.

Given that Dune is a build system, how can it add the missing language feature
of precisely specifying which file to import?
It might help against the "stale vo" problem, but that was just an example.
There are many more reasons for wanting imports to be unambiguous, like being
sure ones code keeps compiling and doing the right thing when more modules are
added.

Kind regards,
Ralf

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

[Coq-Club] option to disable partially qualified Require Imports, Abhishek Anand, 09/17/2020
- Re: [Coq-Club] option to disable partially qualified Require Imports, Théo Zimmermann, 09/17/2020
- Re: [Coq-Club] option to disable partially qualified Require Imports, Guillaume Melquiond, 09/17/2020
  - Re: [Coq-Club] option to disable partially qualified Require Imports, Ralf Jung, 09/17/2020
    - Re: [Coq-Club] option to disable partially qualified Require Imports, Gregory Malecha, 09/17/2020
    - Re: [Coq-Club] option to disable partially qualified Require Imports, Théo Zimmermann, 09/18/2020
      - Re: [Coq-Club] option to disable partially qualified Require Imports, Ralf Jung, 09/18/2020
        
        Re: [Coq-Club] option to disable partially qualified Require Imports, Théo Zimmermann, 09/18/2020
        
        Re: [Coq-Club] option to disable partially qualified Require Imports, Gaëtan Gilbert, 09/18/2020
        
        Re: [Coq-Club] option to disable partially qualified Require Imports, Guillaume Melquiond, 09/18/2020
        Re: [Coq-Club] option to disable partially qualified Require Imports, Ralf Jung, 09/18/2020
        Re: [Coq-Club] option to disable partially qualified Require Imports, Guillaume Melquiond, 09/18/2020
        Re: [Coq-Club] option to disable partially qualified Require Imports, Abhishek Anand, 09/18/2020
        
        Re: [Coq-Club] option to disable partially qualified Require Imports, Ralf Jung, 09/18/2020
        Re: [Coq-Club] option to disable partially qualified Require Imports, Andrew Appel, 09/18/2020
        Re: [Coq-Club] option to disable partially qualified Require Imports, Andrew Appel, 09/18/2020
        Re: [Coq-Club] option to disable partially qualified Require Imports, Ralf Jung, 09/18/2020