New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
omega, romega, lia: pick one #7872
Comments
I think @letouzey probably has some experience to share on this question. |
You must be confusing me with someone... I don't remember ever doing experiments like that.^^ However, what I can say is that in Iris, was prefer to use EDIT: I just replaced all sues of |
@Zimmi48 I don't know how I forgot to cite Pierre's nickname, he's clearly the one who can answer some of the questions above. Thanks! @RalfJung Really? I remember a discussion on gitter where somebody was impressed by the performance of |
Well yeah Robbert told me about that when he re-wrote Iris 3 or 4 years ago. I'm using lia ever since. That was way before I joined Gitter.^^ |
Ok, then I'm definitely confusing you with someone else, sorry about the noise! Anyway, it was useful to learn that for Iris, |
Yeah the discussion on Gitter definitely happened but I don't know who took part. |
Around https://gitter.im/coq/coq?at=5a87038e76ced47639eee0f4 Joachim Breitner
|
I just discovered that some proofs in |
I recently found a case where |
More generally, I've yet to encounter a case in fiat-crypto where |
Killing the legacy code of Now, should we go for So for now I'd vote for PS: I'm also slightly worried by the dependency order : is it that simple to build |
Here is one example that
I am not sure if this is a good example, since |
In the situations where I am using them, I find usually |
@maximedenes You're right. And I had just looked at #7886 when I wrote my post... At least, my example is a little simpler. |
|
The redundancy between these three tactics is putting some burden on maintainers of the system. For example, #186 is much more costly to implement than it should be. I believe the situation is also confusing newcomers. I would like to understand what is the plan to resolve this redundancy, and help implement it.
Here's my understanding of the situation:
romega
was started 17 years ago (according to its header). It is meant as a reflection-based replacement ofomega
but hasn't reached full compatibility. I don't know if it is the sign of serious difficulty in resolving the incompatibilities.romega
is undocumentedromega
should always be preferred toomega
(reflection should bring some performance improvements).lia
has incomparable power (sometimes it can do more than(r)omega
, sometimes less (that's what I thought, although the manual seems to say that it is strictly more powerful).I believe our manpower is way too limited (compared to the size of the code base) to afford maintaining the three. Note however that
lia
is part of the largermicromega
, for which I don't think there exists a general replacement. Not maintaing two of them doesn't necessarily mean making them disappear, but rather moving them out of the Coq repo and calling for external maintainers.So I believe the first question that needs to be evaluated is: can
lia
be used as a replacement for(r)omega
in practice today? I believe @RalfJung experimented it recently, maybe he can give some feedback.If the answer is no, then maybe we should favor
romega
, starting with writing down all known incompatibilties that have been resisting for all those years.@ppedrot do you know if it would be hard to rebind
(r)omega
tolia
, so that we could see what it gives on our CI?The text was updated successfully, but these errors were encountered: