The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

We perhaps could add a syntax with leading dot, so in

    Require .Foo.Bar Baz.

Foo.Bar is fully qualified, Baz isn't.

(kind of like internet domain names with trailing dot)

Gaëtan Gilbert

On 18/09/2020 13:48, Théo Zimmermann wrote:
> 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/