-
Notifications
You must be signed in to change notification settings - Fork 49
Description
We typically track the latest stable dev
branch in CI to ensure that when there's a point release, all our packages keep working. However, it seems that currently there is no version of rocq-equations that's compatible with 9.0.dev? At least, opam can't find a solution. This is probably caused by the following dependency declaration in the rocq-equations.1.3.1+9.0 package:
"rocq-prover" {>= "9.0~" & != "dev" & != "9.0.dev"}
Why does this forbid the dev
versions? In the past those were accepted just fine (coq-equations 1.3.1+8.20 doesn't have anything like this), and that's quite crucial to be able to test the next Rocq release before it is out (i.e., before our users run into issues due to incompatibilities).
My understanding of opam versions is that if I install a dev
package, then build failures can occur and that's fine -- but fundamentally one cannot test pre-releases if opam files are all written in a way that excludes dev
versions just because they might fail.