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
CC @Gregory Malecha @Janno
std.unify already taken? (the non-Evarconv unifycation routine should not be used in new code)
Yeah, it is already used for non-Evarconv unification.
We could switch Std.unify to be evarconv
Is that a good idea with respect to backward-compatibility?
I'm personally fine with doing this, since we can always use
ltac1:(x y |- unify x y) to get the old behaviour.
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.
There might be few enough users of
unify right now that compatibility might not be a big problem.
This obviously will not be true forever though
So you want ltac2 and ltac1 unify to differ? That seems strictly worse than evarconv_unify honestly
And no amount of documentation would fix that.
we could switch the ltac1 unify too
it will have to be done for unifall eventually so why wait
Are we happy with the current state of the PR, which adds new Ltac2 standard library modules
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.
I have a vague recollection of having tried the switch of Ltac's
unify to evarconv. It didn't look good.
Exposing the recommended (evarconv-based) primitives and documenting them as such sounds like a good approach.
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.)
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.
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?
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.
IIUC, Enrico said today that the rc will be tagged tomorrow.
Last updated: Nov 29 2023 at 21:01 UTC