Skip to content

opam package is not compatible with rocq 9.0.dev #651

@RalfJung

Description

@RalfJung

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions