The Coq mailing list

[Théo Zimmermann <theo AT irif.fr>]

Hi Ralf,

I was only talking about the "stale vo" problem indeed.

The approach of Coq developers regarding this ambiguous import feature
so far has been to encourage users to systematically use the From
clause and to encourage library authors to avoid having several
modules named the same under a shared namespace.

Anyway, anyone, feel free to open a feature request on Coq's bug
tracker regarding this flag to disable partially qualified Require.
But I don't think we will be able to turn such a flag on by default as
long as the standard library is organized the way it is today. Feel
free also to prepare a CEP if you see a path that could lead Coq to
move away from the ambiguous import "feature" without suddenly
increasing the verbosity of every Coq file. As often, design is the
hard part.

Kind regards,
Théo

Le ven. 18 sept. 2020 à 13:26, Ralf Jung <jung AT mpi-sws.org> a écrit :
>
> 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/