Hugo Herbelin (Nov 03 2020 at 18:27): 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?
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?
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
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?
Paolo Giarrusso (Nov 03 2020 at 18:43):(sorry to hijack the thread)
Hugo Herbelin (Nov 03 2020 at 18:44):(no problem, digressing is natural)
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
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?
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
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.
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.
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?
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: Sep 09 2024 at 05:02 UTC