Rodolphe Lepigre (Mar 20 2024 at 10:02): Rodolphe Lepigre (Mar 20 2024 at 10:02):How hard would it be to release a new version of coq-elpi? With the changes @Janno and I recently made, our whole code base now build fine (with a custom opam package based on master), so it'd be helpful at least for us to have a new version available on public opam directly. This might also help smoothing the transition to the interp/synterp distinction for others.
Enrico Tassi (Mar 20 2024 at 10:07):I was about to ask you if you need anything more, since the platform wants to pin, especially given the problems with Import/Export mentioned in the other thread. I understand current master works for you.
I can do a release during this week, but if you have something to add, just speak.
Rodolphe Lepigre (Mar 20 2024 at 10:10):There is one thing we rely on for the lens deriver that is not on master: https://github.com/LPCIC/coq-elpi/pull/521. But I'm not sure what the status of this MR is, and if we still want to consider another approach (CC @Janno ).
Enrico Tassi (Mar 20 2024 at 21:50):That PR is mergeable for me (the message is outdated, the PR just exposes an API to fold/unfold a primproj).
Rodolphe Lepigre (Mar 20 2024 at 21:53):In that case it should probably be merged, since we do actually rely on it. I think @Janno was arguing for a more robust fix (that would keep more terms in their original shape), but we can still do that later if we encounter problems.
Last updated: Oct 13 2024 at 01:02 UTC