Stream: Coq devs & plugin devs

Topic: Evarconv.unify as an Ltac2 primitive


view this post on Zulip Rodolphe Lepigre (Jul 10 2023 at 13:22):

I have a PR that adds Evarconv.unify as an Ltac2 primitive Std.evarconv_unify, but that name is definitely not great, so some bikeshedding is required. Another candidates is Std.new_unify, but that does not sound any better to me.

Alternatively, we could decide that Std.evarconv_unify is good enough for now (since it is long, and unambiguous), since it is easy to create an alias if a better name comes up later. (This MR is currently blocking this other PR, which needs it to add a test case for Evarconv.unify).

view this post on Zulip Rodolphe Lepigre (Jul 10 2023 at 13:22):

CC @Gregory Malecha @Janno

view this post on Zulip Enrico Tassi (Jul 10 2023 at 14:18):

Is std.unify already taken? (the non-Evarconv unifycation routine should not be used in new code)

view this post on Zulip Rodolphe Lepigre (Jul 10 2023 at 14:19):

Yeah, it is already used for non-Evarconv unification.

view this post on Zulip Gaëtan Gilbert (Jul 10 2023 at 14:20):

We could switch Std.unify to be evarconv

view this post on Zulip Rodolphe Lepigre (Jul 10 2023 at 14:26):

Is that a good idea with respect to backward-compatibility?

view this post on Zulip Rodolphe Lepigre (Jul 10 2023 at 14:27):

I'm personally fine with doing this, since we can always use ltac1:(x y |- unify x y) to get the old behaviour.

view this post on Zulip Rodolphe Lepigre (Jul 10 2023 at 14:28):

However, one thing to consider, is that the new primitive I implemented respects the transparency state of the goal, while the old Std.unifydid not. So that may be another source of potential issues.

view this post on Zulip Gregory Malecha (Jul 10 2023 at 17:52):

There might be few enough users of unify right now that compatibility might not be a big problem.

view this post on Zulip Gregory Malecha (Jul 10 2023 at 17:53):

This obviously will not be true forever though

view this post on Zulip Paolo Giarrusso (Jul 10 2023 at 20:37):

So you want ltac2 and ltac1 unify to differ? That seems strictly worse than evarconv_unify honestly

view this post on Zulip Paolo Giarrusso (Jul 10 2023 at 20:39):

And no amount of documentation would fix that.

view this post on Zulip Gaëtan Gilbert (Jul 10 2023 at 20:43):

we could switch the ltac1 unify too
it will have to be done for unifall eventually so why wait

view this post on Zulip Rodolphe Lepigre (Jul 14 2023 at 08:48):

Are we happy with the current state of the PR, which adds new Ltac2 standard library modules Unification and TransparentState?
It would certainly be a good thing to change Std.unify to use Evarconv unification (and similarly for Ltac's unify tactic), but it is probably best to experiment separately for that.

view this post on Zulip Maxime Dénès (Jul 14 2023 at 08:50):

I have a vague recollection of having tried the switch of Ltac's unify to evarconv. It didn't look good.

view this post on Zulip Maxime Dénès (Jul 14 2023 at 08:51):

Exposing the recommended (evarconv-based) primitives and documenting them as such sounds like a good approach.

view this post on Zulip Rodolphe Lepigre (Jul 14 2023 at 09:00):

Also, is there any chance my two MRs can still be included in 8.18? This one is a bug fix for Evarconv unification that we definitely need. (We always need a few extra patches, so we can cherry-pick it in our 8.18++ branch if it is too late.)

view this post on Zulip Maxime Dénès (Jul 14 2023 at 09:16):

I'm afraid we already froze and consolidated the 8.18 changelog. So only critical bug fixes would justify delaying the release IMHO (already not trivial to plan in this summer period). But I'll let @Enrico Tassi express his opinion.

view this post on Zulip Hugo Herbelin (Jul 14 2023 at 17:57):

BTW, assuming there will be a summer break, is it yet decided whether the idea is to announce 8.18 before the break, or to rather wait after the break?

view this post on Zulip Karl Palmskog (Jul 14 2023 at 18:12):

I thought it would be the usual process with an 8.18+rc1 that gets tested in lots of projects, and Platform projects do releases based on it. So in my view, the interesting question is when 8.18+rc1 will happen, so we can get it into opam, Docker containers, etc.

view this post on Zulip Hugo Herbelin (Jul 31 2023 at 17:55):

IIUC, Enrico said today that the rc will be tagged tomorrow.

view this post on Zulip Enrico Tassi (Jul 31 2023 at 19:45):

I confirm


Last updated: Jul 24 2024 at 11:01 UTC