Not exactly.
I guess you want to support Coq version x-1 (old) and x (current stable).
For version x, as I was saying, I do release many times for the same Coq version. For that you don't need to wait the Coq release, just a coq-elpi one.
For version x-1 I usually don't backport fixes. I did in a few occasions, and I can do it if really needed. If I do so, then what I do is to release a new version for the old Coq. For example, coq-elpi.1.16.x works with Coq 8.16, while coq-elpi.1.17.x with Coq 8.17 (the fact that the minor numbers match is just luck, usually they don't, indeed I release faster and I just caught up). If you really want to support 8.16 and you need a fix, I can release coq-elpi.1.16.x+1, tied to Coq 8.16.
As I was saying I did so in a few occasions, and we do support two version of Coq in MathComp too, so maybe it will happen again in the future. A release adding just a bugfix on a previous release takes about 20 minutes (if CI is green) + the time to get the opam package in. So it can be be done.
But sure, if I don't backport and release for the Coq x-1, then you have to wait for a release of Coq to have the fix for version x (and hence also for Coq x+1). Currently this happens every 6 months.
And just to be clear, I'm really talking about fixes to Coq-Elpi's ocaml code. locker
or any other Elpi application is just made of text files, if you really need to you can make a local copy of them (as you could do with a piece of ltac code). In some cases you don't even need to copy the code, you can just "patch" it by adding/overriding a few rules. Not clean, not bullet proof, but you may live with that for a few months.
@jung it depends what you want to express.
If any Coq-Elpi release for Coq 8.x works for you, you just depend on coq-elpi (said otherwise, if the first release of Coq-Elpi supporting Coq 8.x works then constraining Coq >= 8.x is all you need).
If you need a fix or an API addition coming with Coq-Elpi 1.y, then you declare coq-elpi >= 1.y, which will inevitably put a lower bound on Coq as well, since all coq-elpi packages are declared to work on coq >= 8.x & < 8.x+1 (and maybe coq-elpi 1.y+1 will say coq >= 8.x+1 & < 8.x+2, etc...).
Since your project may also depends on (recent) Coq features, I would recommend making both lower bounds explicit, opam would then use the most constraining one.
One project out there had an issue with coq-elpi 1.17.0, in that case it adds to the lower bound a blacklist, e.g. ">= 1.15 & != 1.17.0" (so that 1.17.1 is a good pick).
Hello, I was pointed here by the (very welcome) fixes by @Blaisorblade on HB.lock
and I'd like to answer to @msammler and @jung about Coq-Elpi's policy/compat with Coq releases.
I'm the main developer behind Coq-Elpi and I do my best to not break user code and document the changes in each release: https://github.com/LPCIC/coq-elpi/blob/master/Changelog.md
Since most of my users are in the math-comp ecosystem, I have a nix CI which tests if I break my users.
I don't have BRiCk there yet, and help to add it would be welcome (even in a non nix job).
I do provide a coq.version
API and a few gadgets like #[skip]
and #[only]
so that you can have one single code base working on multiple Coq/Coq-Elpi versions, see for example https://github.com/math-comp/hierarchy-builder/blob/c24ca1c5c91a7d9f2b3dfaa18157846956c51b2e/structures.v#L246-L260
Each Coq release requires a new Coq-Elpi release, since I use so many APIs. At the same time I develop against last Coq release, and I typically release more often than Coq so to make new APIs available to final users. Currently the master branch is on Coq 8.17, and I'm about to make a new release (the last one) for Coq 8.17. The coq-master branch, instead, is for Coq's master branch, and it is where Coq developers push fixes when they modify an API, i.e. it is the branch tracked by Coq's CI. This very rarely has any visible impact on the users of Coq-Elpi, so the need for overlays stops there. When a new Coq major version gets released I merge the two branches, and switch master development on the new Coq release. This happens in about a month after the release candidate of Coq, e.g. when the Coq Platform release process pings the community.
Hope it helps.