Coq-Equations
Coq-Equations copied to clipboard
opam package is not compatible with rocq 9.0.dev
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.