Stream: Coq users

Topic: Use of “Require” inside a module is fragile.


view this post on Zulip Pierre Rousselin (Nov 02 2023 at 15:23):

Why is it not recommended to Require inside a module? Doesn't it defeat the purpose to actually hide the implementation?
If I Require a file globally, then the population of lemmas will grow enormously.

view this post on Zulip Kenji Maillard (Nov 02 2023 at 15:34):

Isn't it a question of Require vs Import ? Just requiring a module will not make the names defined in the module available, but will execute some of its side-effects I think, so I would expect it is advised to do it globally so that the order of execution remain predictable.

view this post on Zulip Gaëtan Gilbert (Nov 02 2023 at 15:35):

Require inside a module is not hidden

view this post on Zulip Pierre Rousselin (Nov 02 2023 at 15:52):

But then how to effectively hide stuff? For instance if I Require Rdefinitions.v I end up with (litterally) thousands of identifiers. How could it be possible (for instance for teaching purposes, but I believe it would be needed elsewhere to) to only get the few dozens of lemmas a module (or a file) defines? So that, Search _. gives something manageable?

view this post on Zulip Gaëtan Gilbert (Nov 02 2023 at 15:53):

It's not possible.

view this post on Zulip Karl Palmskog (Nov 02 2023 at 15:53):

I think the standard answer is: "use Search blacklists"

view this post on Zulip Gaëtan Gilbert (Nov 02 2023 at 15:54):

see also https://github.com/coq/ceps/pull/62

view this post on Zulip Pierre Rousselin (Nov 02 2023 at 15:54):

Then it's a problem I think. I'm a strong believer in the benefits of encapsulation and modularity.

view this post on Zulip Pierre Rousselin (Nov 02 2023 at 15:58):

Thanks for the link and the advice. I don't think Search blacklist can handle everything on its own, though.

view this post on Zulip Paolo Giarrusso (Nov 03 2023 at 13:37):

FWIW, I'd also often replace Require Import foo with Require foo. <code block> Import foo., but that can be a dangerous refactoring if there's a mix of Require-time side effects with Import-time side effects.

It's fine if <code block> never depends on hints from foo, but there's no way to enforce this.

view this post on Zulip Paolo Giarrusso (Nov 03 2023 at 13:39):

@Pierre Rousselin I think your only option today is to functorize everything. If your actual code only depend on the interface of Foo, then requires needed only to implement Foo would only be visible when linking the system together.

view this post on Zulip Paolo Giarrusso (Nov 03 2023 at 13:40):

however, functorizing everything has overhead quadratic in the depth of the hierarchy — https://github.com/coq/ceps/pull/62 seems indeed relevant here (tho I _might_ be biased as a coauthor)


Last updated: Jun 13 2024 at 21:01 UTC