Stream: Coq devs & plugin devs

Topic: normalization of universes in interactive mutual fixpoints


view this post on Zulip Hugo Herbelin (Nov 03 2020 at 18:27):

My investigations in universes have shown that in interactive mutual fixpoints, the result of the Qed-time minimization is applied to the first statement of the mutual fixpoint but not to the other statements. Thanks to the cleaning of declaration paths (which is a pleasure to navigate in) it seems to me that this (apparently) long-standing issue could be solved by letting Declare.Proof.close_proofmanage itself the production of the n entries of the mutual entry rather than building one and letting declare_mutdef build the others. Does it make sense? Any objections or recommendations about trying to fix that?

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

I think @Hugo Herbelin the main problem there is users of close_proof do not know about multiple entries; actually, isn't the interactive case doing the right thing already?

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

A first step could be actually to unify more the interactive / non-interactive path

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

Side question: do you know if the mutual inductive is typechecked only once, instead of N times for the N mutual fixpoints, even tho Coq must produce N separate proof terms?

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

(sorry to hijack the thread)

view this post on Zulip Hugo Herbelin (Nov 03 2020 at 18:44):

(no problem, digressing is natural)

view this post on Zulip Hugo Herbelin (Nov 03 2020 at 18:49):

As far as I can tell, the kernel do N distinct checks, one for each component of the mutual fixpoint. answered in Code path in mutual definition

view this post on Zulip Hugo Herbelin (Nov 03 2020 at 18:53):

@ejgallego: I don't know the code as well as you do, close_proof returns a list of entries, so it is easy to know if there is one. What are the users of close_proof which do not know about multiple entries?

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

@Hugo Herbelin many clients don't support multiple entries, as of today the multiple entries system is only used by equations and derive, but indeed it needs some tweaks as the api still needs improvement

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

it needs some tweaks as the api still needs improvement

So the simplest is maybe to wait first for further API improvements on your side.

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

There was a plan to discuss with @Matthieu Sozeau about how to evolve the API, I don't have many concrete plans as of now, so IMHO this is something we could do at CUDW.

view this post on Zulip Hugo Herbelin (Nov 04 2020 at 07:24):

many clients don't support multiple entries, as of today the multiple entries system is only used by equations and derive

Are you saying that the Proof_ending.t (Regular, End_derive, ...) should be known from close_proof already, so that close_proof can use this information to produce the appropriate entries? But maybe this is the same as saying that close_proof and finalize_proof could be merged?

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

Indeed, these are two mechanism that are similar yet disjoint; unfortunately it doesn't seem trivial to do, but we'd like to discuss how to do it.


Last updated: Oct 15 2021 at 19:03 UTC