Stream: Coq devs & plugin devs

Topic: Code path in mutual definition


view this post on Zulip Emilio Jesús Gallego Arias (Nov 03 2020 at 18:47):

@Paolo Giarrusso , I'm moving your question here. So if you look at the code in Declare.declare_mutually_recursive , you can see that

view this post on Zulip Emilio Jesús Gallego Arias (Nov 03 2020 at 18:48):

you can see:

  let csts = CList.map2
      (fun CInfo.{ name; typ; impargs; using } body ->
         let entry = definition_entry ~opaque ~types:typ ~univs ?using body in
         declare_entry ~name ~scope ~kind ~impargs ~uctx entry)
      cinfo fixdecls

so indeed, an entry is declared for each component of the fixpoint; this makes sense due to the way the terms are built before. Unsure if the kernel is doing some sharing here?

view this post on Zulip Paolo Giarrusso (Nov 03 2020 at 18:51):

I’m unfamiliar with the internal APIs, but in Gallina abstract syntax, IIUC, fix decls for decl1 and fix decls for decl2 don’t seem to have a shared decls subnode — or at least, decls is not a term

view this post on Zulip Paolo Giarrusso (Nov 03 2020 at 18:52):

worse, a naive kernel, which works well elsewhere but not here, would provide as API “give me a Gallina AST of a closed term (up to top-level defs. etc) to typecheck and add to the environment”, which isn’t good enough here.

view this post on Zulip Paolo Giarrusso (Nov 03 2020 at 18:53):

the “shared subproblems” are the typechecking of each body decl_i in decls, which are open wrt all the other decl_j, j <> i

view this post on Zulip Paolo Giarrusso (Nov 03 2020 at 18:56):

for a user, the question is whether qed-checking for proofs by mutual fixpoint incurs an Nx slowdown when done directly, without induction principles.

view this post on Zulip Paolo Giarrusso (Nov 03 2020 at 18:58):

right now for me this is just a curiosity, but before I’ve had cases where it mattered

view this post on Zulip Emilio Jesús Gallego Arias (Nov 03 2020 at 19:01):

that part of the code / design is one of the oldest in Coq, the problem is that you need to check the projection indeed, however that's tricky as you cannot have a global let as definitions are top-level entries; ideas on how to update this part are open, we have done significant work in the last times to actually allow to work on this without breaking clienets

view this post on Zulip Paolo Giarrusso (Nov 03 2020 at 20:12):

The goal of my question is to make sure whether there's a potential issue to workaround ;-)

view this post on Zulip Paolo Giarrusso (Nov 03 2020 at 20:13):

And potentially, to mention this in the manual

view this post on Zulip Paolo Giarrusso (Nov 03 2020 at 20:13):

(but I can't promise I'll file the docs MR myself soon)

view this post on Zulip Paolo Giarrusso (Nov 03 2020 at 20:37):

Okay, Herbelin's answer confirms that too.

view this post on Zulip Hugo Herbelin (Nov 03 2020 at 21:23):

There is a CEP on global fixpoints (and a preliminary branch) which could help to address this by sending the tuple of fixpoints once.

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2020 at 01:17):

Indeed, also we could extend the current kernel to take a fixpoint and generate the projections efficiently

view this post on Zulip Emilio Jesús Gallego Arias (Nov 04 2020 at 01:17):

would likely be cleaner than the current approach


Last updated: Oct 15 2021 at 21:02 UTC