Paolo Giarrusso (May 26 2021 at 21:48): Paolo Giarrusso (May 26 2021 at 21:48):Include seems extremely fast, comparable with Require — but how does its complexity scale? And how does it compare with module instantiation? Should I fear that Include is significantly slower because it duplicates code?
The background is that I'm thinking of using modules (and "mixins") for a large-scale project at $job, but using "mixins" seems to involve significant uses of Include. It seems to scale well for Coq's number hierarchy, but what we're doing is likely quite a bit bigger.
Gaëtan Gilbert (May 27 2021 at 08:49):Require has the property that in Require A. Any Commands. Require A. the second require is a noop
OTOH Module Import X. Include A. End X. Include A. will duplicate the effects of A (eg typeclass instances)
also Include is not the most well-understood part of the code so we look forward to your bug reports ;)
Pierre-Marie Pédrot (May 27 2021 at 10:28):In order to Include A you must have Require-d the toplevel library containing A so it's not quite a fair comparison.
Pierre-Marie Pédrot (May 27 2021 at 10:29):@Gaëtan Gilbert I don't think this is true, we still run the superglobal libobjects don't we?
Gaëtan Gilbert (May 27 2021 at 10:29):I don't think we do
Pierre-Marie Pédrot (May 27 2021 at 10:29):Really?
Gaëtan Gilbert (May 27 2021 at 10:30):but we might for include ;)
Pierre-Marie Pédrot (May 27 2021 at 10:30):Knowing what Require does just by looking at the code is a bit hard.
Pierre-Marie Pédrot (May 27 2021 at 10:30):Include calls the cache functions (incorrectly IIRC)
Pierre-Marie Pédrot (May 27 2021 at 10:30):@Paolo Giarrusso I'd warmly recommend to stay as far as possible from Include.
Pierre-Marie Pédrot (May 27 2021 at 10:31):If you have slow Requires, please open a bug report with reproducible examples and I'll have a look.
Pierre-Marie Pédrot (May 27 2021 at 10:34):@Gaëtan Gilbert if I read the code correctly, we do load the superglobal objects at any require
Pierre-Marie Pédrot (May 27 2021 at 10:34):even if it's already required
Pierre-Marie Pédrot (May 27 2021 at 10:34):see Declaremods.register_library
Pierre-Marie Pédrot (May 27 2021 at 10:38):Actually it's worse than that, we call the load function for every single object in the library.
Gaëtan Gilbert (May 27 2021 at 10:38):we don't, I just tested with Extraction Language (which is superglobal)
put
Require Extraction.
Extraction Language Haskell.
in bar
and in foo
Require Extraction tmp.bar.
Extraction nat.
Extraction Language OCaml.
Extraction nat.
Require tmp.bar.
Extraction nat.
the first says data Nat (haskell)
the other 2 say type nat (ocaml)
Gaëtan Gilbert (May 27 2021 at 10:40):oh but that's Keep
nevermind even if I give it the identity substitution I get the same behaviour
Keep vs Subst matters for
Require Extraction.
Module K.
Extraction Language Haskell.
End K.
Extraction nat.
Extraction Language OCaml.
Extraction nat.
Module L := K.
Extraction nat. (* data Nat iff Subst *)
though
Paolo Giarrusso (May 27 2021 at 10:42):My slow Requires are "I use Iris", they just take ~2s and graduated to “fast”
Pierre-Marie Pédrot (May 27 2021 at 10:44):Be warned that if you use Include you'll likely discover interesting bugs in the name aliasing mechanism.
Paolo Giarrusso (May 27 2021 at 10:46):Ahah, is that why sometimes I get aliases and sometimes copies? I had mentally filed that under “to investigate”
Paolo Giarrusso (May 27 2021 at 10:50):For now “export isn’t as good as global” is more annoying: since instances are duplicated (not just by Include, Module A := B. does that, and that’s the only reasonable semantics for Global Hints), I figured every hint had to be an export hint.
Gaëtan Gilbert (May 27 2021 at 10:52):Pierre-Marie Pédrot said:
Gaëtan Gilbert if I read the code correctly, we do load the superglobal objects at any require
see Declaremods.register_library
earlier Library.rec_intern_library produces the list of not-yet-required dependencies, which is why we don't double require
Paolo Giarrusso (May 28 2021 at 11:43):FWIW, my use-case uses Include mostly on Module Type, not Module, which makes it (a) harder to avoid (b) potentially a bit less buggy.
Paolo Giarrusso (Dec 08 2021 at 21:49):Pierre-Marie Pédrot said:
Be warned that if you use
Includeyou'll likely discover interesting bugs in the name aliasing mechanism.
Pierre-Marie, let me award you the prophet award.
Paolo Giarrusso (Dec 08 2021 at 21:56):Actually, I and @Janno are kinda confused. What does it mean if an "alias" of an axiom is a definition? From https://github.com/bedrocksystems/BRiCk/blob/614b303aa6370ecfcb354ec9715e65a5a5a28630/theories/lang/cpp/semantics/values.v#L399-L401
Declare Module PTRS_INTF_AXIOM : PTRS_INTF.
Module Export VALUES_INTF_AXIOM <: VALUES_INTF := PTRS_INTF_AXIOM <+ VALUES_INTF_FUNCTOR.
gives:
Locate _offset_ptr.
(*
Constant values.VALUES_INTF_AXIOM._offset_ptr
(alias of PTRS_INTF_AXIOM._offset_ptr)
Constant values.PTRS_INTF_AXIOM._offset_ptr
(shorter name to refer to it in current context is PTRS_INTF_AXIOM._offset_ptr)
*)
Print _offset_ptr.
Print PTRS_INTF_AXIOM._offset_ptr.
(*
offset_ptr = PTRS_INTF_AXIOM._offset_ptr
: ptr → offset → ptr
Arguments _offset_ptr _%ptr_scope _%offset_scope
*** [ PTRS_INTF_AXIOM._offset_ptr :
PTRS_INTF_AXIOM.ptr → PTRS_INTF_AXIOM.offset → PTRS_INTF_AXIOM.ptr ]
Arguments PTRS_INTF_AXIOM._offset_ptr _%ptr_scope _%offset_scope *)
I haven't forgotten of https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Is.20Include.20not.20generative.3F.
Last updated: Sep 30 2023 at 05:01 UTC