Rodolphe Lepigre (Jul 10 2023 at 13:22): 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).
Rodolphe Lepigre (Jul 10 2023 at 13:22):CC @Gregory Malecha @Janno
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)
Rodolphe Lepigre (Jul 10 2023 at 14:19):Yeah, it is already used for non-Evarconv unification.
Gaëtan Gilbert (Jul 10 2023 at 14:20):We could switch Std.unify to be evarconv
Rodolphe Lepigre (Jul 10 2023 at 14:26):Is that a good idea with respect to backward-compatibility?
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.
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.
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.
Gregory Malecha (Jul 10 2023 at 17:53):This obviously will not be true forever though
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
Paolo Giarrusso (Jul 10 2023 at 20:39):And no amount of documentation would fix that.
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
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.
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.
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.
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.)
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.
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?
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.
Hugo Herbelin (Jul 31 2023 at 17:55):IIUC, Enrico said today that the rc will be tagged tomorrow.
Enrico Tassi (Jul 31 2023 at 19:45):I confirm
Last updated: Oct 13 2024 at 01:02 UTC