Pierre Rousselin (Nov 02 2023 at 15:23): 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.
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.
Gaëtan Gilbert (Nov 02 2023 at 15:35):Require inside a module is not hidden
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?
Gaëtan Gilbert (Nov 02 2023 at 15:53):It's not possible.
Karl Palmskog (Nov 02 2023 at 15:53):I think the standard answer is: "use Search blacklists"
Gaëtan Gilbert (Nov 02 2023 at 15:54):see also https://github.com/coq/ceps/pull/62
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.
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.
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.
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.
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: Oct 13 2024 at 01:02 UTC