Hi, when discussing about merging Unicoq with Mtac2, @Janno proposed to open the discussion to ship Unicoq as part of Coq. We see the following reasons:
FTR, I am in favor of this integration but, when it was last discussed, the concern that was raised by @Enrico Tassi was: We already have two unification algorithms implemented in Coq (evarconv.ml
and unification.ml
) and the project (Unifall) to get rid of the oldest of the two (unification.ml
) seems still far from having reached its completion. What will be the roadmap wrt unification if Unicoq is merged into Coq? That it eventually supersedes evarconv.ml
? How likely is that? How much more work would it represent?
I think @Matthieu Sozeau answered the first question (and only the first): yes, the plan is to supersede evarconv.ml
eventually.
@Beta Ziliani with "ship" do you mean "as part of the sources" or "as part of the platform"? Where the platform is a collection of packages we prebuild (today on windows, hopefully on other platforms in the future).
Sorry, it is clear what you mean. I'd like to know if the platform option would still be viable to you.
I think the idea in this case is quite orthogonal to the platform (and BTW, Mtac2 and thus UniCoq is included in the Windows installer as of today).
Oh, I see, sorry for the noise, I've read the message too quickly :-/
I think for the foreseeable future, most Coq installs will come via OPAM (opam install coq
), so to me the difference between bundling with Coq itself and just with the platform is significant (and for proof/tactic languages and internal Coq algorithms, which people might not understand, even larger)
Sorry, I derailed the discussion. Beta was clearly trying to minimize code duplication and maintenance cost of a piece of code. That piece of code is a variant of evarconv maintained out of tree.
A way to rephrase my concerns is: one thing is a PR adding a few ML files alongside evarconv. Another one is a PR merging unicoq and evarconv into a single file (with possibly a few extra flags to evarconv). Having the first kind of PR without a second kind followup is problematic to me.
I would directly start with a Coq PR that deduplicates the two code bases. To me there is a non zero chance that this deduplication turns out to be non trivial, and I would avoid having duplication in the Coq code base at any point in time. If this is doable in a PR, then I see no obstacle in merging it.
Maybe we can discuss this tomorrow at the Coq call, and gather the opinion of more devs.
Using the Coq Call for that would be great, there are some interesting options as how to organize the integration IMHO
Thanks guys for participating and clarifying.
I cannot promise to be available in the call (when I have time in front of a computer it is usually the case that my baby is sleeping with me ...). At what time will it be?
https://github.com/coq/coq/wiki/Coq-Call-2020-06-03
Ideally we should strive for a super-algorithm, but I prefer to start in stages. wrt the older algorithm, the problem there is that the algorithm is quite different. Instead, Unicoq and evarconv are really not thaaaat different. At the moment, changing evarconv with Unicoq in both CPDT and Mathcomp only required annotations and changes in a negligible amount of lines.
If you plan to attend just edit the wiki and add an item about unicoq
Edited. I will try to make it.
Last updated: Oct 13 2024 at 01:02 UTC