Stream: Coq devs & plugin devs

Topic: Moving Unicoq to Coq


view this post on Zulip Beta Ziliani (Jun 02 2020 at 15:34):

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:

view this post on Zulip Théo Zimmermann (Jun 02 2020 at 15:45):

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?

view this post on Zulip Théo Zimmermann (Jun 02 2020 at 15:46):

I think @Matthieu Sozeau answered the first question (and only the first): yes, the plan is to supersede evarconv.ml eventually.

view this post on Zulip Enrico Tassi (Jun 02 2020 at 16:13):

@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).

view this post on Zulip Enrico Tassi (Jun 02 2020 at 16:14):

Sorry, it is clear what you mean. I'd like to know if the platform option would still be viable to you.

view this post on Zulip Théo Zimmermann (Jun 02 2020 at 16:14):

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).

view this post on Zulip Enrico Tassi (Jun 02 2020 at 16:16):

Oh, I see, sorry for the noise, I've read the message too quickly :-/

view this post on Zulip Karl Palmskog (Jun 02 2020 at 16:17):

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)

view this post on Zulip Enrico Tassi (Jun 02 2020 at 16:22):

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.

view this post on Zulip Enrico Tassi (Jun 02 2020 at 16:25):

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.

view this post on Zulip Enrico Tassi (Jun 02 2020 at 16:30):

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.

view this post on Zulip Enrico Tassi (Jun 02 2020 at 16:31):

Maybe we can discuss this tomorrow at the Coq call, and gather the opinion of more devs.

view this post on Zulip Emilio Jesús Gallego Arias (Jun 02 2020 at 16:47):

Using the Coq Call for that would be great, there are some interesting options as how to organize the integration IMHO

view this post on Zulip Beta Ziliani (Jun 02 2020 at 20:01):

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?

view this post on Zulip Enrico Tassi (Jun 02 2020 at 20:05):

https://github.com/coq/coq/wiki/Coq-Call-2020-06-03

view this post on Zulip Beta Ziliani (Jun 02 2020 at 20:05):

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.

view this post on Zulip Enrico Tassi (Jun 02 2020 at 20:06):

If you plan to attend just edit the wiki and add an item about unicoq

view this post on Zulip Beta Ziliani (Jun 02 2020 at 20:13):

Edited. I will try to make it.


Last updated: Oct 16 2021 at 07:02 UTC