Stream: Coq users

Topic: Performance of `Include` vs `Require` at large scale


view this post on Zulip 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.

view this post on Zulip 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 ;)

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Gaëtan Gilbert (May 27 2021 at 10:29):

I don't think we do

view this post on Zulip Pierre-Marie Pédrot (May 27 2021 at 10:29):

Really?

view this post on Zulip Gaëtan Gilbert (May 27 2021 at 10:30):

but we might for include ;)

view this post on Zulip Pierre-Marie Pédrot (May 27 2021 at 10:30):

Knowing what Require does just by looking at the code is a bit hard.

view this post on Zulip Pierre-Marie Pédrot (May 27 2021 at 10:30):

Include calls the cache functions (incorrectly IIRC)

view this post on Zulip Pierre-Marie Pédrot (May 27 2021 at 10:30):

@Paolo Giarrusso I'd warmly recommend to stay as far as possible from Include.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (May 27 2021 at 10:34):

even if it's already required

view this post on Zulip Pierre-Marie Pédrot (May 27 2021 at 10:34):

see Declaremods.register_library

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Paolo Giarrusso (May 27 2021 at 10:42):

My slow Requires are "I use Iris", they just take ~2s and graduated to “fast”

view this post on Zulip 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.

view this post on Zulip 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”

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Dec 08 2021 at 21:49):

Pierre-Marie Pédrot said:

Be warned that if you use Include you'll likely discover interesting bugs in the name aliasing mechanism.

Pierre-Marie, let me award you the prophet award.

view this post on Zulip 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 *)

view this post on Zulip Paolo Giarrusso (Dec 08 2021 at 21:57):

I haven't forgotten of https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Is.20Include.20not.20generative.3F.


Last updated: Feb 04 2023 at 21:02 UTC